inductive HF : Type

• empty : HF
• insert : HF → HF → HF

def instDecidableEqHF.decEq (x✝ x✝¹ : HF) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqHF.decEq HF.empty HF.empty = isTrue ⋯
• instDecidableEqHF.decEq HF.empty (a.insert a_1) = isFalse ⋯
• instDecidableEqHF.decEq (a.insert a_1) HF.empty = isFalse ⋯

@[implicit_reducible]

instance instDecidableEqHF : DecidableEq HF

Equations

• instDecidableEqHF = instDecidableEqHF.decEq

def instReprHF.repr : HF → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprHF.repr HF.empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HF.empty")).group prec✝

@[implicit_reducible]

instance instReprHF : Repr HF

Equations

• instReprHF = { reprPrec := instReprHF.repr }

theorem Nat.testBit_zero_number (i : Nat) : testBit 0 i = false

Bit 0 of zero is always false (Lean core Nat.zero_testBit).

theorem Nat.testBit_shiftl (a i : Nat) : (1 <<< a).testBit i = (i == a)

Single-bit mask: (1 <<< a) has bit i set iff i = a.

def toNat : HF → Nat

Equations

• toNat HF.empty = 0
• toNat (a.insert a_1) = toNat a_1 ||| 1 <<< toNat a

def ExtEq (x y : HF) : Prop

Equations

• ExtEq x y = (toNat x = toNat y)

def Mem (x y : HF) : Prop

Equations

• Mem x y = ((toNat y).testBit (toNat x) = true)

def HF.pair (x y : HF) : HF

Equations

• x.pair y = x.insert (y.insert HF.empty)

def HF.union : HF → HF → HF

Equations

• HF.empty.union x✝ = x✝
• (x_2.insert z).union x✝ = x_2.insert (z.union x✝)

theorem ExtEq.refl (x : HF) : ExtEq x x

theorem ExtEq.symm {x y : HF} (h : ExtEq x y) : ExtEq y x

theorem ExtEq.trans {x y z : HF} (h1 : ExtEq x y) (h2 : ExtEq y z) : ExtEq x z

theorem bool_or_iff (a b : Bool) : (a || b) = true ↔ a = true ∨ b = true

theorem mem_empty_iff (z : HF) : Mem z HF.empty ↔ False

theorem mem_insert (x y z : HF) : Mem z (x.insert y) ↔ ExtEq z x ∨ Mem z y

theorem mem_pair (x y z : HF) : Mem z (x.pair y) ↔ ExtEq z x ∨ ExtEq z y

theorem toNat_union (x y : HF) : toNat (x.union y) = toNat x ||| toNat y

theorem mem_union (x y z : HF) : Mem z (x.union y) ↔ Mem z x ∨ Mem z y

theorem ExtEq_pair {x₁ x₂ y₁ y₂ : HF} (hx : ExtEq x₁ x₂) (hy : ExtEq y₁ y₂) : ExtEq (x₁.pair y₁) (x₂.pair y₂)

theorem ExtEq_union {x₁ x₂ y₁ y₂ : HF} (hx : ExtEq x₁ x₂) (hy : ExtEq y₁ y₂) : ExtEq (x₁.union y₁) (x₂.union y₂)