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:
gcd_reln
x0
x1
x2
.
Apply H0 with
gcd_reln
x0
(
minus_SNo
x1
)
x2
.
Assume H1:
and
(
divides_int
x2
x0
)
(
divides_int
x2
x1
)
.
Apply H1 with
(
∀ x3 .
divides_int
x3
x0
⟶
divides_int
x3
x1
⟶
SNoLe
x3
x2
)
⟶
gcd_reln
x0
(
minus_SNo
x1
)
x2
.
Assume H2:
divides_int
x2
x0
.
Assume H3:
divides_int
x2
x1
.
Assume H4:
∀ x3 .
divides_int
x3
x0
⟶
divides_int
x3
x1
⟶
SNoLe
x3
x2
.
Apply H3 with
and
(
and
(
divides_int
x2
x0
)
(
divides_int
x2
(
minus_SNo
x1
)
)
)
(
∀ x3 .
divides_int
x3
x0
⟶
divides_int
x3
(
minus_SNo
x1
)
⟶
SNoLe
x3
x2
)
.
Assume H5:
and
(
x2
∈
int
)
(
x1
∈
int
)
.
Assume H6:
∃ x3 .
and
(
x3
∈
int
)
(
mul_SNo
x2
x3
=
x1
)
.
Apply H5 with
and
(
and
(
divides_int
x2
x0
)
(
divides_int
x2
(
minus_SNo
x1
)
)
)
(
∀ x3 .
divides_int
x3
x0
⟶
divides_int
x3
(
minus_SNo
x1
)
⟶
SNoLe
x3
x2
)
.
Assume H7:
x2
∈
int
.
Assume H8:
x1
∈
int
.
Apply and3I with
divides_int
x2
x0
,
divides_int
x2
(
minus_SNo
x1
)
,
∀ x3 .
divides_int
x3
x0
⟶
divides_int
x3
(
minus_SNo
x1
)
⟶
SNoLe
x3
x2
leaving 3 subgoals.
The subproof is completed by applying H2.
Apply divides_int_minus_SNo with
x2
,
x1
.
The subproof is completed by applying H3.
Let x3 of type
ι
be given.
Assume H9:
divides_int
x3
x0
.
Assume H10:
divides_int
x3
(
minus_SNo
x1
)
.
Apply H4 with
x3
leaving 2 subgoals.
The subproof is completed by applying H9.
Apply minus_SNo_invol with
x1
,
λ x4 x5 .
divides_int
x3
x4
leaving 2 subgoals.
Apply int_SNo with
x1
.
The subproof is completed by applying H8.
Apply divides_int_minus_SNo with
x3
,
minus_SNo
x1
.
The subproof is completed by applying H10.
■