Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 368eb.. x0.
Apply H0 with 368eb.. x1SNoLt 0 x0SNoLt 0 x1368eb.. (add_SNo x0 x1).
Let x2 of type ι be given.
Assume H1: (λ x3 . and (x3omega) (∃ x4 . and (x4omega) (or (x0 = mul_SNo (eps_ x3) x4) (x0 = minus_SNo (mul_SNo (eps_ x3) x4))))) x2.
Apply H1 with 368eb.. x1SNoLt 0 x0SNoLt 0 x1368eb.. (add_SNo x0 x1).
Assume H2: x2omega.
Claim L3: ...
...
Assume H4: ∃ x3 . and (x3omega) (or (x0 = mul_SNo (eps_ x2) x3) (x0 = minus_SNo (mul_SNo (eps_ x2) x3))).
Apply H4 with 368eb.. x1SNoLt 0 x0SNoLt 0 x1368eb.. (add_SNo x0 x1).
Let x3 of type ι be given.
Assume H5: (λ x4 . and (x4omega) (or (x0 = mul_SNo (eps_ x2) x4) (x0 = minus_SNo (mul_SNo (eps_ x2) x4)))) x3.
Apply H5 with 368eb.. x1SNoLt 0 x0SNoLt 0 x1368eb.. (add_SNo x0 x1).
Assume H6: x3omega.
Assume H7: or (x0 = mul_SNo (eps_ x2) x3) (x0 = minus_SNo (mul_SNo (eps_ x2) x3)).
Apply H7 with 368eb.. x1SNoLt 0 x0SNoLt 0 x1368eb.. (add_SNo x0 x1) leaving 2 subgoals.
Assume H8: x0 = mul_SNo (eps_ x2) x3.
Assume H9: 368eb.. x1.
Apply H9 with SNoLt 0 x0SNoLt 0 x1368eb.. (add_SNo x0 x1).
Let x4 of type ι be given.
Assume H10: (λ x5 . and (x5omega) (∃ x6 . and (x6omega) (or (x1 = mul_SNo (eps_ x5) x6) (x1 = minus_SNo (mul_SNo (eps_ x5) x6))))) x4.
Apply H10 with SNoLt 0 x0SNoLt 0 x1368eb.. (add_SNo x0 x1).
Assume H11: x4omega.
Claim L12: ...
...
Assume H13: ∃ x5 . and (x5omega) (or (x1 = mul_SNo (eps_ x4) x5) (x1 = minus_SNo (mul_SNo (eps_ x4) x5))).
Apply H13 with SNoLt 0 x0SNoLt 0 x1368eb.. (add_SNo x0 x1).
Let x5 of type ι be given.
Assume H14: (λ x6 . and (x6omega) (or (x1 = mul_SNo (eps_ x4) x6) (x1 = minus_SNo (mul_SNo (eps_ x4) x6)))) x5.
Apply H14 with ......368eb.. (add_SNo ... ...).
...
...