kmill

This is an analysis of https://codegolf.stackexchange.com/a/203685/78112
like in https://gist.github.com/kmill/266ef6bb5690f9c26110673dcc59f710

Input: n A

1. M1    +      A -> M2 + 10 B
2  M1             -> M2 + A
3. M2  +  A + Div -> M1 + B
4. M2 + 4 B + Div -> M1 + A
5. M2             -> Count

kmill

inductive binary_tree : Type
| root : binary_tree
| tree : binary_tree → binary_tree → binary_tree

namespace binary_tree

def mirror : binary_tree → binary_tree
| root := root
| (tree a b) := tree (mirror b) (mirror a)

kmill

/-
A constructive proof of the cantor diagonalization argument: there is
no bijection between a set and its powerset.  Since Lean is based on
type theory, we use a type α rather than a set, and for convenience we
use (α → bool) to represent the powerset, i.e. indicator functions on α.
-/

import data.equiv.basic

open function