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.. x1368eb.. (mul_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.. x1368eb.. (mul_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.. x1368eb.. (mul_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.. x1368eb.. (mul_SNo x0 x1).
Assume H6: x3omega.
Claim L7: ...
...
Claim L8: ...
...
Assume H9: or (x0 = mul_SNo (eps_ x2) x3) (x0 = minus_SNo (mul_SNo (eps_ x2) x3)).
Apply H9 with 368eb.. x1368eb.. (mul_SNo x0 x1) leaving 2 subgoals.
Assume H10: x0 = mul_SNo (eps_ x2) x3.
Assume H11: 368eb.. x1.
Apply H11 with 368eb.. (mul_SNo x0 x1).
Let x4 of type ι be given.
Assume H12: (λ x5 . and (x5omega) (∃ x6 . and (x6omega) (or (x1 = mul_SNo (eps_ x5) x6) (x1 = minus_SNo (mul_SNo (eps_ x5) x6))))) x4.
Apply H12 with 368eb.. (mul_SNo x0 x1).
Assume H13: x4omega.
Assume H14: ∃ x5 . and (x5omega) (or (x1 = mul_SNo (eps_ x4) x5) (x1 = minus_SNo (mul_SNo (eps_ x4) x5))).
Apply H14 with 368eb.. (mul_SNo x0 x1).
Let x5 of type ι be given.
Assume H15: (λ x6 . and (x6omega) (or (x1 = mul_SNo (eps_ x4) x6) (x1 = minus_SNo (mul_SNo (eps_ x4) x6)))) x5.
Apply H15 with 368eb.. (mul_SNo x0 x1).
Assume H16: x5omega.
Claim L17: ...
...
Assume H18: or (x1 = mul_SNo (eps_ x4) x5) (x1 = minus_SNo (mul_SNo (eps_ x4) x5)).
Apply H18 with 368eb.. (mul_SNo x0 x1) leaving 2 subgoals.
Assume H19: x1 = mul_SNo (eps_ x4) x5.
Let x6 of type ο be given.
Assume H20: ∀ x7 . and (x7omega) (∃ x8 . and (x8omega) (or (mul_SNo x0 x1 = mul_SNo (eps_ x7) x8) (mul_SNo ... ... = ...)))x6.
...
...
...