Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι → ι be given.
Assume H1: SNo_ord_seq x0 x1.
Let x2 of type ι be given.
Assume H2: SNo x2.
Assume H3: 2be79.. x0 x1 x2.
Let x3 of type ι be given.
Assume H4: SNo x3.
Assume H5: 2be79.. x0 x1 x3.
Assume H6: SNoLt x2 x3.
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Apply H3 with mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2)), False leaving 3 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying L12.
Let x4 of type ι be given.
Assume H13: (λ x5 . and (x5 ∈ x0) (∀ x6 . x6 ∈ setminus x0 x5 ⟶ SNoLt (abs_SNo (add_SNo (x1 x6) (minus_SNo x2))) (mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2))))) x4.
Apply H13 with False.
Assume H14: x4 ∈ x0.
Assume H15: ∀ x5 . x5 ∈ setminus x0 x4 ⟶ SNoLt (abs_SNo (add_SNo (x1 x5) (minus_SNo x2))) (mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2))).
Apply H5 with mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2)), False leaving 3 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying L12.
Let x5 of type ι be given.
Assume H16: (λ x6 . and (x6 ∈ x0) (∀ x7 . x7 ∈ setminus x0 x6 ⟶ SNoLt (abs_SNo (add_SNo (x1 x7) (minus_SNo x3))) (mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2))))) x5.
Apply H16 with False.
Assume H17: x5 ∈ x0.
Assume H18: ∀ x6 . x6 ∈ setminus x0 x5 ⟶ SNoLt (abs_SNo (add_SNo (x1 x6) (minus_SNo x3))) (mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2))).
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Apply L21 with False.
Let x6 of type ι be given.
Assume H22: (λ x7 . and (x7 ∈ x0) (and (SNoLt (abs_SNo (add_SNo (x1 x7) (minus_SNo x2))) (mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2)))) (SNoLt (abs_SNo (add_SNo (x1 x7) (minus_SNo x3))) (mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2)))))) x6.
Apply H22 with False.
Assume H23: x6 ∈ x0.
Assume H24: and (SNoLt (abs_SNo (add_SNo (x1 x6) (minus_SNo x2))) (mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2)))) (SNoLt (abs_SNo (add_SNo (x1 x6) (minus_SNo x3))) (mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2)))).
Apply H24 with False.
Assume H25: SNoLt (abs_SNo (add_SNo (x1 x6) (minus_SNo x2))) (mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2))).
Assume H26: SNoLt (abs_SNo (add_SNo (x1 x6) (minus_SNo x3))) (mul_SNo (eps_ 1) (add_SNo x3 (minus_SNo x2))).
Claim L27: ...
...
Claim L28: ...
...
Claim L29: ...
...
Apply SNoLt_irref with add_SNo x3 (minus_SNo x2).
Apply SNoLeLt_tra with add_SNo x3 (minus_SNo ...), ..., ... leaving 5 subgoals.
...
...
...
...
...
■