Conclusion
-1.
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
>
0
-2.
divides(max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}),
i!1)
-3.
divides(max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}),
j!1)
-4.
FORALL
x
:
(divides(x,
i!1)
AND
divides(x,
j!1))
IMPLIES
(x
<
=
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}))
-5.
(i!1
/=
0)
OR
(j!1
/=
0)
-6.
divides(kk!1,
i!1)
-7.
divides(kk!1,
j!1)
1.
kk!1
<
=
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
Tactic
INST?
Premise 1. (has proof of 1 step)
-1.
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
>
0
-2.
divides(max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}),
i!1)
-3.
divides(max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}),
j!1)
-4.
(divides(kk!1,
i!1)
AND
divides(kk!1,
j!1))
IMPLIES
(kk!1
<
=
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}))
-5.
(i!1
/=
0)
OR
(j!1
/=
0)
-6.
divides(kk!1,
i!1)
-7.
divides(kk!1,
j!1)
1.
kk!1
<
=
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
Premise 2. (has proof of 1 step)
-1.
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
>
0
-2.
divides(max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}),
i!1)
-3.
divides(max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)}),
j!1)
-4.
(i!1
/=
0)
OR
(j!1
/=
0)
-5.
divides(kk!1,
i!1)
-6.
divides(kk!1,
j!1)
1.
(kk!1
>
=
0)
AND
(kk!1
>
0)
2.
kk!1
<
=
max({k:posnat
|
divides(k,
i!1)
AND
divides(k,
j!1)})
