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: ...
...
Apply CSNo_ReIm_split with mul_CSNo x0 (mul_CSNo x1 x2), mul_CSNo (mul_CSNo x0 x1) x2 leaving 4 subgoals.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with x0, mul_CSNo x1 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with mul_CSNo x0 x1, x2 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
set y3 to be ...
Claim L11: ∀ x4 : ι → ο . x4 y3x4 (CSNo_Re (mul_CSNo x0 (mul_CSNo x1 x2)))
Let x4 of type ιο be given.
Assume H11: x4 (CSNo_Re (mul_CSNo (mul_CSNo x1 x2) y3)).
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with x1, mul_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 L12: ...
...
set y6 to be ...
Apply L12 with λ x7 . y6 x7 y5y6 y5 x7 leaving 2 subgoals.
Assume H13: y6 y5 y5.
The subproof is completed by applying H13.
Apply add_SNo_rotate_4_0312 with mul_SNo (CSNo_Re y3) (mul_SNo (CSNo_Re x4) (CSNo_Re y5)), minus_SNo (mul_SNo (CSNo_Re y3) (mul_SNo (CSNo_Im x4) (CSNo_Im y5))), minus_SNo (mul_SNo (CSNo_Im y3) (mul_SNo (CSNo_Re x4) (CSNo_Im y5))), minus_SNo (mul_SNo (CSNo_Im y3) (mul_SNo (CSNo_Im x4) (CSNo_Re y5))), λ x7 . y6 leaving 5 subgoals.
Apply SNo_mul_SNo_3 with CSNo_Re y3, CSNo_Re x4, CSNo_Re y5 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
The subproof is completed by applying L8.
Apply SNo_minus_SNo with mul_SNo (CSNo_Re y3) (mul_SNo (CSNo_Im x4) (CSNo_Im y5)).
Apply SNo_mul_SNo_3 with CSNo_Re y3, CSNo_Im x4, CSNo_Im y5 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L10.
The subproof is completed by applying H11.
Apply SNo_minus_SNo with mul_SNo (CSNo_Im y3) (mul_SNo (CSNo_Re x4) (CSNo_Im y5)).
Apply SNo_mul_SNo_3 with CSNo_Im y3, CSNo_Re x4, CSNo_Im y5 leaving 3 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying L7.
The subproof is completed by applying H11.
Apply SNo_minus_SNo with mul_SNo (CSNo_Im y3) (mul_SNo (CSNo_Im x4) (CSNo_Re y5)).
Apply SNo_mul_SNo_3 with CSNo_Im y3, CSNo_Im x4, CSNo_Re y5 leaving 3 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying L10.
The subproof is completed by applying L8.
set y7 to be ...
Claim L13: ∀ x8 : ι → ο . x8 y7x8 (add_SNo (add_SNo (mul_SNo (CSNo_Re y3) (mul_SNo (CSNo_Re x4) (CSNo_Re y5))) (minus_SNo (mul_SNo (CSNo_Im y3) (mul_SNo (CSNo_Im x4) (CSNo_Re y5))))) (add_SNo (minus_SNo (mul_SNo (CSNo_Re y3) (mul_SNo (CSNo_Im x4) (CSNo_Im y5)))) (minus_SNo (mul_SNo (CSNo_Im y3) (mul_SNo (CSNo_Re x4) (CSNo_Im y5))))))
Let x8 of type ιο be given.
Assume H13: x8 (add_SNo (mul_SNo (CSNo_Re (mul_CSNo x4 y5)) (CSNo_Re y6)) (minus_SNo (mul_SNo (CSNo_Im (mul_CSNo x4 y5)) (CSNo_Im y6)))).
set y9 to be ...
Claim L14: ...
...
set y10 to be ...
Apply L14 with λ x11 . y10 ... ...y10 y9 x11 leaving 2 subgoals.
...
...
set y8 to be λ x8 . y7
Apply L13 with λ x9 . y8 x9 y7y8 y7 x9 leaving 2 subgoals.
Assume H14: y8 y7 y7.
The subproof is completed by applying H14.
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with mul_CSNo y5 y6, y7, λ x9 x10 . (λ x11 . y8) x10 x9 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L4.
The subproof is completed by applying L13.
Let x4 of type ιιο be given.
Apply L11 with λ x5 . x4 x5 y3x4 y3 x5.
Assume H12: x4 y3 y3.
The subproof is completed by applying H12.
...