Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Let x1 of type ι be given.
Assume H1: x1 ∈ real.
Apply SNo_approx_real_rep with x0, add_SNo x0 x1 ∈ real leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H2: x2 ∈ setexp (SNoS_ omega) omega.
Let x3 of type ι be given.
Assume H3: x3 ∈ setexp (SNoS_ omega) omega.
Assume H4: ∀ x4 . x4 ∈ omega ⟶ SNoLt (ap x2 x4) x0.
Assume H5: ∀ x4 . x4 ∈ omega ⟶ SNoLt x0 (add_SNo (ap x2 x4) (eps_ x4)).
Assume H6: ∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ x4 ⟶ SNoLt (ap x2 x5) (ap x2 x4).
Assume H7: ∀ x4 . x4 ∈ omega ⟶ SNoLt (add_SNo (ap x3 x4) (minus_SNo (eps_ x4))) x0.
Assume H8: ∀ x4 . x4 ∈ omega ⟶ SNoLt x0 (ap x3 x4).
Assume H9: ∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ x4 ⟶ SNoLt (ap x3 x4) (ap x3 x5).
Assume H10: SNoCutP (prim5 omega (ap x2)) (prim5 omega (ap x3)).
Assume H11: x0 = SNoCut (prim5 omega (ap x2)) (prim5 omega (ap x3)).
Apply SNo_approx_real_rep with x1, add_SNo x0 x1 ∈ real leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Assume H12: x4 ∈ setexp (SNoS_ omega) omega.
Let x5 of type ι be given.
Assume H13: x5 ∈ setexp (SNoS_ omega) omega.
Assume H14: ∀ x6 . x6 ∈ omega ⟶ SNoLt (ap x4 x6) x1.
Assume H15: ∀ x6 . x6 ∈ omega ⟶ SNoLt x1 (add_SNo (ap x4 x6) (eps_ x6)).
Assume H16: ∀ x6 . x6 ∈ omega ⟶ ∀ x7 . x7 ∈ x6 ⟶ SNoLt (ap x4 x7) (ap x4 x6).
Assume H17: ∀ x6 . x6 ∈ omega ⟶ SNoLt (add_SNo (ap x5 x6) (minus_SNo (eps_ x6))) x1.
Assume H18: ∀ x6 . x6 ∈ omega ⟶ SNoLt x1 (ap x5 x6).
Assume H19: ∀ x6 . x6 ∈ omega ⟶ ∀ x7 . x7 ∈ x6 ⟶ SNoLt (ap x5 x6) (ap x5 x7).
Assume H20: SNoCutP (prim5 omega (ap x4)) (prim5 omega (ap x5)).
Assume H21: x1 = SNoCut (prim5 omega (ap x4)) (prim5 omega (ap x5)).
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Claim L26: ...
...
Claim L27: ...
...
Claim L28: ...
...
Claim L29: ...
...
Claim L30: ...
...
Claim L31: ...
...
Claim L32: ...
...
Claim L33: ...
...
Claim L34: ...
...
Claim L35: ...
...
Claim L36: ...
...
Claim L37: ...
...
Claim L38: ...
...
Claim L39: ...
...
Claim L40: ...
...
Claim L41: ...
...
Apply SNoCutP_SNoCut_impred with {ap (lam omega (λ x7 . add_SNo (ap x2 (ordsucc x7)) (ap x4 (ordsucc x7)))) x6|x6 ∈ omega}, {ap (lam omega (λ x7 . add_SNo ... ...)) ...|x6 ∈ omega}, ... leaving 2 subgoals.
...
...
■