Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
CSNo
x0
.
Claim L1:
SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
Apply SNo_minus_SNo with
CSNo_Re
x0
.
Apply CSNo_ReR with
x0
.
The subproof is completed by applying H0.
Claim L2:
SNo
(
minus_SNo
(
CSNo_Im
x0
)
)
Apply SNo_minus_SNo with
CSNo_Im
x0
.
Apply CSNo_ImR with
x0
.
The subproof is completed by applying H0.
Apply CSNo_Re2 with
minus_SNo
(
CSNo_Re
x0
)
,
minus_SNo
(
CSNo_Im
x0
)
,
λ x1 x2 .
SNo_pair
(
add_SNo
x2
(
CSNo_Re
x0
)
)
(
add_SNo
(
CSNo_Im
(
SNo_pair
(
minus_SNo
(
CSNo_Re
x0
)
)
(
minus_SNo
(
CSNo_Im
x0
)
)
)
)
(
CSNo_Im
x0
)
)
=
0
leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply CSNo_Im2 with
minus_SNo
(
CSNo_Re
x0
)
,
minus_SNo
(
CSNo_Im
x0
)
,
λ x1 x2 .
SNo_pair
(
add_SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
(
CSNo_Re
x0
)
)
(
add_SNo
x2
(
CSNo_Im
x0
)
)
=
0
leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply add_SNo_minus_SNo_linv with
CSNo_Re
x0
,
λ x1 x2 .
SNo_pair
x2
(
add_SNo
(
minus_SNo
(
CSNo_Im
x0
)
)
(
CSNo_Im
x0
)
)
=
0
leaving 2 subgoals.
Apply CSNo_ReR with
x0
.
The subproof is completed by applying H0.
Apply add_SNo_minus_SNo_linv with
CSNo_Im
x0
,
λ x1 x2 .
SNo_pair
0
x2
=
0
leaving 2 subgoals.
Apply CSNo_ImR with
x0
.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_pair_0 with
0
.
■