Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ SNoS_ (ordsucc omega).
Apply SNoS_E with ordsucc omega, x0, x0 = SNoCut (SNoL_omega x0) (SNoR_omega x0) leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H1: (λ x2 . and (x2 ∈ ordsucc omega) (SNo_ x2 x0)) x1.
Apply H1 with x0 = SNoCut (SNoL_omega x0) (SNoR_omega x0).
Assume H2: x1 ∈ ordsucc omega.
Assume H3: SNo_ x1 x0.
Claim L4: ordinal x1
Apply ordinal_Hered with ordsucc omega, x1 leaving 2 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H2.
Claim L5: SNo x0
Apply SNo_SNo with x1, x0 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H3.
Claim L6: SNoCutP (SNoL_omega x0) (SNoR_omega x0)
Apply unknownprop_15b221ba0c4ae0e05ed8cc21a7cdf61ac684525faddd1c477ed29fb7cbd9ee7b with x0.
The subproof is completed by applying L5.
Claim L7: SNoLev x0 = x1
Apply SNoLev_uniq with x0, SNoLev x0, x1 leaving 4 subgoals.
Apply SNoLev_ordinal with x0.
The subproof is completed by applying L5.
The subproof is completed by applying L4.
Apply SNoLev_ with x0.
The subproof is completed by applying L5.
The subproof is completed by applying H3.
Claim L8: SNoLev x0 ⊆ omega
Apply L7 with λ x2 x3 . x3 ⊆ omega.
Apply TransSet_In_ordsucc_Subq with x1, omega leaving 2 subgoals.
The subproof is completed by applying omega_TransSet.
The subproof is completed by applying H2.
Apply SNo_eta with x0, λ x2 x3 . x3 = SNoCut (SNoL_omega x0) (SNoR_omega x0) leaving 2 subgoals.
The subproof is completed by applying L5.
Apply SNoCut_ext with SNoL x0, SNoR x0, SNoL_omega x0, SNoR_omega x0 leaving 6 subgoals.
Apply SNoCutP_SNoL_SNoR with x0.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
Let x2 of type ι be given.
Assume H9: x2 ∈ SNoL x0.
Apply SNoL_E with x0, x2, SNoLt x2 (SNoCut (SNoL_omega x0) (SNoR_omega x0)) leaving 3 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying H9.
Assume H10: SNo x2.
Assume H11: SNoLev x2 ∈ SNoLev x0.
Assume H12: SNoLt x2 x0.
Apply SNoCutP_SNoCut_L with SNoL_omega x0, SNoR_omega x0, x2 leaving 2 subgoals.
The subproof is completed by applying L6.
Apply SepI with SNoS_ omega, λ x3 . SNoLt x3 x0, x2 leaving 2 subgoals.
Apply SNoS_I with omega, x2, SNoLev x2 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Apply L8 with SNoLev x2.
The subproof is completed by applying H11.
Apply SNoLev_ with x2.
The subproof is completed by applying H10.
The subproof is completed by applying H12.
Let x2 of type ι be given.
Assume H9: x2 ∈ SNoR x0.
Apply SNoR_E with x0, x2, SNoLt (SNoCut (SNoL_omega x0) (SNoR_omega x0)) x2 leaving 3 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying H9.
Assume H10: SNo x2.
Assume H11: SNoLev x2 ∈ SNoLev x0.
Assume H12: SNoLt x0 x2.
Apply SNoCutP_SNoCut_R with SNoL_omega x0, SNoR_omega x0, x2 leaving 2 subgoals.
The subproof is completed by applying L6.
Apply SepI with SNoS_ omega, λ x3 . SNoLt x0 x3, x2 leaving 2 subgoals.
Apply SNoS_I with omega, x2, SNoLev x2 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Apply L8 with SNoLev x2.
The subproof is completed by applying H11.
Apply SNoLev_ with x2.
The subproof is completed by applying H10.
The subproof is completed by applying H12.
Let x2 of type ι be given.
Assume H9: x2 ∈ SNoL_omega x0.
Apply SNo_eta with x0, λ x3 x4 . SNoLt x2 x3 leaving 2 subgoals.
The subproof is completed by applying L5.
Apply SepE with SNoS_ omega, λ x3 . SNoLt x3 x0, x2, SNoLt x2 x0 leaving 2 subgoals.
The subproof is completed by applying H9.
Assume H10: x2 ∈ SNoS_ omega.
Assume H11: SNoLt x2 x0.
The subproof is completed by applying H11.
Let x2 of type ι be given.
Assume H9: x2 ∈ SNoR_omega x0.
Apply SNo_eta with x0, λ x3 x4 . SNoLt x3 x2 leaving 2 subgoals.
The subproof is completed by applying L5.
Apply SepE with SNoS_ omega, λ x3 . SNoLt x0 x3, x2, SNoLt x0 x2 leaving 2 subgoals.
The subproof is completed by applying H9.
Assume H10: x2 ∈ SNoS_ omega.
Assume H11: SNoLt x0 x2.
The subproof is completed by applying H11.
■