Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Let x1 of type ι be given.
Assume H1: x1 ∈ setexp (SNoS_ omega) omega.
Let x2 of type ι be given.
Assume H2: x2 ∈ setexp (SNoS_ omega) omega.
Assume H3: ∀ x3 . x3 ∈ omega ⟶ SNoLt (ap x1 x3) x0.
Assume H4: ∀ x3 . x3 ∈ omega ⟶ SNoLt x0 (add_SNo (ap x1 x3) (eps_ x3)).
Assume H5: ∀ x3 . x3 ∈ omega ⟶ ∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x1 x4) (ap x1 x3).
Assume H6: ∀ x3 . x3 ∈ omega ⟶ SNoLt x0 (ap x2 x3).
Assume H7: ∀ x3 . x3 ∈ omega ⟶ ∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x2 x3) (ap x2 x4).
Assume H8: x0 = SNoCut {ap x1 x3|x3 ∈ omega} {ap x2 x3|x3 ∈ omega}.
Claim L9: ...
...
Claim L10: ...
...
Apply SNo_approx_real_lem with x1, x2, x0 ∈ real leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H11: x3 ∈ omega.
Let x4 of type ι be given.
Assume H12: x4 ∈ omega.
Apply SNoLt_tra with ap x1 x3, x0, ap x2 x4 leaving 5 subgoals.
Apply L9 with x3.
The subproof is completed by applying H11.
The subproof is completed by applying H0.
Apply L10 with x4.
The subproof is completed by applying H12.
Apply H3 with x3.
The subproof is completed by applying H11.
Apply H6 with x4.
The subproof is completed by applying H12.
Apply H8 with λ x3 x4 . SNoCutP (prim5 omega (ap x1)) (prim5 omega (ap x2)) ⟶ SNo x3 ⟶ SNoLev (SNoCut (prim5 omega (ap x1)) (prim5 omega (ap x2))) ∈ ordsucc omega ⟶ SNoCut (prim5 omega (ap x1)) (prim5 omega (ap x2)) ∈ SNoS_ (ordsucc omega) ⟶ (∀ x5 . x5 ∈ omega ⟶ SNoLt (ap x1 x5) (SNoCut (prim5 omega (ap x1)) (prim5 omega (ap x2)))) ⟶ (∀ x5 . x5 ∈ omega ⟶ SNoLt (SNoCut (prim5 omega (ap x1)) (prim5 omega (ap x2))) (ap x2 x5)) ⟶ x0 ∈ real.
Assume H11: SNoCutP {ap x1 x3|x3 ∈ omega} {ap x2 x3|x3 ∈ omega}.
Assume H12: SNo x0.
Apply H8 with λ x3 x4 . SNoLev x3 ∈ ... ⟶ SNoCut (prim5 omega (ap x1)) (prim5 omega (ap x2)) ∈ SNoS_ (ordsucc omega) ⟶ (∀ x5 . x5 ∈ omega ⟶ SNoLt (ap x1 x5) (SNoCut (prim5 omega (ap x1)) (prim5 omega (ap x2)))) ⟶ (∀ x5 . x5 ∈ omega ⟶ SNoLt (SNoCut (prim5 omega (ap x1)) (prim5 omega (ap x2))) (ap x2 x5)) ⟶ x0 ∈ real.
...
■