Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: x1int.
Assume H1: gcd_reln x0 (add_SNo x1 (minus_SNo x0)) x2.
Apply H1 with gcd_reln x0 x1 x2.
Assume H2: and (divides_int x2 x0) (divides_int x2 (add_SNo x1 (minus_SNo x0))).
Apply H2 with (∀ x3 . divides_int x3 x0divides_int x3 (add_SNo x1 (minus_SNo x0))SNoLe x3 x2)gcd_reln x0 x1 x2.
Assume H3: divides_int x2 x0.
Assume H4: divides_int x2 (add_SNo x1 (minus_SNo x0)).
Assume H5: ∀ x3 . divides_int x3 x0divides_int x3 (add_SNo x1 (minus_SNo x0))SNoLe x3 x2.
Apply H3 with gcd_reln x0 x1 x2.
Assume H6: and (x2int) (x0int).
Assume H7: ∃ x3 . and (x3int) (mul_SNo x2 x3 = x0).
Apply H6 with gcd_reln x0 x1 x2.
Assume H8: x2int.
Assume H9: x0int.
Apply and3I with divides_int x2 x0, divides_int x2 x1, ∀ x3 . divides_int x3 x0divides_int x3 x1SNoLe x3 x2 leaving 3 subgoals.
The subproof is completed by applying H3.
Apply add_SNo_minus_R2' with x1, x0, λ x3 x4 . divides_int x2 x3 leaving 3 subgoals.
Apply int_SNo with x1.
The subproof is completed by applying H0.
Apply int_SNo with x0.
The subproof is completed by applying H9.
Apply divides_int_add_SNo with x2, add_SNo x1 (minus_SNo x0), x0 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Assume H10: divides_int x3 x0.
Assume H11: divides_int x3 x1.
Apply H5 with x3 leaving 2 subgoals.
The subproof is completed by applying H10.
Apply divides_int_add_SNo with x3, x1, minus_SNo x0 leaving 2 subgoals.
The subproof is completed by applying H11.
Apply divides_int_minus_SNo with x3, x0.
The subproof is completed by applying H10.