Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Apply mul_SNo_eq_2 with x0, 0, mul_SNo x0 0 = 0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H1: ∀ x3 . x3x1∀ x4 : ο . (∀ x5 . x5SNoL x0∀ x6 . x6SNoL 0x3 = add_SNo (mul_SNo x5 0) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x4)(∀ x5 . x5SNoR x0∀ x6 . x6SNoR 0x3 = add_SNo (mul_SNo x5 0) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x4)x4.
Assume H2: ∀ x3 . x3SNoL x0∀ x4 . x4SNoL 0add_SNo (mul_SNo x3 0) (add_SNo (mul_SNo x0 x4) (minus_SNo (mul_SNo x3 x4)))x1.
Assume H3: ∀ x3 . x3SNoR x0∀ x4 . x4SNoR 0add_SNo (mul_SNo x3 0) (add_SNo (mul_SNo x0 x4) (minus_SNo (mul_SNo x3 x4)))x1.
Assume H4: ∀ x3 . x3x2∀ x4 : ο . (∀ x5 . x5SNoL x0∀ x6 . x6SNoR 0x3 = add_SNo (mul_SNo x5 0) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x4)(∀ x5 . x5SNoR x0∀ x6 . x6SNoL 0x3 = add_SNo (mul_SNo x5 0) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x4)x4.
Assume H5: ∀ x3 . x3SNoL x0∀ x4 . x4SNoR 0add_SNo (mul_SNo x3 0) (add_SNo (mul_SNo x0 x4) (minus_SNo (mul_SNo x3 x4)))x2.
Assume H6: ∀ x3 . x3SNoR x0∀ x4 . x4SNoL 0add_SNo (mul_SNo x3 0) (add_SNo (mul_SNo x0 x4) (minus_SNo (mul_SNo x3 x4)))x2.
Assume H7: mul_SNo x0 0 = SNoCut x1 x2.
Apply H7 with λ x3 x4 . x4 = 0.
Claim L8: ...
...
Claim L9: x2 = 0
Apply Empty_Subq_eq with x2.
Let x3 of type ι be given.
Assume H9: x3x2.
Apply FalseE with x30.
Apply H4 with x3, False leaving 3 subgoals.
The subproof is completed by applying H9.
Let x4 of type ι be given.
Assume H10: x4SNoL x0.
Let x5 of type ι be given.
Apply SNoR_0 with λ x6 x7 . ...... = ...False.
...
...
Apply L8 with λ x3 x4 . SNoCut x4 x2 = 0.
Apply L9 with λ x3 x4 . SNoCut 0 x4 = 0.
The subproof is completed by applying SNoCut_0_0.