inductive Auto.Pos : Type

• xH : Pos
• xO : Pos → Pos
• xI : Pos → Pos

instance Auto.instInhabitedPos : Inhabited Pos

Equations

• Auto.instInhabitedPos = { default := Auto.Pos.xH }

instance Auto.instHashablePos : Hashable Pos

Equations

• Auto.instHashablePos = { hash := Auto.hashPos✝ }

instance Auto.instToExprPos : Lean.ToExpr Pos

Equations

• Auto.instToExprPos = { toExpr := Auto.toExprPos✝, toTypeExpr := Lean.Expr.const `Auto.Pos [] }

@[reducible, inline]

abbrev Auto.Pos.one : Pos

Equations

• Auto.Pos.one = Auto.Pos.xH

def Auto.Pos.toNat' : Pos → Nat

Equations

• Auto.Pos.xH.toNat' = 1
• a.xO.toNat' = a.toNat' * 2
• a.xI.toNat' = a.toNat' * 2 + 1

def Auto.Pos.toNat (p : Pos) : Nat

Equations

• p.toNat = p.toNat'.pred

theorem Auto.Pos.toNat'_not_zero (p : Pos) : p.toNat' ≠ 0

@[irreducible]

def Auto.Pos.ofNat'WF (n : Nat) : Pos

Equations

• Auto.Pos.ofNat'WF 0 = Auto.Pos.xH
• Auto.Pos.ofNat'WF 1 = Auto.Pos.xH
• Auto.Pos.ofNat'WF n_2.succ.succ = match n_2.succ.succ % 2 with | 0 => (Auto.Pos.ofNat'WF (n_2.succ.succ / 2)).xO | x => (Auto.Pos.ofNat'WF (n_2.succ.succ / 2)).xI

@[irreducible]

def Auto.Pos.ofNat'WF.inductionOn {motive : Nat → Sort u} (ind : (x : Nat) → motive ((x + 2) / 2) → motive (x + 2)) (base₀ : motive 0) (base₁ : motive 1) (x : Nat) : motive x

Equations

• Auto.Pos.ofNat'WF.inductionOn ind base₀ base₁ 0 = base₀
• Auto.Pos.ofNat'WF.inductionOn ind base₀ base₁ 1 = base₁
• Auto.Pos.ofNat'WF.inductionOn ind base₀ base₁ n_1.succ.succ = ind n_1 (Auto.Pos.ofNat'WF.inductionOn ind base₀ base₁ ((n_1 + 2) / 2))

@[irreducible]

def Auto.Pos.ofNat'WF.induction {motive : Nat → Sort u} (ind : (x : Nat) → motive ((x + 2) / 2) → motive (x + 2)) (base₀ : motive 0) (base₁ : motive 1) (x : Nat) : motive x

Equations

• Auto.Pos.ofNat'WF.induction ind base₀ base₁ x = Auto.Pos.ofNat'WF.inductionOn ind base₀ base₁ x

theorem Auto.Pos.ofNat'WF.succSucc (n : Nat) : ofNat'WF (n + 2) = match (n + 2) % 2 with | 0 => (ofNat'WF ((n + 2) / 2)).xO | x => (ofNat'WF ((n + 2) / 2)).xI

theorem Auto.Pos.ofNat'WF.double_xO (n : Nat) : n ≠ 0 → ofNat'WF (n * 2) = (ofNat'WF n).xO

theorem Auto.Pos.ofNat'WF.doubleSucc_xI (n : Nat) : n ≠ 0 → ofNat'WF (n * 2 + 1) = (ofNat'WF n).xI

theorem Auto.Pos.ofNat'WF_toNat' (p : Pos) : ofNat'WF p.toNat' = p

theorem Auto.Pos.toNat'_ofNat'WF (n : Nat) : n ≠ 0 → (ofNat'WF n).toNat' = n

def Auto.Pos.ofNat'RD (rd n : Nat) : Pos

Equations

• Auto.Pos.ofNat'RD 0 n = Auto.Pos.xH
• Auto.Pos.ofNat'RD rd'.succ 0 = Auto.Pos.xH
• Auto.Pos.ofNat'RD rd'.succ 1 = Auto.Pos.xH
• Auto.Pos.ofNat'RD rd'.succ n = match n.mod 2 with | 0 => (Auto.Pos.ofNat'RD rd' (n.div 2)).xO | x => (Auto.Pos.ofNat'RD rd' (n.div 2)).xI

theorem Auto.Pos.ofNat'.equivAux (rd n : Nat) : rd ≥ n → ofNat'WF n = ofNat'RD rd n

def Auto.Pos.ofNat' (n : Nat) : Pos

Equations

• Auto.Pos.ofNat' n = Auto.Pos.ofNat'RD n n

theorem Auto.Pos.ofNat'.equiv (n : Nat) : ofNat'WF n = ofNat' n

def Auto.Pos.ofNat (n : Nat) : Pos

Equations

• Auto.Pos.ofNat n = Auto.Pos.ofNat' n.succ

def Auto.Pos.reprPrec (p : Pos) : Nat → Std.Format

Equations

• p.reprPrec x✝ = Std.format "Pos.ofNat " ++ Std.format p.toNat ++ Std.format ""

instance Auto.Pos.instRepr : Repr Pos

Equations

• Auto.Pos.instRepr = { reprPrec := Auto.Pos.reprPrec }

def Auto.Pos.beq (p q : Pos) : Bool

Equations

• Auto.Pos.xH.beq Auto.Pos.xH = true
• p'.xO.beq q'.xO = p'.beq q'
• p'.xI.beq q'.xI = p'.beq q'
• x✝¹.beq x✝ = false

theorem Auto.Pos.beq_refl {p : Pos} : p.beq p = true

theorem Auto.Pos.eq_of_beq_eq_true {p q : Pos} : p.beq q = true → p = q

theorem Auto.Pos.ne_of_beq_eq_false {p q : Pos} : p.beq q = false → p ≠ q

instance Auto.Pos.instBEq : BEq Pos

Equations

• Auto.Pos.instBEq = { beq := Auto.Pos.beq }

instance Auto.Pos.instLawfulBEq : LawfulBEq Pos

def Auto.Pos.succ (p : Pos) : Pos

Equations

• Auto.Pos.xH.succ = Auto.Pos.xH.xO
• a.xO.succ = a.xI
• a.xI.succ = a.succ.xO

def Auto.Pos.predXO : Pos → Pos

Equations

• Auto.Pos.xH.predXO = Auto.Pos.xH
• a.xO.predXO = a.predXO.xI
• a.xI.predXO = a.xO.xI

def Auto.Pos.pred (p : Pos) : Pos

Equations

• Auto.Pos.xH.pred = Auto.Pos.xH
• a.xO.pred = a.predXO
• a.xI.pred = a.xO

theorem Auto.Pos.succ_neq (p : Pos) : p ≠ p.succ

theorem Auto.Pos.pred_neq (p : Pos) : p ≠ xH → p ≠ p.pred

theorem Auto.Pos.predXO_spec (p : Pos) : p.predXO = p.xO.pred

theorem Auto.Pos.succ_predXO (p : Pos) : p.predXO.succ = p.xO

theorem Auto.Pos.predXO_succ (p : Pos) : p.succ.predXO = p.xI

theorem Auto.Pos.double_succ (p : Pos) : p.succ.xO = p.xO.succ.succ

theorem Auto.Pos.predXO_neq_xO (p : Pos) : p.predXO ≠ p.xO

theorem Auto.Pos.succ_not_1 (p : Pos) : p.succ ≠ one

theorem Auto.Pos.pred_succ_eq (p : Pos) : p.succ.pred = p

theorem Auto.Pos.succ_pred_xO (p : Pos) : p.xO.pred.succ = p.xO

theorem Auto.Pos.succ_pred_xI (p : Pos) : p.xI.pred.succ = p.xI

theorem Auto.Pos.neq_XH_succ_pred_eq (p : Pos) : p ≠ xH → p.pred.succ = p

theorem Auto.Pos.succ_inj (p q : Pos) : p.succ = q.succ → p = q