Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_complete_ind with λ x0 . add_SNo (eps_ (ordsucc x0)) (eps_ (ordsucc x0)) = eps_ x0.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ∀ x1 . x1x0add_SNo (eps_ (ordsucc x1)) (eps_ (ordsucc x1)) = eps_ x1.
Claim L2: ...
...
Apply eps_SNoCut with x0, λ x1 x2 . add_SNo (eps_ (ordsucc x0)) (eps_ (ordsucc x0)) = x2 leaving 2 subgoals.
The subproof is completed by applying L2.
Claim L3: ...
...
Claim L4: ...
...
Apply add_SNo_eq with eps_ (ordsucc x0), eps_ (ordsucc x0), λ x1 x2 . x2 = SNoCut (Sing 0) (prim5 x0 eps_) leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L3.
Apply SNoCut_ext with binunion {add_SNo x1 (eps_ (ordsucc x0))|x1 ∈ SNoL (eps_ (ordsucc x0))} {add_SNo (eps_ (ordsucc x0)) x1|x1 ∈ SNoL (eps_ (ordsucc x0))}, binunion {add_SNo x1 (eps_ (ordsucc x0))|x1 ∈ SNoR (eps_ (ordsucc x0))} {add_SNo (eps_ (ordsucc x0)) x1|x1 ∈ SNoR (eps_ (ordsucc x0))}, Sing 0, {eps_ x1|x1 ∈ x0} leaving 6 subgoals.
Apply add_SNo_SNoCutP with eps_ (ordsucc x0), eps_ (ordsucc x0) leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L3.
Apply eps_SNoCutP with x0.
The subproof is completed by applying L2.
Claim L5: ...
...
Let x1 of type ι be given.
Assume H6: x1binunion {add_SNo x2 (eps_ (ordsucc x0))|x2 ∈ SNoL (eps_ (ordsucc x0))} {add_SNo (eps_ (ordsucc x0)) x2|x2 ∈ SNoL (eps_ (ordsucc x0))}.
Apply eps_SNoCut with x0, λ x2 x3 . SNoLt x1 x2 leaving 2 subgoals.
The subproof is completed by applying L2.
Apply binunionE with {add_SNo x2 (eps_ (ordsucc x0))|x2 ∈ SNoL (eps_ (ordsucc x0))}, {add_SNo (eps_ (ordsucc x0)) x2|x2 ∈ SNoL (eps_ (ordsucc x0))}, x1, SNoLt x1 (eps_ x0) leaving 3 subgoals.
The subproof is completed by applying H6.
Assume H7: x1{add_SNo x2 (eps_ (ordsucc x0))|x2 ∈ SNoL (eps_ (ordsucc x0))}.
Apply ReplE_impred with SNoL (eps_ (ordsucc x0)), λ x2 . add_SNo x2 (eps_ (ordsucc x0)), x1, SNoLt x1 (eps_ x0) leaving 2 subgoals.
The subproof is completed by applying H7.
Let x2 of type ι be given.
Assume H8: x2SNoL (eps_ (ordsucc x0)).
Assume H9: x1 = add_SNo x2 (eps_ (ordsucc x0)).
Apply H9 with λ x3 x4 . SNoLt x4 (eps_ x0).
Apply andEL with SNoLt (add_SNo x2 (eps_ (ordsucc x0))) (eps_ x0), SNoLt (add_SNo (eps_ (ordsucc x0)) x2) (eps_ x0).
Apply L5 with x2.
The subproof is completed by applying H8.
Assume H7: x1{add_SNo (eps_ (ordsucc x0)) x2|x2 ∈ SNoL (eps_ (ordsucc x0))}.
Apply ReplE_impred with SNoL (eps_ (ordsucc x0)), λ x2 . add_SNo (eps_ (ordsucc x0)) x2, x1, SNoLt x1 (eps_ x0) leaving 2 subgoals.
The subproof is completed by applying H7.
Let x2 of type ι be given.
Assume H8: x2SNoL (eps_ (ordsucc x0)).
Assume H9: ....
...
...
...
...