FDL > PVS > Number Theory > gcd > gcd_TCC1 : formula-decl

(TCC) gcd_TCC1: OBLIGATION FORALL (i:int), (j:{(jj:int) | (i = 0) = > (jj /= 0)} ) : nonempty?[posnat]({(k:posnat) | divides(k, i) AND divides(k, j)}) AND (EXISTS UB : FORALL (y:({(k:posnat) | divides(k, i) AND divides(k, j)}) ) : y < = UB)

Subproof Addresses (4 steps)
top :
top 1 :
top 1 1 :
top 1 1 1 :