Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ SNoS_ omega.
Let x1 of type ι be given.
Assume H1: x1 ∈ SNoS_ omega.
Assume H2: SNoLt x0 x1.
Apply SNoS_E2 with omega, x0, ∃ x2 . and (x2 ∈ omega) (SNoLt (add_SNo x0 (eps_ x2)) x1) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H0.
Assume H3: SNoLev x0 ∈ omega.
Assume H4: ordinal (SNoLev x0).
Assume H5: SNo x0.
Assume H6: SNo_ (SNoLev x0) x0.
Apply SNoS_E2 with omega, x1, ∃ x2 . and (x2 ∈ omega) (SNoLt (add_SNo x0 (eps_ x2)) x1) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H1.
Assume H7: SNoLev x1 ∈ omega.
Assume H8: ordinal (SNoLev x1).
Assume H9: SNo x1.
Assume H10: SNo_ (SNoLev x1) x1.
Claim L11: ...
...
Apply SNoS_E2 with omega, add_SNo x1 (minus_SNo x0), ∃ x2 . and (x2 ∈ omega) (SNoLt (add_SNo x0 (eps_ x2)) x1) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying L11.
Assume H12: SNoLev (add_SNo x1 (minus_SNo x0)) ∈ omega.
Assume H13: ordinal (SNoLev (add_SNo x1 (minus_SNo x0))).
Assume H14: SNo (add_SNo x1 (minus_SNo x0)).
Assume H15: SNo_ (SNoLev (add_SNo x1 (minus_SNo x0))) (add_SNo x1 (minus_SNo x0)).
Claim L16: ...
...
Claim L17: add_SNo x1 (minus_SNo x0) ∈ SNoS_ (ordsucc (SNoLev (add_SNo x1 (minus_SNo x0))))
Apply SNoS_I with ordsucc (SNoLev (add_SNo x1 (minus_SNo x0))), add_SNo ... ..., ... leaving 3 subgoals.
...
...
...
Claim L18: ordsucc (SNoLev (add_SNo x1 (minus_SNo x0))) ∈ omega
Apply omega_ordsucc with SNoLev (add_SNo x1 (minus_SNo x0)).
The subproof is completed by applying H12.
Claim L19: SNoLt (eps_ (ordsucc (SNoLev (add_SNo x1 (minus_SNo x0))))) (add_SNo x1 (minus_SNo x0))
Apply unknownprop_575b837b657e6e7a9b06a3cf27feee72addd6cc960da74d3e2bbceddc997f016 with ordsucc (SNoLev (add_SNo x1 (minus_SNo x0))), add_SNo x1 (minus_SNo x0) leaving 3 subgoals.
Apply omega_nat_p with ordsucc (SNoLev (add_SNo x1 (minus_SNo x0))).
The subproof is completed by applying L18.
The subproof is completed by applying L17.
The subproof is completed by applying L16.
Claim L20: SNo (eps_ (ordsucc (SNoLev (add_SNo x1 (minus_SNo x0)))))
Apply SNo_eps_ with ordsucc (SNoLev (add_SNo x1 (minus_SNo x0))).
The subproof is completed by applying L18.
Let x2 of type ο be given.
Assume H21: ∀ x3 . and (x3 ∈ omega) (SNoLt (add_SNo x0 (eps_ x3)) x1) ⟶ x2.
Apply H21 with ordsucc (SNoLev (add_SNo x1 (minus_SNo x0))).
Apply andI with ordsucc (SNoLev (add_SNo x1 (minus_SNo x0))) ∈ omega, SNoLt (add_SNo x0 (eps_ (ordsucc (SNoLev (add_SNo x1 (minus_SNo x0)))))) x1 leaving 2 subgoals.
The subproof is completed by applying L18.
Apply add_SNo_com with x0, eps_ (ordsucc (SNoLev (add_SNo x1 (minus_SNo x0)))), λ x3 x4 . SNoLt x4 x1 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying L20.
Apply add_SNo_minus_Lt2 with x1, x0, eps_ (ordsucc (SNoLev (add_SNo x1 (minus_SNo x0)))) leaving 4 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H5.
The subproof is completed by applying L20.
The subproof is completed by applying L19.
■