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 Th4;

hence ( m < (card I) + 2 iff m in dom (while<0 (a,i,I)) ) by AFINSQ_1:66; :: thesis: verum

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 Th4;

hence ( m < (card I) + 2 iff m in dom (while<0 (a,i,I)) ) by AFINSQ_1:66; :: thesis: verum