FDL > PVS > Number Theory > gcd > gcd def > pf:gcd def > 1 > 1 > 1 > 1 > 1 > 1 (3 nodes)

Conclusion

-1. FORALL i:int, j:int, kk:nzint : (((i /= 0) OR (j /= 0)) AND divides(kk, i) AND divides(kk, j)) IMPLIES (kk < = gcd(i, j))
-2. gcd(i!1, j!1) = nn!1
-3. divides(mm!1, i!1)
-4. divides(mm!1, j!1)
-5. (i!1 /= 0) OR (j!1 /= 0)

1. mm!1 < = nn!1

Tactic
 INST?
Premise 1.   (has proof of 2 steps)

-1. FORALL kk:nzint : (((i!1 /= 0) OR (j!1 /= 0)) AND divides(kk, i!1) AND divides(kk, j!1)) IMPLIES (kk < = gcd(i!1, j!1))
-2. gcd(i!1, j!1) = nn!1
-3. divides(mm!1, i!1)
-4. divides(mm!1, j!1)
-5. (i!1 /= 0) OR (j!1 /= 0)

1. mm!1 < = nn!1