Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: CSNo x0.
Claim L1: ...
...
Claim L2: ...
...
Apply CSNo_ReIm_split with mul_CSNo 1 x0, x0 leaving 4 subgoals.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with 1, x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_33594f786441fb94cfa9c7be2034d88216fac0dbcbe9e223f18185e2cf6cb053.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
set y1 to be ...
Claim L3: ∀ x2 : ι → ο . x2 y1 ⟶ x2 (CSNo_Re (mul_CSNo 1 x0))
Let x2 of type ι → ο be given.
Assume H3: x2 (CSNo_Re y1).
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with 1, y1, λ x3 . x2 leaving 3 subgoals.
The subproof is completed by applying unknownprop_33594f786441fb94cfa9c7be2034d88216fac0dbcbe9e223f18185e2cf6cb053.
The subproof is completed by applying H0.
set y3 to be ...
Claim L4: ∀ x4 : ι → ο . x4 y3 ⟶ x4 (add_SNo (mul_SNo (CSNo_Re 1) (CSNo_Re y1)) (minus_SNo (mul_SNo (CSNo_Im 1) (CSNo_Im y1))))
Let x4 of type ι → ο be given.
Assume H4: x4 (add_SNo (CSNo_Re x2) 0).
Apply SNo_pair_0 with 1, λ x5 x6 . mul_SNo (CSNo_Re x5) (CSNo_Re x2) = CSNo_Re x2, λ x5 x6 . (λ x7 . x4) (add_SNo x5 (minus_SNo (mul_SNo (CSNo_Im 1) (CSNo_Im x2)))) (add_SNo x6 (minus_SNo (mul_SNo (CSNo_Im 1) (CSNo_Im x2)))) leaving 2 subgoals.
Apply CSNo_Re2 with 1, 0, λ x5 x6 . mul_SNo x6 (CSNo_Re x2) = CSNo_Re x2 leaving 3 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_0.
Apply mul_SNo_oneL with CSNo_Re x2.
The subproof is completed by applying L1.
Apply minus_SNo_0 with λ x5 x6 . minus_SNo (mul_SNo (CSNo_Im 1) (CSNo_Im x2)) = x5, λ x5 x6 . (λ x7 . x4) (add_SNo (CSNo_Re x2) x5) (add_SNo (CSNo_Re x2) x6) leaving 2 subgoals.
set y5 to be ...
Claim L5: ∀ x6 : ι → ο . x6 y5 ⟶ x6 (minus_SNo (mul_SNo (CSNo_Im 1) (CSNo_Im x2)))
Let x6 of type ι → ο be given.
Apply SNo_pair_0 with 1, λ x7 x8 . mul_SNo (CSNo_Im x7) (CSNo_Im y3) = 0, λ x7 x8 . (λ x9 . x6) (minus_SNo x7) (minus_SNo x8).
Let x7 of type ι → ι → ο be given.
set y8 to be ...
Claim L5: ...
...
set y9 to be ...
Claim L6: ∀ x10 : ι → ο . x10 y9 ⟶ x10 (mul_SNo (CSNo_Im (SNo_pair 1 0)) (CSNo_Im y3))
Let x10 of type ι → ο be given.
Apply CSNo_Im2 with 1, 0, λ x11 x12 . (λ x13 . x10) (mul_SNo x11 (CSNo_Im ...)) ... leaving 2 subgoals.
...
...
set y10 to be λ x10 . y9
Apply L6 with λ x11 . y10 x11 y9 ⟶ y10 y9 x11 leaving 2 subgoals.
Assume H7: y10 y9 y9.
The subproof is completed by applying H7.
Apply mul_SNo_zeroL with CSNo_Im y5, λ x11 . y10 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L6.
Let x6 of type ι → ι → ο be given.
Apply L5 with λ x7 . x6 x7 y5 ⟶ x6 y5 x7.
Assume H6: x6 y5 y5.
The subproof is completed by applying H6.
...
set y4 to be λ x4 . y3
Apply L4 with λ x5 . y4 x5 y3 ⟶ y4 y3 x5 leaving 2 subgoals.
Assume H5: y4 y3 y3.
The subproof is completed by applying H5.
set y5 to be CSNo_Re y3
Claim L5: ∀ x6 : ι → ο . x6 y5 ⟶ x6 (add_SNo (CSNo_Re y3) 0)
Let x6 of type ι → ο be given.
Assume H5: x6 (CSNo_Re y4).
Apply add_SNo_com with CSNo_Re y4, 0, λ x7 . x6 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying SNo_0.
Apply add_SNo_0L with CSNo_Re y4, λ x7 . x6 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H5.
set y6 to be λ x6 . y5
Apply L5 with λ x7 . y6 x7 y5 ⟶ y6 y5 x7 leaving 2 subgoals.
Assume H6: y6 y5 y5.
The subproof is completed by applying H6.
The subproof is completed by applying L5.
Let x2 of type ι → ι → ο be given.
Apply L3 with λ x3 . x2 x3 y1 ⟶ x2 y1 x3.
Assume H4: x2 y1 y1.
The subproof is completed by applying H4.
...
■