Search for blocks/addresses/...

Proofgold Proof

pf
Apply SNoLev_ind2 with λ x0 x1 . mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1).
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: ∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ mul_SNo (minus_SNo x2) x1 = minus_SNo (mul_SNo x2 x1).
Assume H3: ∀ x2 . x2 ∈ SNoS_ (SNoLev x1) ⟶ mul_SNo (minus_SNo x0) x2 = minus_SNo (mul_SNo x0 x2).
Assume H4: ∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x3 . x3 ∈ SNoS_ (SNoLev x1) ⟶ mul_SNo (minus_SNo x2) x3 = minus_SNo (mul_SNo x2 x3).
Claim L5: ...
...
Apply mul_SNo_eq_3 with x0, x1, mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H6: SNoCutP x2 x3.
Assume H7: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 : ο . (∀ x6 . x6 ∈ SNoL x0 ⟶ ∀ x7 . x7 ∈ SNoL x1 ⟶ x4 = add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ⟶ x5) ⟶ (∀ x6 . x6 ∈ SNoR x0 ⟶ ∀ x7 . x7 ∈ SNoR x1 ⟶ x4 = add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ⟶ x5) ⟶ x5.
Assume H8: ∀ x4 . x4 ∈ SNoL x0 ⟶ ∀ x5 . x5 ∈ SNoL x1 ⟶ add_SNo (mul_SNo x4 x1) (add_SNo (mul_SNo x0 x5) (minus_SNo (mul_SNo x4 x5))) ∈ x2.
Assume H9: ∀ x4 . x4 ∈ SNoR x0 ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ add_SNo (mul_SNo x4 x1) (add_SNo (mul_SNo x0 x5) (minus_SNo (mul_SNo x4 x5))) ∈ x2.
Assume H10: ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 : ο . (∀ x6 . x6 ∈ SNoL x0 ⟶ ∀ x7 . x7 ∈ SNoR x1 ⟶ x4 = add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ⟶ x5) ⟶ (∀ x6 . x6 ∈ SNoR x0 ⟶ ∀ x7 . x7 ∈ SNoL x1 ⟶ x4 = add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ⟶ x5) ⟶ x5.
Assume H11: ∀ x4 . ... ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ add_SNo (mul_SNo x4 x1) (add_SNo (mul_SNo x0 x5) (minus_SNo (mul_SNo x4 x5))) ∈ x3.
...
■