Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Claim L2: ...
...
set y2 to be ...
Claim L3: ∀ x3 : ι → ο . x3 y2 ⟶ x3 ((λ x4 . mul_SNo x4 x4) (add_SNo x0 x1))
Let x3 of type ι → ο be given.
Assume H3: x3 (add_SNo ((λ x4 . mul_SNo x4 x4) x1) (add_SNo (mul_SNo 2 (mul_SNo x1 y2)) ((λ x4 . mul_SNo x4 x4) y2))).
Apply SNo_foil with x1, y2, x1, y2, λ x4 . x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
set y4 to be ...
Claim L4: ∀ x5 : ι → ο . x5 y4 ⟶ x5 (add_SNo ((λ x6 . mul_SNo x6 x6) x1) (add_SNo (mul_SNo x1 y2) (add_SNo (mul_SNo y2 x1) (mul_SNo y2 y2))))
Let x5 of type ι → ο be given.
Apply mul_SNo_com with x3, y2, λ x6 x7 . add_SNo (mul_SNo y2 x3) (add_SNo x7 ((λ x8 . mul_SNo x8 x8) x3)) = add_SNo (mul_SNo 2 (mul_SNo y2 x3)) ((λ x8 . mul_SNo x8 x8) x3), λ x6 x7 . (λ x8 . x5) (add_SNo ((λ x8 . mul_SNo x8 x8) y2) x6) (add_SNo ((λ x8 . mul_SNo x8 x8) y2) x7) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
set y6 to be ...
Claim L4: ∀ x7 : ι → ο . x7 y6 ⟶ x7 (add_SNo (mul_SNo y2 x3) (add_SNo (mul_SNo y2 x3) ((λ x8 . mul_SNo x8 x8) x3)))
Let x7 of type ι → ο be given.
Assume H4: x7 (add_SNo (mul_SNo 2 (mul_SNo x3 y4)) ((λ x8 . mul_SNo x8 x8) y4)).
Apply add_SNo_assoc with mul_SNo x3 y4, mul_SNo x3 y4, (λ x8 . mul_SNo x8 x8) y4, λ x8 . x7 leaving 4 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L2.
Apply SNo_mul_SNo with y4, y4 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
set y8 to be add_SNo (mul_SNo 2 ...) ...
Claim L5: ∀ x9 : ι → ο . x9 y8 ⟶ x9 (add_SNo (add_SNo (mul_SNo x3 y4) (mul_SNo x3 y4)) ((λ x10 . mul_SNo x10 x10) y4))
Let x9 of type ι → ο be given.
Apply unknownprop_e5d031cf873471b22fe77dee36ebb6254dbd5df83fe741afd4ca8450323be464 with mul_SNo y4 x5, λ x10 x11 . (λ x12 x13 . (λ x14 . x9) (add_SNo x12 ((λ x14 . mul_SNo x14 x14) x5)) (add_SNo x13 ((λ x14 . mul_SNo x14 x14) x5))) x11 x10.
The subproof is completed by applying L2.
set y9 to be λ x9 . y8
Apply L5 with λ x10 . y9 x10 y8 ⟶ y9 y8 x10 leaving 2 subgoals.
Assume H6: y9 y8 y8.
The subproof is completed by applying H6.
The subproof is completed by applying L5.
Let x7 of type ι → ι → ο be given.
Apply L4 with λ x8 . x7 x8 y6 ⟶ x7 y6 x8.
Assume H5: x7 y6 y6.
The subproof is completed by applying H5.
set y5 to be λ x5 . y4
Apply L4 with λ x6 . y5 x6 y4 ⟶ y5 y4 x6 leaving 2 subgoals.
Assume H5: y5 y4 y4.
The subproof is completed by applying H5.
The subproof is completed by applying L4.
Let x3 of type ι → ι → ο be given.
Apply L3 with λ x4 . x3 x4 y2 ⟶ x3 y2 x4.
Assume H4: x3 y2 y2.
The subproof is completed by applying H4.
■