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 ∈ real 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 real_I with x0 leaving 4 subgoals.
Apply SNoS_Subq with omega, ordsucc omega, x0 leaving 4 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying ordsuccI1 with omega.
The subproof is completed by applying H0.
Assume H5: x0 = omega.
Apply In_irref with SNoLev x0.
Apply H5 with λ x1 x2 . SNoLev x0 ∈ SNoLev x2.
Apply ordinal_SNoLev with omega, λ x1 x2 . SNoLev x0 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H1.
Assume H5: x0 = minus_SNo omega.
Apply In_irref with SNoLev x0.
Apply H5 with λ x1 x2 . SNoLev x0 ∈ SNoLev x2.
Apply minus_SNo_Lev with omega, λ x1 x2 . SNoLev x0 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying SNo_omega.
Apply ordinal_SNoLev with omega, λ x1 x2 . SNoLev x0 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H5: x1 ∈ SNoS_ omega.
Assume H6: ∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2).
Apply SNoS_E2 with omega, x1, x1 = x0 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H5.
Assume H7: SNoLev x1 ∈ omega.
Assume H8: ordinal (SNoLev x1).
Assume H9: SNo x1.
Assume H10: SNo_ (SNoLev x1) x1.
Apply SNoLt_trichotomy_or_impred with x1, x0, x1 = x0 leaving 5 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H3.
Assume H11: SNoLt x1 x0.
Apply FalseE with x1 = x0.
Apply SNoS_E2 with omega, add_SNo x0 (minus_SNo x1), False leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Apply add_SNo_SNoS_omega with x0, minus_SNo x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply minus_SNo_SNoS_omega with x1.
The subproof is completed by applying H5.
Assume H12: SNoLev (add_SNo x0 (minus_SNo x1)) ∈ omega.
Assume H13: ordinal (SNoLev (add_SNo x0 (minus_SNo x1))).
Assume H14: SNo (add_SNo x0 (minus_SNo x1)).
Assume H15: SNo_ (SNoLev (add_SNo x0 (minus_SNo x1))) (add_SNo x0 (minus_SNo x1)).
Apply SNoLt_irref with add_SNo x0 (minus_SNo x1).
Apply SNoLt_tra with add_SNo x0 (minus_SNo x1), eps_ (SNoLev (add_SNo x0 (minus_SNo x1))), add_SNo x0 (minus_SNo x1) leaving 5 subgoals.
The subproof is completed by applying H14.
Apply SNo_eps_ with SNoLev (add_SNo x0 (minus_SNo x1)).
The subproof is completed by applying H12.
The subproof is completed by applying H14.
Apply abs_SNo_dist_swap with x1, x0, λ x2 x3 . x3 = add_SNo x0 (minus_SNo x1), λ x2 x3 . SNoLt x2 (eps_ (SNoLev (add_SNo x0 (minus_SNo x1)))) leaving 4 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H3.
Apply pos_abs_SNo with add_SNo x0 (minus_SNo x1).
Apply SNoLt_minus_pos with x1, x0 leaving 3 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H3.
The subproof is completed by applying H11.
Apply H6 with SNoLev (add_SNo x0 (minus_SNo x1)).
The subproof is completed by applying H12.
Apply SNo_pos_eps_Lt with SNoLev (add_SNo x0 (minus_SNo x1)), add_SNo x0 (minus_SNo x1) leaving 3 subgoals.
Apply omega_nat_p with SNoLev (add_SNo x0 (minus_SNo x1)).
The subproof is completed by applying H12.
Apply SNoS_I with ordsucc (SNoLev (add_SNo x0 (minus_SNo x1))), add_SNo x0 (minus_SNo x1), SNoLev (add_SNo x0 (minus_SNo x1)) leaving 3 subgoals.
Apply ordinal_ordsucc with SNoLev (add_SNo x0 (minus_SNo x1)).
The subproof is completed by applying H13.
The subproof is completed by applying ordsuccI2 with SNoLev (add_SNo x0 (minus_SNo x1)).
The subproof is completed by applying H15.
Apply SNoLt_minus_pos with x1, x0 leaving 3 subgoals.
The subproof is completed by applying H9.
...
...
...
...
■