Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: CSNo x0.
Assume H1: CSNo x1.
Assume H2: CSNo x2.
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply CSNo_ReIm_split with mul_CSNo x0 (add_CSNo x1 x2), add_CSNo (mul_CSNo x0 x1) (mul_CSNo x0 x2) leaving 4 subgoals.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with x0, add_CSNo x1 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply CSNo_add_CSNo with mul_CSNo x0 x1, mul_CSNo x0 x2 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
set y3 to be ...
Claim L12: ∀ x4 : ι → ο . x4 y3x4 (CSNo_Re (mul_CSNo x0 (add_CSNo x1 x2)))
Let x4 of type ιο be given.
Assume H12: x4 (CSNo_Re (add_CSNo (mul_CSNo x1 x2) (mul_CSNo x1 y3))).
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with x1, add_CSNo x2 y3, λ x5 . x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
set y5 to be ...
Claim L13: ...
...
set y6 to be ...
Apply L13 with λ x7 . y6 x7 y5y6 y5 x7 leaving 2 subgoals.
Assume H14: y6 y5 y5.
The subproof is completed by applying H14.
Apply add_SNo_com_4_inner_mid with mul_SNo (CSNo_Re y3) (CSNo_Re x4), mul_SNo (CSNo_Re y3) (CSNo_Re y5), minus_SNo (mul_SNo (CSNo_Im y3) (CSNo_Im x4)), minus_SNo (mul_SNo (CSNo_Im y3) (CSNo_Im y5)), λ x7 . y6 leaving 5 subgoals.
Apply SNo_mul_SNo with CSNo_Re y3, CSNo_Re x4 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L8.
Apply SNo_mul_SNo with CSNo_Re y3, CSNo_Re y5 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L9.
Apply SNo_minus_SNo with mul_SNo (CSNo_Im y3) (CSNo_Im x4).
Apply SNo_mul_SNo with CSNo_Im y3, CSNo_Im x4 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L11.
Apply SNo_minus_SNo with mul_SNo (CSNo_Im y3) (CSNo_Im y5).
Apply SNo_mul_SNo with CSNo_Im y3, CSNo_Im y5 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying H12.
set y7 to be ...
Claim L14: ∀ x8 : ι → ο . x8 y7x8 (add_SNo (add_SNo (mul_SNo (CSNo_Re y3) (CSNo_Re x4)) (minus_SNo (mul_SNo (CSNo_Im y3) (CSNo_Im x4)))) (add_SNo (mul_SNo (CSNo_Re y3) (CSNo_Re y5)) (minus_SNo (mul_SNo (CSNo_Im y3) (CSNo_Im y5)))))
Let x8 of type ιο be given.
Assume H14: x8 (add_SNo (CSNo_Re (mul_CSNo x4 y5)) (CSNo_Re (mul_CSNo x4 y6))).
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with x4, y5, λ x9 x10 . (λ x11 x12 . (λ x13 . x8) (add_SNo x11 (add_SNo (mul_SNo (CSNo_Re x4) (CSNo_Re y6)) (minus_SNo (mul_SNo (CSNo_Im x4) (CSNo_Im y6))))) (add_SNo x12 (add_SNo (mul_SNo (CSNo_Re x4) (CSNo_Re y6)) (minus_SNo (mul_SNo (CSNo_Im x4) (CSNo_Im y6)))))) x10 x9 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with x4, y6, λ x9 x10 . (λ x11 x12 . (λ x13 . x8) (add_SNo (CSNo_Re (mul_CSNo x4 y5)) x11) (add_SNo (CSNo_Re (mul_CSNo x4 y5)) x12)) ... ... leaving 3 subgoals.
...
...
...
set y8 to be λ x8 . y7
Apply L14 with λ x9 . y8 x9 y7y8 y7 x9 leaving 2 subgoals.
Assume H15: y8 y7 y7.
The subproof is completed by applying H15.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with mul_CSNo y5 y6, mul_CSNo y5 y7, λ x9 x10 . (λ x11 . y8) x10 x9 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
The subproof is completed by applying L14.
Let x4 of type ιιο be given.
Apply L12 with λ x5 . x4 x5 y3x4 y3 x5.
Assume H13: x4 y3 y3.
The subproof is completed by applying H13.
...