Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_complete_ind with λ x0 . ∀ x1 . x1 ∈ SNoS_ x0 ⟶ SNoLt 0 x1 ⟶ SNoLt (eps_ x0) x1.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ SNoS_ x1 ⟶ SNoLt 0 x2 ⟶ SNoLt (eps_ x1) x2.
Let x1 of type ι be given.
Assume H2: x1 ∈ SNoS_ x0.
Assume H3: SNoLt 0 x1.
Claim L4: ...
...
Apply SNoS_E2 with x0, x1, SNoLt (eps_ x0) x1 leaving 3 subgoals.
Apply nat_p_ordinal with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Assume H5: SNoLev x1 ∈ x0.
Assume H6: ordinal (SNoLev x1).
Assume H7: SNo x1.
Assume H8: SNo_ (SNoLev x1) x1.
Apply SNoLt_trichotomy_or_impred with eps_ x0, x1, SNoLt (eps_ x0) x1 leaving 5 subgoals.
Apply SNo_eps_ with x0.
The subproof is completed by applying L4.
The subproof is completed by applying H7.
Assume H9: SNoLt (eps_ x0) x1.
The subproof is completed by applying H9.
Assume H9: eps_ x0 = x1.
Apply FalseE with SNoLt (eps_ x0) x1.
Apply In_no2cycle with x0, ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying ordsuccI2 with x0.
Apply SNoLev_eps_ with x0, λ x2 x3 . x2 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying L4.
Apply H9 with λ x2 x3 . SNoLev x3 ∈ x0.
The subproof is completed by applying H5.
Assume H9: SNoLt x1 (eps_ x0).
Apply FalseE with SNoLt (eps_ x0) x1.
Apply SNoLtE with x1, eps_ x0, False leaving 6 subgoals.
The subproof is completed by applying H7.
Apply SNo_eps_ with x0.
The subproof is completed by applying L4.
The subproof is completed by applying H9.
Let x2 of type ι be given.
Assume H10: SNo x2.
Assume H11: SNoLev x2 ∈ binintersect (SNoLev x1) (SNoLev (eps_ x0)).
Assume H12: SNoEq_ (SNoLev x2) x2 x1.
Assume H13: SNoEq_ (SNoLev x2) x2 (eps_ x0).
Assume H14: SNoLt x1 x2.
Assume H15: SNoLt x2 (eps_ x0).
Assume H16: nIn (SNoLev x2) x1.
Assume H17: SNoLev x2 ∈ eps_ x0.
Claim L18: ordsucc (SNoLev x2) ∈ x0
Apply ordinal_ordsucc_In_Subq with x0, SNoLev x1, ordsucc (SNoLev ...) leaving 3 subgoals.
...
...
...
Claim L19: nat_p (ordsucc (SNoLev x2))
Apply nat_p_trans with x0, ordsucc (SNoLev x2) leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L18.
Claim L20: ordsucc (SNoLev x2) ∈ omega
Apply nat_p_omega with ordsucc (SNoLev x2).
The subproof is completed by applying L19.
Claim L21: x2 ∈ SNoS_ (ordsucc (SNoLev x2))
Apply SNoS_I with ordsucc (SNoLev x2), x2, SNoLev x2 leaving 3 subgoals.
Apply nat_p_ordinal with ordsucc (SNoLev x2).
The subproof is completed by applying L19.
The subproof is completed by applying ordsuccI2 with SNoLev x2.
Apply SNoLev_ with x2.
The subproof is completed by applying H10.
Claim L22: SNoLt 0 x2
Apply SNoLt_tra with 0, x1, x2 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H7.
The subproof is completed by applying H10.
The subproof is completed by applying H3.
The subproof is completed by applying H14.
Claim L23: SNoLt (eps_ (ordsucc (SNoLev x2))) x2
Apply H1 with ordsucc (SNoLev x2), x2 leaving 3 subgoals.
The subproof is completed by applying L18.
The subproof is completed by applying L21.
The subproof is completed by applying L22.
Apply SNoLt_irref with eps_ x0.
Apply SNoLt_tra with eps_ x0, eps_ (ordsucc (SNoLev x2)), eps_ x0 leaving 5 subgoals.
Apply SNo_eps_ with x0.
The subproof is completed by applying L4.
Apply SNo_eps_ with ordsucc (SNoLev x2).
The subproof is completed by applying L20.
Apply SNo_eps_ with x0.
The subproof is completed by applying L4.
Apply SNo_eps_decr with x0, ordsucc (SNoLev x2) leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L18.
Apply SNoLt_tra with eps_ (ordsucc (SNoLev x2)), x2, eps_ x0 leaving 5 subgoals.
Apply SNo_eps_ with ordsucc (SNoLev x2).
The subproof is completed by applying L20.
The subproof is completed by applying H10.
Apply SNo_eps_ with x0.
The subproof is completed by applying L4.
The subproof is completed by applying L23.
The subproof is completed by applying H15.
...
...
■