Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ SNoS_ omega.
Apply SNoS_E2 with omega, x0, x0 ∈ 87ab7.. leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H0.
Assume H1: SNoLev x0 ∈ omega.
Assume H2: ordinal (SNoLev x0).
Assume H3: SNo x0.
Assume H4: SNo_ (SNoLev x0) x0.
Apply unknownprop_09fffc7b9e5d0b1d7f15cd56209324363defbb3ebe9c272e83a66e2590b7bd24 with x0 leaving 5 subgoals.
Apply SNoS_I with ordsucc omega, x0, SNoLev x0 leaving 3 subgoals.
Apply ordinal_ordsucc with omega.
The subproof is completed by applying omega_ordinal.
Apply ordsuccI1 with omega, SNoLev x0.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Assume H5: SNoL_omega x0 = 0.
Apply EmptyE with SNo_extend0 x0.
Apply H5 with λ x1 x2 . SNo_extend0 x0 ∈ x1.
Apply SepI with SNoS_ omega, λ x1 . SNoLt x1 x0, SNo_extend0 x0 leaving 2 subgoals.
Apply SNoS_I with omega, SNo_extend0 x0, ordsucc (SNoLev x0) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Apply omega_ordsucc with SNoLev x0.
The subproof is completed by applying H1.
Apply SNo_extend0_SNo_ with x0.
The subproof is completed by applying H3.
Apply SNo_extend0_Lt with x0.
The subproof is completed by applying H3.
Assume H5: SNoR_omega x0 = 0.
Apply EmptyE with SNo_extend1 x0.
Apply H5 with λ x1 x2 . SNo_extend1 x0 ∈ x1.
Apply SepI with SNoS_ omega, λ x1 . SNoLt x0 x1, SNo_extend1 x0 leaving 2 subgoals.
Apply SNoS_I with omega, SNo_extend1 x0, ordsucc (SNoLev x0) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Apply omega_ordsucc with SNoLev x0.
The subproof is completed by applying H1.
Apply SNo_extend1_SNo_ with x0.
The subproof is completed by applying H3.
Apply SNo_extend1_Gt with x0.
The subproof is completed by applying H3.
Apply unknownprop_f034141f72d6c4eb35d80a2119f7efda32b3a2da588de397b25001b9c4cc72d9 with x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H5: x1 ∈ SNoL_omega x0.
Apply SepE with SNoS_ omega, λ x2 . SNoLt x2 x0, x1, ∃ x2 . and (x2 ∈ omega) (SNoLt (add_SNo x1 (eps_ x2)) x0) leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H6: x1 ∈ SNoS_ omega.
Assume H7: SNoLt x1 x0.
Apply add_SNo_omega_eps_Lt with x1, x0 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H0.
The subproof is completed by applying H7.
Apply unknownprop_76200c785beb8c7d3f1ca8ae3c4cf9b46875e0cfc933a9cb2834cf5dfa366c76 with x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H5: x1 ∈ SNoR_omega x0.
Apply SepE with SNoS_ omega, λ x2 . SNoLt x0 x2, x1, ∃ x2 . and (x2 ∈ omega) (SNoLt x0 (add_SNo x1 (minus_SNo (eps_ x2)))) leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H6: x1 ∈ SNoS_ omega.
Assume H7: SNoLt x0 x1.
Apply SNoS_E2 with omega, x1, ∃ x2 . and (x2 ∈ omega) (SNoLt x0 (add_SNo x1 (minus_SNo (eps_ x2)))) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H6.
Assume H8: SNoLev x1 ∈ omega.
Assume H9: ordinal (SNoLev x1).
Assume H10: SNo x1.
Assume H11: SNo_ (SNoLev x1) x1.
Apply add_SNo_omega_eps_Lt with x0, x1, ∃ x2 . and (x2 ∈ omega) (SNoLt x0 (add_SNo x1 (minus_SNo (eps_ x2)))) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Let x2 of type ι be given.
Assume H12: (λ x3 . and (x3 ∈ omega) (SNoLt (add_SNo x0 (eps_ x3)) x1)) x2.
Apply H12 with ∃ x3 . and (x3 ∈ omega) (SNoLt x0 (add_SNo x1 (minus_SNo (eps_ x3)))).
Assume H13: x2 ∈ omega.
Assume H14: SNoLt (add_SNo x0 (eps_ x2)) x1.
Let x3 of type ο be given.
Assume H15: ∀ x4 . and (x4 ∈ omega) (SNoLt x0 (add_SNo x1 (minus_SNo (eps_ x4)))) ⟶ x3.
Apply H15 with x2.
Apply andI with x2 ∈ omega, ... leaving 2 subgoals.
...
...
■