Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
CSNo
x0
.
Let x1 of type
ι
be given.
Assume H1:
SNo
x1
.
Assume H2:
mul_SNo
(
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
(
CSNo_Re
x0
)
)
(
mul_SNo
(
CSNo_Im
x0
)
(
CSNo_Im
x0
)
)
)
x1
=
1
.
Claim L3:
...
...
Claim L4:
...
...
Apply unknownprop_e8fe572c395c46aa7a6d67f7a8cd850bf647261d6b3677aecbf3b7ddfa5a7193 with
x1
,
CSNo_Re
x0
,
λ x2 x3 .
mul_CSNo
x0
(
add_CSNo
x2
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_CSNo
x1
(
CSNo_Im
x0
)
)
)
)
)
=
1
leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L3.
Apply unknownprop_e8fe572c395c46aa7a6d67f7a8cd850bf647261d6b3677aecbf3b7ddfa5a7193 with
x1
,
CSNo_Im
x0
,
λ x2 x3 .
mul_CSNo
x0
(
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
x2
)
)
)
=
1
leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying 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
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
,
1
leaving 4 subgoals.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
x0
,
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L11.
The subproof is completed by applying unknownprop_33594f786441fb94cfa9c7be2034d88216fac0dbcbe9e223f18185e2cf6cb053.
Apply Re_1 with
λ x2 x3 .
CSNo_Re
(
mul_CSNo
x0
(
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
)
=
x3
.
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with
x0
,
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
,
λ x2 x3 .
x3
=
1
leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L11.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with
mul_SNo
x1
(
CSNo_Re
x0
)
,
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
,
λ x2 x3 .
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
x3
)
(
minus_SNo
(
mul_SNo
(
CSNo_Im
x0
)
(
CSNo_Im
(
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
)
)
)
=
1
leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L10.
Apply unknownprop_7f97cbea1b316ccd537155d989f2889dd5c3074e8edefbeca1dbc06c62876158 with
mul_SNo
x1
(
CSNo_Re
x0
)
,
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
,
λ x2 x3 .
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
(
add_SNo
(
CSNo_Re
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
)
(
CSNo_Re
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
)
)
(
minus_SNo
(
mul_SNo
(
CSNo_Im
x0
)
x3
)
)
=
1
leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L10.
Apply unknownprop_b3da9c8705efa35c67169a2e2027e4447fcfab350671212d3a9a4c69902c0e94 with
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
,
λ x2 x3 .
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
(
add_SNo
(
CSNo_Re
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
)
x3
)
)
(
minus_SNo
(
mul_SNo
(
CSNo_Im
x0
)
(
add_SNo
(
CSNo_Im
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
)
(
CSNo_Im
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
)
)
)
=
1
leaving 2 subgoals.
The subproof is completed by applying L9.
Apply unknownprop_efd7dfcd3e80202ffcc3e685b73692d3dd99f31e27f878a9cd3b14c55287909a with
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
,
λ x2 x3 .
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
(
add_SNo
(
CSNo_Re
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
)
(
minus_SNo
(
CSNo_Re
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
...
)
)
)
)
)
)
)
...
=
1
leaving 2 subgoals.
...
...
...
■