Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ 87ab7...
Apply unknownprop_44069e352f5036a86127073abddc29a0ac5cf4eb6f4d81d6ec3a0209c2755103 with x0, minus_SNo x0 ∈ 87ab7.. leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: x0 ∈ SNoS_ (ordsucc omega).
Assume H2: SNoL_omega x0 = 0 ⟶ ∀ x1 : ο . x1.
Assume H3: SNoR_omega x0 = 0 ⟶ ∀ x1 : ο . x1.
Assume H4: f8473.. (SNoL_omega x0).
Assume H5: f8473.. (SNoR_omega x0).
Apply H4 with minus_SNo x0 ∈ 87ab7...
Assume H6: SNoL_omega x0 ⊆ SNoS_ omega.
Assume H7: ∀ x1 . x1 ∈ SNoL_omega x0 ⟶ ∃ x2 . and (x2 ∈ omega) (∀ x3 . x3 ∈ SNoS_ omega ⟶ SNoLt (add_SNo x1 (minus_SNo (eps_ x2))) x3 ⟶ SNoLt x3 (add_SNo x1 (eps_ x2)) ⟶ x3 ∈ SNoL_omega x0).
Apply H5 with minus_SNo x0 ∈ 87ab7...
Assume H8: SNoR_omega x0 ⊆ SNoS_ omega.
Assume H9: ∀ x1 . x1 ∈ SNoR_omega x0 ⟶ ∃ x2 . and (x2 ∈ omega) (∀ x3 . x3 ∈ SNoS_ omega ⟶ SNoLt (add_SNo x1 (minus_SNo (eps_ x2))) x3 ⟶ SNoLt x3 (add_SNo x1 (eps_ x2)) ⟶ x3 ∈ SNoR_omega x0).
Apply SNoS_E2 with ordsucc omega, x0, minus_SNo x0 ∈ 87ab7.. leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H1.
Assume H10: SNoLev x0 ∈ ordsucc omega.
Assume H11: ordinal (SNoLev x0).
Assume H12: SNo x0.
Assume H13: SNo_ (SNoLev x0) x0.
Claim L14: ...
...
Apply unknownprop_09fffc7b9e5d0b1d7f15cd56209324363defbb3ebe9c272e83a66e2590b7bd24 with minus_SNo x0 leaving 5 subgoals.
Apply SNoS_I with ordsucc omega, minus_SNo x0, SNoLev (minus_SNo x0) leaving 3 subgoals.
Apply ordinal_ordsucc with omega.
The subproof is completed by applying omega_ordinal.
Apply minus_SNo_Lev with x0, λ x1 x2 . x2 ∈ ordsucc omega leaving 2 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H10.
Apply SNoLev_ with minus_SNo x0.
The subproof is completed by applying L14.
Assume H15: SNoL_omega (minus_SNo x0) = 0.
Apply H3.
Apply Empty_eq with SNoR_omega x0.
Let x1 of type ι be given.
Assume H16: x1 ∈ SNoR_omega x0.
Apply SepE with SNoS_ omega, λ x2 . SNoLt x0 x2, x1, False leaving 2 subgoals.
The subproof is completed by applying H16.
Assume H17: x1 ∈ SNoS_ omega.
Assume H18: SNoLt x0 x1.
Apply SNoS_E2 with omega, x1, False leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H17.
Assume H19: SNoLev x1 ∈ omega.
Assume H20: ordinal (SNoLev x1).
Assume H21: SNo x1.
Assume H22: SNo_ (SNoLev x1) x1.
Apply EmptyE with minus_SNo x1.
Apply H15 with λ x2 x3 . minus_SNo x1 ∈ x2.
Apply SepI with SNoS_ omega, λ x2 . SNoLt x2 (minus_SNo x0), minus_SNo x1 leaving 2 subgoals.
Apply minus_SNo_SNoS_omega with x1.
The subproof is completed by applying H17.
Apply minus_SNo_Lt_contra with x0, x1 leaving 3 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H21.
The subproof is completed by applying H18.
Assume H15: SNoR_omega (minus_SNo x0) = 0.
Apply H2.
Apply Empty_eq with SNoL_omega x0.
Let x1 of type ι be given.
Assume H16: x1 ∈ SNoL_omega x0.
Apply SepE with SNoS_ omega, λ x2 . SNoLt x2 x0, x1, False leaving 2 subgoals.
The subproof is completed by applying H16.
Assume H17: x1 ∈ SNoS_ omega.
Assume H18: SNoLt x1 x0.
Apply SNoS_E2 with omega, x1, False leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H17.
Assume H19: SNoLev x1 ∈ ....
...
...
...
■