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