Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Assume H1: x1 ∈ SNoS_ (ordsucc x0).
Assume H2: SNoLt 0 x1.
Claim L3: x0 ∈ omega
Apply nat_p_omega with x0.
The subproof is completed by applying H0.
Apply SNoS_E2 with ordsucc x0, x1, SNoLt (eps_ x0) x1 leaving 3 subgoals.
Apply nat_p_ordinal with ordsucc x0.
Apply nat_ordsucc with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H4: SNoLev x1 ∈ ordsucc x0.
Assume H5: ordinal (SNoLev x1).
Assume H6: SNo x1.
Assume H7: 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 L3.
The subproof is completed by applying H6.
Assume H8: SNoLt (eps_ x0) x1.
The subproof is completed by applying H8.
Assume H8: eps_ x0 = x1.
Apply FalseE with SNoLt (eps_ x0) x1.
Apply In_irref with ordsucc x0.
Apply SNoLev_eps_ with x0, λ x2 x3 . x2 ∈ ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying L3.
Apply H8 with λ x2 x3 . SNoLev x3 ∈ ordsucc x0.
The subproof is completed by applying H4.
Assume H8: 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 H6.
Apply SNo_eps_ with x0.
The subproof is completed by applying L3.
The subproof is completed by applying H8.
Let x2 of type ι be given.
Assume H9: SNo x2.
Assume H10: SNoLev x2 ∈ binintersect (SNoLev x1) (SNoLev (eps_ x0)).
Assume H11: SNoEq_ (SNoLev x2) x2 x1.
Assume H12: SNoEq_ (SNoLev x2) x2 (eps_ x0).
Assume H13: SNoLt x1 x2.
Assume H14: SNoLt x2 (eps_ x0).
Assume H15: nIn (SNoLev x2) x1.
Assume H16: SNoLev x2 ∈ eps_ x0.
Claim L17: x2 = 0
Apply SNoLev_0_eq_0 with x2 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply eps_ordinal_In_eq_0 with x0, SNoLev x2 leaving 2 subgoals.
Apply SNoLev_ordinal with x2.
The subproof is completed by applying H9.
The subproof is completed by applying H16.
Apply SNoLt_irref with x1.
Apply SNoLt_tra with x1, x2, x1 leaving 5 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H9.
The subproof is completed by applying H6.
The subproof is completed by applying H13.
Apply L17 with λ x3 x4 . SNoLt x4 x1.
The subproof is completed by applying H2.
Assume H9: SNoLev x1 ∈ SNoLev (eps_ x0).
Assume H10: SNoEq_ (SNoLev x1) x1 (eps_ x0).
Assume H11: SNoLev x1 ∈ eps_ x0.
Claim L12: x1 = 0
Apply SNoLev_0_eq_0 with x1 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply eps_ordinal_In_eq_0 with x0, SNoLev x1 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H11.
Apply SNoLt_irref with x1.
Apply L12 with λ x2 x3 . SNoLt x3 x1.
The subproof is completed by applying H2.
Apply SNoLev_eps_ with x0, λ x2 x3 . x3 ∈ SNoLev x1 ⟶ SNoEq_ x3 x1 (eps_ x0) ⟶ nIn x3 x1 ⟶ False leaving 2 subgoals.
The subproof is completed by applying L3.
Assume H9: ordsucc x0 ∈ SNoLev x1.
Apply FalseE with SNoEq_ (ordsucc x0) x1 (eps_ x0) ⟶ nIn (ordsucc x0) x1 ⟶ False.
Apply In_no2cycle with SNoLev x1, ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H9.
■