FDL > PVS > Number Theory > gcd > gcd TCC1 > pf:gcd TCC1 > 1 > 1 (2 nodes)

Conclusion

1. EXISTS UB : FORALL y:({k:posnat | divides(k, i!1) AND divides(k, j!1)}) : y < = UB

Tactic
 ASSERT
Premise 1.   (has proof of 1 step)

1. EXISTS UB : FORALL y:({k:posnat | divides(k, i!1) AND divides(k, j!1)}) : y < = UB