Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Apply and3I with ∀ x1 . x1 ∈ SNoL_omega x0 ⟶ SNo x1, ∀ x1 . x1 ∈ SNoR_omega x0 ⟶ SNo x1, ∀ x1 . x1 ∈ SNoL_omega x0 ⟶ ∀ x2 . x2 ∈ SNoR_omega x0 ⟶ SNoLt x1 x2 leaving 3 subgoals.
Let x1 of type ι be given.
Assume H1: x1 ∈ SNoL_omega x0.
Apply SepE with SNoS_ omega, λ x2 . SNoLt x2 x0, x1, SNo x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: x1 ∈ SNoS_ omega.
Assume H3: SNoLt x1 x0.
Apply SNoS_E2 with omega, x1, SNo x1 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H2.
Assume H4: SNoLev x1 ∈ omega.
Assume H5: ordinal (SNoLev x1).
Assume H6: SNo x1.
Assume H7: SNo_ (SNoLev x1) x1.
The subproof is completed by applying H6.
Let x1 of type ι be given.
Assume H1: x1 ∈ SNoR_omega x0.
Apply SepE with SNoS_ omega, λ x2 . SNoLt x0 x2, x1, SNo x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: x1 ∈ SNoS_ omega.
Assume H3: SNoLt x0 x1.
Apply SNoS_E2 with omega, x1, SNo x1 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H2.
Assume H4: SNoLev x1 ∈ omega.
Assume H5: ordinal (SNoLev x1).
Assume H6: SNo x1.
Assume H7: SNo_ (SNoLev x1) x1.
The subproof is completed by applying H6.
Let x1 of type ι be given.
Assume H1: x1 ∈ SNoL_omega x0.
Let x2 of type ι be given.
Assume H2: x2 ∈ SNoR_omega x0.
Apply SepE with SNoS_ omega, λ x3 . SNoLt x3 x0, x1, SNoLt x1 x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3: x1 ∈ SNoS_ omega.
Assume H4: SNoLt x1 x0.
Apply SNoS_E2 with omega, x1, SNoLt x1 x2 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H3.
Assume H5: SNoLev x1 ∈ omega.
Assume H6: ordinal (SNoLev x1).
Assume H7: SNo x1.
Assume H8: SNo_ (SNoLev x1) x1.
Apply SepE with SNoS_ omega, λ x3 . SNoLt x0 x3, x2, SNoLt x1 x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H9: x2 ∈ SNoS_ omega.
Assume H10: SNoLt x0 x2.
Apply SNoS_E2 with omega, x2, SNoLt x1 x2 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H9.
Assume H11: SNoLev x2 ∈ omega.
Assume H12: ordinal (SNoLev x2).
Assume H13: SNo x2.
Assume H14: SNo_ (SNoLev x2) x2.
Apply SNoLt_tra with x1, x0, x2 leaving 5 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H0.
The subproof is completed by applying H13.
The subproof is completed by applying H4.
The subproof is completed by applying H10.
■