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

gcd_def: LEMMA ((i /= 0) OR (j /= 0)) IMPLIES ((gcd(i, j) = nn) IFF ((divides(nn, i) AND divides(nn, j)) AND (FORALL mm : (divides(mm, i) AND divides(mm, j)) IMPLIES (mm < = nn))))

Subproof Addresses (20 steps)
top :
top 1 :
top 1 1 :
top 1 1 1 :
top 1 1 1 1 :
top 1 1 1 1 1 :
top 1 1 1 1 1 1 :
top 1 1 1 1 1 1 1 :
top 1 1 1 1 1 1 1 1 :
top 1 2 :
top 1 2 1 :
top 1 2 1 1 :
top 1 2 1 1 1 :
top 1 2 1 1 1 1 :
top 1 2 1 1 1 1 1 :
top 1 2 1 1 1 1 1 1 :
top 1 2 1 1 1 1 1 1 1 :
top 1 2 1 1 1 2 :
top 1 2 1 1 1 2 1 :
top 1 2 1 1 1 2 1 1 :