Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: diadic_rational_p x0.
Apply H0 with diadic_rational_p x1diadic_rational_p (add_SNo x0 x1).
Let x2 of type ι be given.
Assume H1: (λ x3 . and (x3omega) (∃ x4 . and (x4int) (x0 = mul_SNo (eps_ x3) x4))) x2.
Apply H1 with diadic_rational_p x1diadic_rational_p (add_SNo x0 x1).
Assume H2: x2omega.
Claim L3: ...
...
Assume H4: ∃ x3 . and (x3int) (x0 = mul_SNo (eps_ x2) x3).
Apply H4 with diadic_rational_p x1diadic_rational_p (add_SNo x0 x1).
Let x3 of type ι be given.
Assume H5: (λ x4 . and (x4int) (x0 = mul_SNo (eps_ x2) x4)) x3.
Apply H5 with diadic_rational_p x1diadic_rational_p (add_SNo x0 x1).
Assume H6: x3int.
Assume H7: x0 = mul_SNo (eps_ x2) x3.
Assume H8: diadic_rational_p x1.
Apply H8 with diadic_rational_p (add_SNo x0 x1).
Let x4 of type ι be given.
Assume H9: (λ x5 . and (x5omega) (∃ x6 . and (x6int) (x1 = mul_SNo (eps_ x5) x6))) x4.
Apply H9 with diadic_rational_p (add_SNo x0 x1).
Assume H10: x4omega.
Claim L11: ...
...
Assume H12: ∃ x5 . and (x5int) (x1 = mul_SNo (eps_ x4) x5).
Apply H12 with diadic_rational_p (add_SNo x0 x1).
Let x5 of type ι be given.
Assume H13: (λ x6 . and (x6int) (x1 = mul_SNo (eps_ x4) x6)) x5.
Apply H13 with diadic_rational_p (add_SNo x0 x1).
Assume H14: x5int.
Assume H15: x1 = mul_SNo (eps_ x4) x5.
Let x6 of type ο be given.
Assume H16: ∀ x7 . and (x7omega) (∃ x8 . and (x8int) (add_SNo x0 x1 = mul_SNo (eps_ x7) x8))x6.
Apply H16 with add_SNo x2 x4.
Apply andI with add_SNo x2 x4omega, ∃ x7 . and (x7int) (add_SNo x0 x1 = mul_SNo (eps_ (add_SNo x2 x4)) x7) leaving 2 subgoals.
Apply add_SNo_In_omega with x2, x4 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H10.
Let x7 of type ο be given.
Assume H17: ∀ x8 . and (x8int) (add_SNo x0 x1 = mul_SNo (eps_ (add_SNo x2 x4)) x8)x7.
Apply H17 with add_SNo (mul_SNo (exp_SNo_nat 2 x4) x3) (mul_SNo (exp_SNo_nat 2 x2) x5).
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Apply andI with add_SNo (mul_SNo (exp_SNo_nat 2 x4) x3) (mul_SNo (exp_SNo_nat 2 x2) x5)int, add_SNo x0 x1 = mul_SNo (eps_ (add_SNo x2 x4)) (add_SNo (mul_SNo (exp_SNo_nat 2 x4) x3) (mul_SNo (exp_SNo_nat 2 x2) x5)) leaving 2 subgoals.
Apply int_add_SNo with mul_SNo ... ..., ... leaving 2 subgoals.
...
...
...