Search for blocks/addresses/...

Proofgold Proof

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