[GOAL]
m n : ℕ
⊢ bodd (subNatNat m n) = xor (Nat.bodd m) (Nat.bodd n)
[PROOFSTEP]
apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd
[GOAL]
case hp
m n : ℕ
⊢ ∀ (i n : ℕ), bodd ↑i = xor (Nat.bodd (n + i)) (Nat.bodd n)
[PROOFSTEP]
intros i j
[GOAL]
case hn
m n : ℕ
⊢ ∀ (i m : ℕ), bodd -[i+1] = xor (Nat.bodd m) (Nat.bodd (m + i + 1))
[PROOFSTEP]
intros i j
[GOAL]
case hp
m n i j : ℕ
⊢ bodd ↑i = xor (Nat.bodd (j + i)) (Nat.bodd j)
[PROOFSTEP]
simp only [Int.bodd, Int.bodd_coe, Nat.bodd_add]
[GOAL]
case hn
m n i j : ℕ
⊢ bodd -[i+1] = xor (Nat.bodd j) (Nat.bodd (j + i + 1))
[PROOFSTEP]
simp only [Int.bodd, Int.bodd_coe, Nat.bodd_add]
[GOAL]
case hp
m n i j : ℕ
⊢ Nat.bodd i = xor (xor (Nat.bodd j) (Nat.bodd i)) (Nat.bodd j)
[PROOFSTEP]
cases Nat.bodd i
[GOAL]
case hn
m n i j : ℕ
⊢ (!Nat.bodd i) = xor (Nat.bodd j) (xor (xor (Nat.bodd j) (Nat.bodd i)) (Nat.bodd 1))
[PROOFSTEP]
cases Nat.bodd i
[GOAL]
case hp.false
m n i j : ℕ
⊢ false = xor (xor (Nat.bodd j) false) (Nat.bodd j)
[PROOFSTEP]
simp
[GOAL]
case hp.true
m n i j : ℕ
⊢ true = xor (xor (Nat.bodd j) true) (Nat.bodd j)
[PROOFSTEP]
simp
[GOAL]
case hn.false
m n i j : ℕ
⊢ (!false) = xor (Nat.bodd j) (xor (xor (Nat.bodd j) false) (Nat.bodd 1))
[PROOFSTEP]
simp
[GOAL]
case hn.true
m n i j : ℕ
⊢ (!true) = xor (Nat.bodd j) (xor (xor (Nat.bodd j) true) (Nat.bodd 1))
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ bodd (negOfNat n) = Nat.bodd n
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ bodd (negOfNat Nat.zero) = Nat.bodd Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
⊢ bodd (negOfNat (Nat.succ n✝)) = Nat.bodd (Nat.succ n✝)
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
⊢ bodd (negOfNat (Nat.succ n✝)) = !Nat.bodd n✝
[PROOFSTEP]
rfl
[GOAL]
n : ℤ
⊢ bodd (-n) = bodd n
[PROOFSTEP]
cases n with
| ofNat =>
  rw [← negOfNat_eq, bodd_negOfNat]
  simp
| negSucc n =>
  rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
  change (!Nat.bodd n) = !(bodd n)
  rw [bodd_coe]
    -- Porting note: Heavily refactored proof, used to work all with `simp`:
    -- `cases n <;> simp [Neg.neg, Int.coe_nat_eq, Int.neg, bodd, -of_nat_eq_coe]`
[GOAL]
n : ℤ
⊢ bodd (-n) = bodd n
[PROOFSTEP]
cases n with
| ofNat =>
  rw [← negOfNat_eq, bodd_negOfNat]
  simp
| negSucc n =>
  rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
  change (!Nat.bodd n) = !(bodd n)
  rw [bodd_coe]
    -- Porting note: Heavily refactored proof, used to work all with `simp`:
    -- `cases n <;> simp [Neg.neg, Int.coe_nat_eq, Int.neg, bodd, -of_nat_eq_coe]`
[GOAL]
case ofNat
a✝ : ℕ
⊢ bodd (-ofNat a✝) = bodd (ofNat a✝)
[PROOFSTEP]

| ofNat =>
  rw [← negOfNat_eq, bodd_negOfNat]
  simp
[GOAL]
case ofNat
a✝ : ℕ
⊢ bodd (-ofNat a✝) = bodd (ofNat a✝)
[PROOFSTEP]
rw [← negOfNat_eq, bodd_negOfNat]
[GOAL]
case ofNat
a✝ : ℕ
⊢ Nat.bodd a✝ = bodd (ofNat a✝)
[PROOFSTEP]
simp
[GOAL]
case negSucc
n : ℕ
⊢ bodd (- -[n+1]) = bodd -[n+1]
[PROOFSTEP]

| negSucc n =>
  rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
  change (!Nat.bodd n) = !(bodd n)
  rw [bodd_coe]
    -- Porting note: Heavily refactored proof, used to work all with `simp`:
    -- `cases n <;> simp [Neg.neg, Int.coe_nat_eq, Int.neg, bodd, -of_nat_eq_coe]`
[GOAL]
case negSucc
n : ℕ
⊢ bodd (- -[n+1]) = bodd -[n+1]
[PROOFSTEP]
rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
[GOAL]
case negSucc
n : ℕ
⊢ (!Nat.bodd n) = bodd -[n+1]
[PROOFSTEP]
change (!Nat.bodd n) = !(bodd n)
[GOAL]
case negSucc
n : ℕ
⊢ (!Nat.bodd n) = !bodd ↑n
[PROOFSTEP]
rw [bodd_coe]
  -- Porting note: Heavily refactored proof, used to work all with `simp`:
  -- `cases n <;> simp [Neg.neg, Int.coe_nat_eq, Int.neg, bodd, -of_nat_eq_coe]`
[GOAL]
m n : ℤ
⊢ bodd (m + n) = xor (bodd m) (bodd n)
[PROOFSTEP]
cases' m with m m
[GOAL]
case ofNat
n : ℤ
m : ℕ
⊢ bodd (ofNat m + n) = xor (bodd (ofNat m)) (bodd n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case negSucc
n : ℤ
m : ℕ
⊢ bodd (-[m+1] + n) = xor (bodd -[m+1]) (bodd n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat.ofNat
m n : ℕ
⊢ bodd (ofNat m + ofNat n) = xor (bodd (ofNat m)) (bodd (ofNat n))
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat, negSucc_add_negSucc, bodd_subNatNat]
[GOAL]
case ofNat.negSucc
m n : ℕ
⊢ bodd (ofNat m + -[n+1]) = xor (bodd (ofNat m)) (bodd -[n+1])
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat, negSucc_add_negSucc, bodd_subNatNat]
[GOAL]
case negSucc.ofNat
m n : ℕ
⊢ bodd (-[m+1] + ofNat n) = xor (bodd -[m+1]) (bodd (ofNat n))
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat, negSucc_add_negSucc, bodd_subNatNat]
[GOAL]
case negSucc.negSucc
m n : ℕ
⊢ bodd (-[m+1] + -[n+1]) = xor (bodd -[m+1]) (bodd -[n+1])
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat, negSucc_add_negSucc, bodd_subNatNat]
[GOAL]
case ofNat.ofNat
m n : ℕ
⊢ bodd (↑m + ↑n) = xor (bodd ↑m) (bodd ↑n)
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_add, Bool.xor_comm, ← Nat.cast_add]
[GOAL]
case ofNat.negSucc
m n : ℕ
⊢ xor (Nat.bodd m) (Nat.bodd (Nat.succ n)) = xor (bodd ↑m) (bodd -[n+1])
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_add, Bool.xor_comm, ← Nat.cast_add]
[GOAL]
case negSucc.ofNat
m n : ℕ
⊢ xor (Nat.bodd n) (Nat.bodd (Nat.succ m)) = xor (bodd -[m+1]) (bodd ↑n)
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_add, Bool.xor_comm, ← Nat.cast_add]
[GOAL]
case negSucc.negSucc
m n : ℕ
⊢ bodd -[Nat.succ (m + n)+1] = xor (bodd -[m+1]) (bodd -[n+1])
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_add, Bool.xor_comm, ← Nat.cast_add]
[GOAL]
case negSucc.negSucc
m n : ℕ
⊢ Nat.bodd (Nat.succ (m + n) + 1) = Nat.bodd (m + 1 + (n + 1))
[PROOFSTEP]
rw [← Nat.succ_add, add_assoc]
  -- Porting note: Heavily refactored proof, used to work all with `simp`:
  -- `by cases m with m m; cases n with n n; unfold has_add.add;`
  -- `simp [int.add, -of_nat_eq_coe, bool.bxor_comm]`
[GOAL]
m n : ℤ
⊢ bodd (m * n) = (bodd m && bodd n)
[PROOFSTEP]
cases' m with m m
[GOAL]
case ofNat
n : ℤ
m : ℕ
⊢ bodd (ofNat m * n) = (bodd (ofNat m) && bodd n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case negSucc
n : ℤ
m : ℕ
⊢ bodd (-[m+1] * n) = (bodd -[m+1] && bodd n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat.ofNat
m n : ℕ
⊢ bodd (ofNat m * ofNat n) = (bodd (ofNat m) && bodd (ofNat n))
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat, negSucc_mul_negSucc]
[GOAL]
case ofNat.negSucc
m n : ℕ
⊢ bodd (ofNat m * -[n+1]) = (bodd (ofNat m) && bodd -[n+1])
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat, negSucc_mul_negSucc]
[GOAL]
case negSucc.ofNat
m n : ℕ
⊢ bodd (-[m+1] * ofNat n) = (bodd -[m+1] && bodd (ofNat n))
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat, negSucc_mul_negSucc]
[GOAL]
case negSucc.negSucc
m n : ℕ
⊢ bodd (-[m+1] * -[n+1]) = (bodd -[m+1] && bodd -[n+1])
[PROOFSTEP]
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat, negSucc_mul_negSucc]
[GOAL]
case ofNat.ofNat
m n : ℕ
⊢ bodd ↑(m * n) = (bodd ↑m && bodd ↑n)
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_mul]
  -- Porting note: Heavily refactored proof, used to be:
  -- `by cases m with m m; cases n with n n;`
  -- `simp [← int.mul_def, int.mul, -of_nat_eq_coe, bool.bxor_comm]`
[GOAL]
case ofNat.negSucc
m n : ℕ
⊢ bodd (-↑(m * Nat.succ n)) = (bodd ↑m && bodd -[n+1])
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_mul]
  -- Porting note: Heavily refactored proof, used to be:
  -- `by cases m with m m; cases n with n n;`
  -- `simp [← int.mul_def, int.mul, -of_nat_eq_coe, bool.bxor_comm]`
[GOAL]
case negSucc.ofNat
m n : ℕ
⊢ bodd (-↑(Nat.succ m * n)) = (bodd -[m+1] && bodd ↑n)
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_mul]
  -- Porting note: Heavily refactored proof, used to be:
  -- `by cases m with m m; cases n with n n;`
  -- `simp [← int.mul_def, int.mul, -of_nat_eq_coe, bool.bxor_comm]`
[GOAL]
case negSucc.negSucc
m n : ℕ
⊢ bodd ↑(Nat.succ m * Nat.succ n) = (bodd -[m+1] && bodd -[n+1])
[PROOFSTEP]
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_mul]
  -- Porting note: Heavily refactored proof, used to be:
  -- `by cases m with m m; cases n with n n;`
  -- `simp [← int.mul_def, int.mul, -of_nat_eq_coe, bool.bxor_comm]`
[GOAL]
n : ℕ
⊢ (bif bodd ↑n then 1 else 0) + 2 * div2 ↑n = ↑n
[PROOFSTEP]
rw [show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl]
[GOAL]
n : ℕ
⊢ (bif bodd ↑n then 1 else 0) = ↑(bif bodd ↑n then 1 else 0)
[PROOFSTEP]
cases bodd n
[GOAL]
case false
n : ℕ
⊢ (bif false then 1 else 0) = ↑(bif false then 1 else 0)
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
⊢ (bif true then 1 else 0) = ↑(bif true then 1 else 0)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ ↑(bif bodd ↑n then 1 else 0) + 2 * div2 ↑n = ↑n
[PROOFSTEP]
exact congr_arg ofNat n.bodd_add_div2
[GOAL]
n : ℕ
⊢ (bif bodd -[n+1] then 1 else 0) + 2 * div2 -[n+1] = -[n+1]
[PROOFSTEP]
refine' Eq.trans _ (congr_arg negSucc n.bodd_add_div2)
[GOAL]
n : ℕ
⊢ (bif bodd -[n+1] then 1 else 0) + 2 * div2 -[n+1] = -[(bif Nat.bodd n then 1 else 0) + 2 * Nat.div2 n+1]
[PROOFSTEP]
dsimp [bodd]
[GOAL]
n : ℕ
⊢ (bif !Nat.bodd n then 1 else 0) + 2 * div2 -[n+1] = -[(bif Nat.bodd n then 1 else 0) + 2 * Nat.div2 n+1]
[PROOFSTEP]
cases Nat.bodd n
[GOAL]
case false
n : ℕ
⊢ (bif !false then 1 else 0) + 2 * div2 -[n+1] = -[(bif false then 1 else 0) + 2 * Nat.div2 n+1]
[PROOFSTEP]
dsimp [cond, not, div2, Int.mul]
[GOAL]
case true
n : ℕ
⊢ (bif !true then 1 else 0) + 2 * div2 -[n+1] = -[(bif true then 1 else 0) + 2 * Nat.div2 n+1]
[PROOFSTEP]
dsimp [cond, not, div2, Int.mul]
[GOAL]
case false
n : ℕ
⊢ 1 + 2 * -[Nat.div2 n+1] = -[0 + 2 * Nat.div2 n+1]
[PROOFSTEP]
change -[2 * Nat.div2 n+1] = _
[GOAL]
case false
n : ℕ
⊢ -[2 * Nat.div2 n+1] = -[0 + 2 * Nat.div2 n+1]
[PROOFSTEP]
rw [zero_add]
[GOAL]
case true
n : ℕ
⊢ 0 + 2 * -[Nat.div2 n+1] = -[1 + 2 * Nat.div2 n+1]
[PROOFSTEP]
rw [zero_add, add_comm]
[GOAL]
case true
n : ℕ
⊢ 2 * -[Nat.div2 n+1] = -[2 * Nat.div2 n + 1+1]
[PROOFSTEP]
rfl
[GOAL]
b : Bool
n : ℤ
⊢ bit b n = 2 * n + bif b then 1 else 0
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℤ
⊢ bit false n = 2 * n + bif false then 1 else 0
case true n : ℤ ⊢ bit true n = 2 * n + bif true then 1 else 0
[PROOFSTEP]
apply (bit0_val n).trans (add_zero _).symm
[GOAL]
case true
n : ℤ
⊢ bit true n = 2 * n + bif true then 1 else 0
[PROOFSTEP]
apply bit1_val
[GOAL]
C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C n
[PROOFSTEP]
rw [← bit_decomp n]
[GOAL]
C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C (bit (bodd n) (div2 n))
[PROOFSTEP]
apply h
[GOAL]
b : Bool
n : ℕ
⊢ bit b ↑n = ↑(Nat.bit b n)
[PROOFSTEP]
rw [bit_val, Nat.bit_val]
[GOAL]
b : Bool
n : ℕ
⊢ (2 * ↑n + bif b then 1 else 0) = ↑(2 * n + bif b then 1 else 0)
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ (2 * ↑n + bif false then 1 else 0) = ↑(2 * n + bif false then 1 else 0)
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
⊢ (2 * ↑n + bif true then 1 else 0) = ↑(2 * n + bif true then 1 else 0)
[PROOFSTEP]
rfl
[GOAL]
b : Bool
n : ℕ
⊢ bit b -[n+1] = -[Nat.bit (!b) n+1]
[PROOFSTEP]
rw [bit_val, Nat.bit_val]
[GOAL]
b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + bif !b then 1 else 0+1]
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ (2 * -[n+1] + bif false then 1 else 0) = -[2 * n + bif !false then 1 else 0+1]
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
⊢ (2 * -[n+1] + bif true then 1 else 0) = -[2 * n + bif !true then 1 else 0+1]
[PROOFSTEP]
rfl
[GOAL]
b : Bool
n : ℤ
⊢ bodd (bit b n) = b
[PROOFSTEP]
rw [bit_val]
[GOAL]
b : Bool
n : ℤ
⊢ bodd (2 * n + bif b then 1 else 0) = b
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℤ
⊢ bodd (2 * n + bif false then 1 else 0) = false
[PROOFSTEP]
cases bodd n
[GOAL]
case true
n : ℤ
⊢ bodd (2 * n + bif true then 1 else 0) = true
[PROOFSTEP]
cases bodd n
[GOAL]
case false.false
n : ℤ
⊢ bodd (2 * n + bif false then 1 else 0) = false
[PROOFSTEP]
simp
[GOAL]
case false.true
n : ℤ
⊢ bodd (2 * n + bif false then 1 else 0) = false
[PROOFSTEP]
simp
[GOAL]
case true.false
n : ℤ
⊢ bodd (2 * n + bif true then 1 else 0) = true
[PROOFSTEP]
simp
[GOAL]
case true.true
n : ℤ
⊢ bodd (2 * n + bif true then 1 else 0) = true
[PROOFSTEP]
simp
[GOAL]
m n : ℤ
⊢ ¬bodd (bit0 m) = bodd (bit1 n)
[PROOFSTEP]
simp
[GOAL]
m : ℤ
⊢ bit1 m ≠ 0
[PROOFSTEP]
simpa only [bit0_zero] using bit1_ne_bit0 m 0
[GOAL]
b : Bool
n : ℕ
⊢ testBit (bit b ↑n) 0 = b
[PROOFSTEP]
rw [bit_coe_nat]
[GOAL]
b : Bool
n : ℕ
⊢ testBit (↑(Nat.bit b n)) 0 = b
[PROOFSTEP]
apply Nat.testBit_zero
[GOAL]
b : Bool
n : ℕ
⊢ testBit (bit b -[n+1]) 0 = b
[PROOFSTEP]
rw [bit_negSucc]
[GOAL]
b : Bool
n : ℕ
⊢ testBit -[Nat.bit (!b) n+1] 0 = b
[PROOFSTEP]
dsimp [testBit]
[GOAL]
b : Bool
n : ℕ
⊢ (!Nat.testBit (Nat.bit (!b) n) 0) = b
[PROOFSTEP]
rw [Nat.testBit_zero]
[GOAL]
b : Bool
n : ℕ
⊢ (!!b) = b
[PROOFSTEP]
clear testBit_zero
[GOAL]
b : Bool
n : ℕ
⊢ (!!b) = b
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ (!!false) = false
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
⊢ (!!true) = true
[PROOFSTEP]
rfl
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ testBit (bit b ↑n) (Nat.succ m) = testBit (↑n) m
[PROOFSTEP]
rw [bit_coe_nat]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ testBit (↑(Nat.bit b n)) (Nat.succ m) = testBit (↑n) m
[PROOFSTEP]
apply Nat.testBit_succ
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ testBit (bit b -[n+1]) (Nat.succ m) = testBit -[n+1] m
[PROOFSTEP]
dsimp [testBit]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ (match bit b -[n+1], Nat.succ m with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    !Nat.testBit n m
[PROOFSTEP]
simp only [bit_negSucc]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ (!Nat.testBit (Nat.bit (!b) n) (Nat.succ m)) = !Nat.testBit n m
[PROOFSTEP]
cases b
[GOAL]
case false
m n : ℕ
⊢ (!Nat.testBit (Nat.bit (!false) n) (Nat.succ m)) = !Nat.testBit n m
[PROOFSTEP]
simp [Nat.testBit_succ]
[GOAL]
case true
m n : ℕ
⊢ (!Nat.testBit (Nat.bit (!true) n) (Nat.succ m)) = !Nat.testBit n m
[PROOFSTEP]
simp [Nat.testBit_succ]
[GOAL]
⊢ bitwise or = lor
[PROOFSTEP]
funext m n
[GOAL]
case h.h
m n : ℤ
⊢ bitwise or m n = lor m n
[PROOFSTEP]
cases' m with m m
[GOAL]
case h.h.ofNat
n : ℤ
m : ℕ
⊢ bitwise or (ofNat m) n = lor (ofNat m) n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.negSucc
n : ℤ
m : ℕ
⊢ bitwise or -[m+1] n = lor -[m+1] n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = lor (ofNat m) (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = lor (ofNat m) (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = lor (ofNat m) (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = lor (ofNat m) -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = lor (ofNat m) -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = lor (ofNat m) -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = lor -[m+1] (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = lor -[m+1] (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = lor -[m+1] (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = lor -[m+1] -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = lor -[m+1] -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = lor -[m+1] -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = lor (ofNat m) -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff', negSucc.injEq, Bool.true_or,
  Nat.land']
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = lor -[m+1] (ofNat n)
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff', negSucc.injEq, Bool.true_or,
  Nat.land']
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = lor -[m+1] -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff', negSucc.injEq, Bool.true_or,
  Nat.land']
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(x || !y)) m n = Nat.bitwise' (fun a b => a && !b) n m
[PROOFSTEP]
rw [Nat.bitwise'_swap, Function.swap]
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun y x => !(x || !y)) n m = Nat.bitwise' (fun a b => a && !b) n m
case h.h.ofNat.negSucc m n : ℕ ⊢ (!(false || !false)) = false
[PROOFSTEP]
congr
[GOAL]
case h.h.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun y x => !(x || !y)) = fun a b => a && !b
case h.h.ofNat.negSucc m n : ℕ ⊢ (!(false || !false)) = false
[PROOFSTEP]
funext x y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(y || !x)) = (x && !y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!(y || !false)) = (false && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!(y || !true)) = (true && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false.false
m n : ℕ
⊢ (!(false || !false)) = (false && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false.true
m n : ℕ
⊢ (!(true || !false)) = (false && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true.false
m n : ℕ
⊢ (!(false || !true)) = (true && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true.true
m n : ℕ
⊢ (!(true || !true)) = (true && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ (!(false || !false)) = false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x || y)) m n = Nat.bitwise' (fun a b => a && !b) m n
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x || y)) = fun a b => a && !b
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x || y)) = (x && !y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!(!false || y)) = (false && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!(!true || y)) = (true && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.false
m n : ℕ
⊢ (!(!false || false)) = (false && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.true
m n : ℕ
⊢ (!(!false || true)) = (false && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.false
m n : ℕ
⊢ (!(!true || false)) = (true && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.true
m n : ℕ
⊢ (!(!true || true)) = (true && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x || !y)) m n = Nat.bitwise' and m n
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.negSucc.e_f
m n : ℕ
⊢ (fun x y => !(!x || !y)) = and
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x || !y)) = (x && y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!(!false || !y)) = (false && y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!(!true || !y)) = (true && y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.false.false
m n : ℕ
⊢ (!(!false || !false)) = (false && false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.false.true
m n : ℕ
⊢ (!(!false || !true)) = (false && true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.true.false
m n : ℕ
⊢ (!(!true || !false)) = (true && false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_f.h.h.true.true
m n : ℕ
⊢ (!(!true || !true)) = (true && true)
[PROOFSTEP]
rfl
[GOAL]
⊢ bitwise and = land
[PROOFSTEP]
funext m n
[GOAL]
case h.h
m n : ℤ
⊢ bitwise and m n = land m n
[PROOFSTEP]
cases' m with m m
[GOAL]
case h.h.ofNat
n : ℤ
m : ℕ
⊢ bitwise and (ofNat m) n = land (ofNat m) n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.negSucc
n : ℤ
m : ℕ
⊢ bitwise and -[m+1] n = land -[m+1] n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = land (ofNat m) (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = land (ofNat m) (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = land (ofNat m) (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = land (ofNat m) -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = land (ofNat m) -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = land (ofNat m) -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = land -[m+1] (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = land -[m+1] (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = land -[m+1] (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = land -[m+1] -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = land -[m+1] -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = land -[m+1] -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = land -[m+1] (ofNat n)
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.and_false, Nat.land']
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = land -[m+1] -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.and_false, Nat.land']
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => !x && y) m n) = land -[m+1] (ofNat n)
[PROOFSTEP]
rw [Nat.bitwise'_swap, Function.swap]
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise' (fun y x => !x && y) n m) = land -[m+1] (ofNat n)
case h.h.negSucc.ofNat m n : ℕ ⊢ (!false && false) = false
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f
m n : ℕ
⊢ (fun y x => !x && y) = fun a b => a && !b
case h.h.negSucc.ofNat m n : ℕ ⊢ (!false && false) = false
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!y && x) = (x && !y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!y && false) = (false && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!y && true) = (true && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.false.false
m n : ℕ
⊢ (!false && false) = (false && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.false.true
m n : ℕ
⊢ (!true && false) = (false && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.true.false
m n : ℕ
⊢ (!false && true) = (true && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_a.e_f.h.h.true.true
m n : ℕ
⊢ (!true && true) = (true && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ (!false && false) = false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise' (fun x y => !(!x && !y)) m n+1] = land -[m+1] -[n+1]
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!(!false && !y)) = (false || y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!(!true && !y)) = (true || y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.false
m n : ℕ
⊢ (!(!false && !false)) = (false || false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.true
m n : ℕ
⊢ (!(!false && !true)) = (false || true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.false
m n : ℕ
⊢ (!(!true && !false)) = (true || false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.true
m n : ℕ
⊢ (!(!true && !true)) = (true || true)
[PROOFSTEP]
rfl
[GOAL]
⊢ (bitwise fun a b => a && !b) = ldiff'
[PROOFSTEP]
funext m n
[GOAL]
case h.h
m n : ℤ
⊢ bitwise (fun a b => a && !b) m n = ldiff' m n
[PROOFSTEP]
cases' m with m m
[GOAL]
case h.h.ofNat
n : ℤ
m : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) n = ldiff' (ofNat m) n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.negSucc
n : ℤ
m : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] n = ldiff' -[m+1] n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) (ofNat n) = ldiff' (ofNat m) (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) (ofNat n) = ldiff' (ofNat m) (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) (ofNat n) = ldiff' (ofNat m) (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) -[n+1] = ldiff' (ofNat m) -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) -[n+1] = ldiff' (ofNat m) -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) -[n+1] = ldiff' (ofNat m) -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] (ofNat n) = ldiff' -[m+1] (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] (ofNat n) = ldiff' -[m+1] (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] (ofNat n) = ldiff' -[m+1] (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] -[n+1] = ldiff' -[m+1] -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] -[n+1] = ldiff' -[m+1] -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] -[n+1] = ldiff' -[m+1] -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) -[n+1] = ldiff' (ofNat m) -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor']
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] (ofNat n) = ldiff' -[m+1] (ofNat n)
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor']
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b => a && !b) -[m+1] -[n+1] = ldiff' -[m+1] -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor']
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => x && !!y) m n) = ↑(Nat.bitwise' and m n)
[PROOFSTEP]
congr
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => x && !!y) = and
[PROOFSTEP]
funext x y
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (x && !!y) = (x && y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (false && !!y) = (false && y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (true && !!y) = (true && y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.false.false
m n : ℕ
⊢ (false && !!false) = (false && false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.false.true
m n : ℕ
⊢ (false && !!true) = (false && true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.true.false
m n : ℕ
⊢ (true && !!false) = (true && false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_a.e_f.h.h.true.true
m n : ℕ
⊢ (true && !!true) = (true && true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x && !y)) m n = Nat.bitwise' or m n
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!(!false && !y)) = (false || y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!(!true && !y)) = (true || y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.false
m n : ℕ
⊢ (!(!false && !false)) = (false || false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.true
m n : ℕ
⊢ (!(!false && !true)) = (false || true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.false
m n : ℕ
⊢ (!(!true && !false)) = (true || false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.true
m n : ℕ
⊢ (!(!true && !true)) = (true || true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => !x && !!y) m n) = ↑(Nat.bitwise' (fun a b => a && !b) n m)
[PROOFSTEP]
rw [Nat.bitwise'_swap, Function.swap]
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun y x => !x && !!y) n m) = ↑(Nat.bitwise' (fun a b => a && !b) n m)
case h.h.negSucc.negSucc m n : ℕ ⊢ (!false && !!false) = false
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun y x => !x && !!y) = fun a b => a && !b
case h.h.negSucc.negSucc m n : ℕ ⊢ (!false && !!false) = false
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!y && !!x) = (x && !y)
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!y && !!false) = (false && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!y && !!true) = (true && !y)
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.false
m n : ℕ
⊢ (!false && !!false) = (false && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.true
m n : ℕ
⊢ (!true && !!false) = (false && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.false
m n : ℕ
⊢ (!false && !!true) = (true && !false)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.true
m n : ℕ
⊢ (!true && !!true) = (true && !true)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ (!false && !!false) = false
[PROOFSTEP]
rfl
[GOAL]
⊢ bitwise xor = lxor'
[PROOFSTEP]
funext m n
[GOAL]
case h.h
m n : ℤ
⊢ bitwise xor m n = lxor' m n
[PROOFSTEP]
cases' m with m m
[GOAL]
case h.h.ofNat
n : ℤ
m : ℕ
⊢ bitwise xor (ofNat m) n = lxor' (ofNat m) n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.negSucc
n : ℤ
m : ℕ
⊢ bitwise xor -[m+1] n = lxor' -[m+1] n
[PROOFSTEP]
cases' n with n n
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = lxor' (ofNat m) (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = lxor' (ofNat m) (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = lxor' (ofNat m) (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = lxor' (ofNat m) -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = lxor' (ofNat m) -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = lxor' (ofNat m) -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = lxor' -[m+1] (ofNat n)
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = lxor' -[m+1] (ofNat n)
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = lxor' -[m+1] (ofNat n)
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = lxor' -[m+1] -[n+1]
[PROOFSTEP]
try {rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = lxor' -[m+1] -[n+1]
[PROOFSTEP]
{rfl
}
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = lxor' -[m+1] -[n+1]
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = lxor' (ofNat m) -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.false_xor, Bool.true_xor, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor', lxor',
  Nat.lxor']
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = lxor' -[m+1] (ofNat n)
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.false_xor, Bool.true_xor, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor', lxor',
  Nat.lxor']
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = lxor' -[m+1] -[n+1]
[PROOFSTEP]
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_false, cond_true, lor, Nat.ldiff', Bool.and_true,
  negSucc.injEq, Bool.false_xor, Bool.true_xor, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor', lxor',
  Nat.lxor']
[GOAL]
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor x !y) m n = Nat.bitwise' xor m n
[PROOFSTEP]
congr
[GOAL]
case h.h.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun x y => !xor x !y) = xor
[PROOFSTEP]
funext x y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!xor x !y) = xor x y
[PROOFSTEP]
cases x
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!xor false !y) = xor false y
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!xor true !y) = xor true y
[PROOFSTEP]
cases y
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false.false
m n : ℕ
⊢ (!xor false !false) = xor false false
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.false.true
m n : ℕ
⊢ (!xor false !true) = xor false true
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true.false
m n : ℕ
⊢ (!xor true !false) = xor true false
[PROOFSTEP]
rfl
[GOAL]
case h.h.ofNat.negSucc.e_f.h.h.true.true
m n : ℕ
⊢ (!xor true !true) = xor true true
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor (!x) y) m n = Nat.bitwise' xor m n
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !xor (!x) y) = xor
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!xor (!x) y) = xor x y
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (!xor (!false) y) = xor false y
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (!xor (!true) y) = xor true y
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.false
m n : ℕ
⊢ (!xor (!false) false) = xor false false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.false.true
m n : ℕ
⊢ (!xor (!false) true) = xor false true
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.false
m n : ℕ
⊢ (!xor (!true) false) = xor true false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.ofNat.e_f.h.h.true.true
m n : ℕ
⊢ (!xor (!true) true) = xor true true
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => xor (!x) !y) m n) = ↑(Nat.bitwise' xor m n)
[PROOFSTEP]
congr
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => xor (!x) !y) = xor
[PROOFSTEP]
funext x y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (xor (!x) !y) = xor x y
[PROOFSTEP]
cases x
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false
m n : ℕ
y : Bool
⊢ (xor (!false) !y) = xor false y
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true
m n : ℕ
y : Bool
⊢ (xor (!true) !y) = xor true y
[PROOFSTEP]
cases y
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.false
m n : ℕ
⊢ (xor (!false) !false) = xor false false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.false.true
m n : ℕ
⊢ (xor (!false) !true) = xor false true
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.false
m n : ℕ
⊢ (xor (!true) !false) = xor true false
[PROOFSTEP]
rfl
[GOAL]
case h.h.negSucc.negSucc.e_a.e_f.h.h.true.true
m n : ℕ
⊢ (xor (!true) !true) = xor true true
[PROOFSTEP]
rfl
[GOAL]
f : Bool → Bool → Bool
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)
[PROOFSTEP]
cases' m with m m
[GOAL]
case ofNat
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b n) = bit (f a b) (bitwise f (ofNat m) n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case negSucc
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b n) = bit (f a b) (bitwise f -[m+1] n)
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b (ofNat n)) = bit (f a b) (bitwise f (ofNat m) (ofNat n))
[PROOFSTEP]
simp only [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false', bit_negSucc]
[GOAL]
case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b -[n+1]) = bit (f a b) (bitwise f (ofNat m) -[n+1])
[PROOFSTEP]
simp only [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false', bit_negSucc]
[GOAL]
case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b (ofNat n)) = bit (f a b) (bitwise f -[m+1] (ofNat n))
[PROOFSTEP]
simp only [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false', bit_negSucc]
[GOAL]
case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b -[n+1]) = bit (f a b) (bitwise f -[m+1] -[n+1])
[PROOFSTEP]
simp only [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false', bit_negSucc]
[GOAL]
case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false false then -[Nat.bitwise' (fun x y => !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise' (fun x y => !f x y) m n+1] else ↑(Nat.bitwise' f m n))
[PROOFSTEP]
by_cases h : f false false
[GOAL]
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false false = true
⊢ (bif f false false then -[Nat.bitwise' (fun x y => !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise' (fun x y => !f x y) m n+1] else ↑(Nat.bitwise' f m n))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false false = true
⊢ (bif f false false then -[Nat.bitwise' (fun x y => !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise' (fun x y => !f x y) m n+1] else ↑(Nat.bitwise' f m n))
[PROOFSTEP]
simp [h]
[GOAL]
case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))
[PROOFSTEP]
by_cases h : f false true
[GOAL]
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false true = true
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false true = true
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))
[PROOFSTEP]
by_cases h : f true false
[GOAL]
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f true false = true
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f true false = true
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
[PROOFSTEP]
by_cases h : f true true
[GOAL]
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f true true = true
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f true true = true
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
[PROOFSTEP]
simp [h]
[GOAL]
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ lor (bit a m) (bit b n) = bit (a || b) (lor m n)
[PROOFSTEP]
rw [← bitwise_or, bitwise_bit]
[GOAL]
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ land (bit a m) (bit b n) = bit (a && b) (land m n)
[PROOFSTEP]
rw [← bitwise_and, bitwise_bit]
[GOAL]
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ ldiff' (bit a m) (bit b n) = bit (a && !b) (ldiff' m n)
[PROOFSTEP]
rw [← bitwise_diff, bitwise_bit]
[GOAL]
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ lxor' (bit a m) (bit b n) = bit (xor a b) (lxor' m n)
[PROOFSTEP]
rw [← bitwise_xor, bitwise_bit]
[GOAL]
b : Bool
n : ℕ
⊢ lnot (bit b ↑n) = bit (!b) (lnot ↑n)
[PROOFSTEP]
simp [lnot]
[GOAL]
b : Bool
n : ℕ
⊢ lnot (bit b -[n+1]) = bit (!b) (lnot -[n+1])
[PROOFSTEP]
simp [lnot]
[GOAL]
f : Bool → Bool → Bool
m n : ℤ
k : ℕ
⊢ testBit (bitwise f m n) k = f (testBit m k) (testBit n k)
[PROOFSTEP]
cases m
[GOAL]
case ofNat
f : Bool → Bool → Bool
n : ℤ
k a✝ : ℕ
⊢ testBit (bitwise f (ofNat a✝) n) k = f (testBit (ofNat a✝) k) (testBit n k)
[PROOFSTEP]
cases n
[GOAL]
case negSucc
f : Bool → Bool → Bool
n : ℤ
k a✝ : ℕ
⊢ testBit (bitwise f -[a✝+1] n) k = f (testBit -[a✝+1] k) (testBit n k)
[PROOFSTEP]
cases n
[GOAL]
case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ testBit (bitwise f (ofNat a✝¹) (ofNat a✝)) k = f (testBit (ofNat a✝¹) k) (testBit (ofNat a✝) k)
[PROOFSTEP]
simp only [testBit, bitwise, natBitwise]
[GOAL]
case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ testBit (bitwise f (ofNat a✝¹) -[a✝+1]) k = f (testBit (ofNat a✝¹) k) (testBit -[a✝+1] k)
[PROOFSTEP]
simp only [testBit, bitwise, natBitwise]
[GOAL]
case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ testBit (bitwise f -[a✝¹+1] (ofNat a✝)) k = f (testBit -[a✝¹+1] k) (testBit (ofNat a✝) k)
[PROOFSTEP]
simp only [testBit, bitwise, natBitwise]
[GOAL]
case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ testBit (bitwise f -[a✝¹+1] -[a✝+1]) k = f (testBit -[a✝¹+1] k) (testBit -[a✝+1] k)
[PROOFSTEP]
simp only [testBit, bitwise, natBitwise]
[GOAL]
case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match bif f false false then -[Nat.bitwise' (fun x y => !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise' f a✝¹ a✝), k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
by_cases h : f false false
[GOAL]
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false false = true
⊢ (match bif f false false then -[Nat.bitwise' (fun x y => !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise' f a✝¹ a✝), k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false false = true
⊢ (match bif f false false then -[Nat.bitwise' (fun x y => !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise' f a✝¹ a✝), k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
simp [h]
[GOAL]
case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f false !false then -[Nat.bitwise' (fun x y => !f x !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
by_cases h : f false true
[GOAL]
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false true = true
⊢ (match
      bif f false !false then -[Nat.bitwise' (fun x y => !f x !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false true = true
⊢ (match
      bif f false !false then -[Nat.bitwise' (fun x y => !f x !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
simp [h]
[GOAL]
case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) false then -[Nat.bitwise' (fun x y => !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
by_cases h : f true false
[GOAL]
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true false = true
⊢ (match
      bif f (!false) false then -[Nat.bitwise' (fun x y => !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true false = true
⊢ (match
      bif f (!false) false then -[Nat.bitwise' (fun x y => !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) (Nat.testBit a✝ k)
[PROOFSTEP]
simp [h]
[GOAL]
case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) !false then -[Nat.bitwise' (fun x y => !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
by_cases h : f true true
[GOAL]
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true true = true
⊢ (match
      bif f (!false) !false then -[Nat.bitwise' (fun x y => !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
simp [h]
[GOAL]
case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true true = true
⊢ (match
      bif f (!false) !false then -[Nat.bitwise' (fun x y => !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => Nat.testBit m n
    | -[m+1], n => !Nat.testBit m n) =
    f (!Nat.testBit a✝¹ k) !Nat.testBit a✝ k
[PROOFSTEP]
simp [h]
[GOAL]
m n : ℤ
k : ℕ
⊢ testBit (lor m n) k = (testBit m k || testBit n k)
[PROOFSTEP]
rw [← bitwise_or, testBit_bitwise]
[GOAL]
m n : ℤ
k : ℕ
⊢ testBit (land m n) k = (testBit m k && testBit n k)
[PROOFSTEP]
rw [← bitwise_and, testBit_bitwise]
[GOAL]
m n : ℤ
k : ℕ
⊢ testBit (ldiff' m n) k = (testBit m k && !testBit n k)
[PROOFSTEP]
rw [← bitwise_diff, testBit_bitwise]
[GOAL]
m n : ℤ
k : ℕ
⊢ testBit (lxor' m n) k = xor (testBit m k) (testBit n k)
[PROOFSTEP]
rw [← bitwise_xor, testBit_bitwise]
[GOAL]
n k : ℕ
⊢ testBit (lnot ↑n) k = !testBit (↑n) k
[PROOFSTEP]
simp [lnot, testBit]
[GOAL]
n k : ℕ
⊢ testBit (lnot -[n+1]) k = !testBit -[n+1] k
[PROOFSTEP]
simp [lnot, testBit]
[GOAL]
m n : ℤ
⊢ shiftr m (-n) = shiftl m n
[PROOFSTEP]
rw [← shiftl_neg, neg_neg]
[GOAL]
m n : ℕ
⊢ shiftr ↑m ↑n = ↑(Nat.shiftr m n)
[PROOFSTEP]
cases n
[GOAL]
case zero
m : ℕ
⊢ shiftr ↑m ↑Nat.zero = ↑(Nat.shiftr m Nat.zero)
[PROOFSTEP]
rfl
[GOAL]
case succ
m n✝ : ℕ
⊢ shiftr ↑m ↑(Nat.succ n✝) = ↑(Nat.shiftr m (Nat.succ n✝))
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
⊢ shiftr -[m+1] ↑n = -[Nat.shiftr m n+1]
[PROOFSTEP]
cases n
[GOAL]
case zero
m : ℕ
⊢ shiftr -[m+1] ↑Nat.zero = -[Nat.shiftr m Nat.zero+1]
[PROOFSTEP]
rfl
[GOAL]
case succ
m n✝ : ℕ
⊢ shiftr -[m+1] ↑(Nat.succ n✝) = -[Nat.shiftr m (Nat.succ n✝)+1]
[PROOFSTEP]
rfl
[GOAL]
m n k : ℕ
⊢ shiftr (↑m) (↑n + ↑k) = shiftr (shiftr ↑m ↑n) ↑k
[PROOFSTEP]
rw [shiftr_coe_nat, shiftr_coe_nat, ← Int.ofNat_add, shiftr_coe_nat, Nat.shiftr_add]
[GOAL]
m n k : ℕ
⊢ shiftr -[m+1] (↑n + ↑k) = shiftr (shiftr -[m+1] ↑n) ↑k
[PROOFSTEP]
rw [shiftr_negSucc, shiftr_negSucc, ← Int.ofNat_add, shiftr_negSucc, Nat.shiftr_add]
[GOAL]
m n✝ k i n : ℕ
⊢ (fun n k i => shiftl (↑m) i = ↑(Nat.shiftr (Nat.shiftl m n) k)) (n + i) n ↑i
[PROOFSTEP]
dsimp
[GOAL]
m n✝ k i n : ℕ
⊢ ↑(Nat.shiftl m i) = ↑(Nat.shiftr (Nat.shiftl m (n + i)) n)
[PROOFSTEP]
rw [← Nat.shiftl_sub, add_tsub_cancel_left]
[GOAL]
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
[PROOFSTEP]
apply Nat.le_add_right
[GOAL]
m n✝ k i n : ℕ
⊢ (fun n k i => shiftl (↑m) i = ↑(Nat.shiftr (Nat.shiftl m n) k)) n (n + i + 1) -[i+1]
[PROOFSTEP]
dsimp
[GOAL]
m n✝ k i n : ℕ
⊢ shiftl ↑m -[i+1] = ↑(Nat.shiftr (Nat.shiftl m n) (n + i + 1))
[PROOFSTEP]
rw [add_assoc, Nat.shiftr_add, ← Nat.shiftl_sub, tsub_self]
[GOAL]
m n✝ k i n : ℕ
⊢ shiftl ↑m -[i+1] = ↑(Nat.shiftr (Nat.shiftl m 0) (i + 1))
[PROOFSTEP]
rfl
[GOAL]
case a
m n✝ k i n : ℕ
⊢ n ≤ n
[PROOFSTEP]
rfl
[GOAL]
m n✝ k i n : ℕ
⊢ Nat.shiftl' true m i = Nat.shiftr (Nat.shiftl' true m (n + i)) n
[PROOFSTEP]
rw [← Nat.shiftl'_sub, add_tsub_cancel_left]
[GOAL]
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
[PROOFSTEP]
apply Nat.le_add_right
[GOAL]
m n✝ k i n : ℕ
⊢ Nat.shiftr m (Nat.succ i) = Nat.shiftr (Nat.shiftl' true m n) (n + i + 1)
[PROOFSTEP]
rw [add_assoc, Nat.shiftr_add, ← Nat.shiftl'_sub, tsub_self]
[GOAL]
m n✝ k i n : ℕ
⊢ Nat.shiftr m (Nat.succ i) = Nat.shiftr (Nat.shiftl' true m 0) (i + 1)
[PROOFSTEP]
rfl
[GOAL]
case a
m n✝ k i n : ℕ
⊢ n ≤ n
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
⊢ shiftr ↑m ↑n = ↑m / ↑(2 ^ n)
[PROOFSTEP]
rw [shiftr_coe_nat, Nat.shiftr_eq_div_pow _ _]
[GOAL]
m n : ℕ
⊢ ↑(m / 2 ^ n) = ↑m / ↑(2 ^ n)
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
⊢ shiftr -[m+1] ↑n = -[m+1] / ↑(2 ^ n)
[PROOFSTEP]
rw [shiftr_negSucc, negSucc_ediv, Nat.shiftr_eq_div_pow]
[GOAL]
m n : ℕ
⊢ -[m / 2 ^ n+1] = -(div ↑m ↑(2 ^ n) + 1)
case H m n : ℕ ⊢ 0 < ↑(2 ^ n)
[PROOFSTEP]
rfl
[GOAL]
case H
m n : ℕ
⊢ 0 < ↑(2 ^ n)
[PROOFSTEP]
exact ofNat_lt_ofNat_of_lt (pow_pos (by decide) _)
[GOAL]
m n : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide
