Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: x0 = 0∀ x1 : ο . x1.
Claim L2: ...
...
Apply nat_ind with λ x1 . ∃ x2 . and (x2int) (and (SNoLe (mul_SNo 2 (abs_SNo x2)) x0) (divides_nat x0 (add_SNo x1 (minus_SNo x2)))) leaving 2 subgoals.
Let x1 of type ο be given.
Assume H3: ∀ x2 . and (x2int) (and (SNoLe (mul_SNo 2 (abs_SNo x2)) x0) (divides_nat x0 (add_SNo 0 (minus_SNo x2))))x1.
Apply H3 with 0.
Apply andI with 0int, and (SNoLe (mul_SNo 2 (abs_SNo 0)) x0) (divides_nat x0 (add_SNo 0 (minus_SNo 0))) leaving 2 subgoals.
Apply nat_p_int with 0.
The subproof is completed by applying nat_0.
Apply andI with SNoLe (mul_SNo 2 (abs_SNo 0)) x0, divides_nat x0 (add_SNo 0 (minus_SNo 0)) leaving 2 subgoals.
Apply abs_SNo_0 with λ x2 x3 . SNoLe (mul_SNo 2 x3) x0.
Apply mul_SNo_zeroR with 2, λ x2 x3 . SNoLe x3 x0 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply unknownprop_72fc13f59561a486e7f04b4e6ad6c40ec1d48eeac6e68c47cb50fa618c19e933 with x0.
The subproof is completed by applying H0.
Apply minus_SNo_0 with λ x2 x3 . divides_nat x0 (add_SNo 0 x3).
Apply add_SNo_0L with 0, λ x2 x3 . divides_nat x0 x3 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply unknownprop_94b9b73b1207350973a964cfd79fac000c8d717e12b3149994867d613d318c69 with x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H3: nat_p x1.
Assume H4: ∃ x2 . and (x2int) (and (SNoLe (mul_SNo 2 (abs_SNo x2)) x0) (divides_nat x0 (add_SNo x1 (minus_SNo x2)))).
Apply H4 with ∃ x2 . and (x2int) (and (SNoLe (mul_SNo 2 (abs_SNo x2)) x0) (divides_nat x0 (add_SNo (ordsucc x1) (minus_SNo x2)))).
Let x2 of type ι be given.
Assume H5: (λ x3 . and (x3int) (and (SNoLe (mul_SNo 2 (abs_SNo x3)) x0) (divides_nat x0 (add_SNo x1 (minus_SNo x3))))) x2.
Apply H5 with ∃ x3 . and (x3int) (and (SNoLe (mul_SNo 2 (abs_SNo x3)) x0) (divides_nat x0 (add_SNo (ordsucc x1) (minus_SNo x3)))).
Assume H6: x2int.
Assume H7: and (SNoLe (mul_SNo 2 (abs_SNo x2)) x0) (divides_nat x0 (add_SNo x1 (minus_SNo x2))).
Apply H7 with ∃ x3 . and (x3int) (and (SNoLe (mul_SNo 2 (abs_SNo x3)) x0) (divides_nat x0 (add_SNo (ordsucc x1) (minus_SNo x3)))).
Assume H8: SNoLe (mul_SNo 2 (abs_SNo x2)) x0.
Assume H9: divides_nat x0 (add_SNo x1 (minus_SNo x2)).
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Apply SNoLtLe_or with x2, 0, ∃ x3 . and (x3int) (and (SNoLe (mul_SNo 2 (abs_SNo x3)) x0) (divides_nat x0 (add_SNo (ordsucc x1) (minus_SNo x3)))) leaving 4 subgoals.
Apply int_SNo with x2.
The subproof is completed by applying H6.
The subproof is completed by applying SNo_0.
Assume H14: SNoLt x2 0.
...
...