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

Conclusion

-1. gcd(i!1, j!1) = nn!1
-2. divides(mm!1, i!1)
-3. divides(mm!1, j!1)
-4. (i!1 /= 0) OR (j!1 /= 0)

1. mm!1 < = nn!1

Tactic
 LEMMA "gcd_is_max"
Premise 1.   (has proof of 3 steps)

-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