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: ...
...
Apply CSNo_ReIm_split with add_CSNo x0 (add_CSNo x1 x2), add_CSNo (add_CSNo x0 x1) x2 leaving 4 subgoals.
Apply CSNo_add_CSNo 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 add_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 L5: ∀ x4 : ι → ο . x4 y3x4 (CSNo_Re (add_CSNo x0 (add_CSNo x1 x2)))
Let x4 of type ιο be given.
Assume H5: x4 (CSNo_Re (add_CSNo (add_CSNo x1 x2) y3)).
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 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 L6: ∀ x6 : ι → ο . x6 y5x6 (add_SNo (CSNo_Re x1) (CSNo_Re (add_CSNo x2 y3)))
Let x6 of type ιο be given.
Assume H6: x6 (CSNo_Re (add_CSNo (add_CSNo x2 y3) x4)).
set y7 to be ...
Claim L7: ∀ x8 : ι → ο . x8 y7x8 (add_SNo (CSNo_Re x2) (CSNo_Re (add_CSNo y3 x4)))
Let x8 of type ιο be given.
Assume H7: x8 (add_SNo (CSNo_Re (add_CSNo y3 x4)) (CSNo_Re y5)).
Apply f_eq_i with λ x9 . add_SNo (CSNo_Re y3) x9, CSNo_Re (add_CSNo x4 y5), add_SNo (CSNo_Re x4) (CSNo_Re y5), λ x9 . x8 leaving 2 subgoals.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with x4, y5 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
set y9 to be ...
Claim L8: ∀ x10 : ι → ο . x10 y9x10 (add_SNo (CSNo_Re y3) (add_SNo (CSNo_Re x4) (CSNo_Re y5)))
Let x10 of type ιο be given.
Assume H8: x10 (add_SNo (CSNo_Re (add_CSNo x4 y5)) (CSNo_Re x6)).
Apply add_SNo_assoc with CSNo_Re x4, CSNo_Re y5, CSNo_Re x6, λ x11 . x10 leaving 4 subgoals.
Apply CSNo_ReR with x4.
The subproof is completed by applying H0.
Apply CSNo_ReR with y5.
The subproof is completed by applying H1.
Apply CSNo_ReR with x6.
The subproof is completed by applying H2.
set y11 to be ...
Claim L9: ∀ x12 : ι → ο . x12 y11x12 ((λ x13 . add_SNo x13 (CSNo_Re x6)) (CSNo_Re (add_CSNo x4 y5)))
Let x12 of type ιο be given.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with y5, x6, λ x13 x14 . (λ x15 . x12) ((λ x15 . add_SNo x15 (CSNo_Re y7)) x13) ((λ x15 . add_SNo x15 ...) ...) leaving 2 subgoals.
...
...
set y12 to be λ x12 x13 . (λ x14 . y11) x13 x12
Apply L9 with λ x13 . y12 x13 y11y12 y11 x13 leaving 2 subgoals.
Assume H10: y12 y11 y11.
The subproof is completed by applying H10.
The subproof is completed by applying L9.
set y10 to be λ x10 . y9
Apply L8 with λ x11 . y10 x11 y9y10 y9 x11 leaving 2 subgoals.
Assume H9: y10 y9 y9.
The subproof is completed by applying H9.
The subproof is completed by applying L8.
set y8 to be λ x8 . y7
Apply L7 with λ x9 . y8 x9 y7y8 y7 x9 leaving 2 subgoals.
Assume H8: y8 y7 y7.
The subproof is completed by applying H8.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with add_CSNo x4 y5, x6, λ x9 x10 . (λ x11 . y8) x10 x9 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying L3.
The subproof is completed by applying L7.
set y6 to be λ x6 . y5
Apply L6 with λ x7 . y6 x7 y5y6 y5 x7 leaving 2 subgoals.
Assume H7: y6 y5 y5.
The subproof is completed by applying H7.
The subproof is completed by applying L6.
Let x4 of type ιιο be given.
Apply L5 with λ x5 . x4 x5 y3x4 y3 x5.
Assume H6: x4 y3 y3.
The subproof is completed by applying H6.
...