let a be Int_position; :: thesis: for i being Integer
for m being Nat
for I being Program of SCMPDS holds
( m < (card I) + 2 iff m in dom (while>0 (a,i,I)) )
let i be Integer; :: thesis: for m being Nat
for I being Program of SCMPDS holds
( m < (card I) + 2 iff m in dom (while>0 (a,i,I)) )
let m be Nat; :: thesis: for I being Program of SCMPDS holds
( m < (card I) + 2 iff m in dom (while>0 (a,i,I)) )
let I be Program of SCMPDS; :: thesis: ( m < (card I) + 2 iff m in dom (while>0 (a,i,I)) )
card (while>0 (a,i,I)) = (card I) + 2 by Th15;
hence ( m < (card I) + 2 iff m in dom (while>0 (a,i,I)) ) by AFINSQ_1:66; :: thesis: verum