let a be Int-Location ; :: thesis: for I being Program of SCM+FSA
for k being Element of NAT st k < (card I) + 6 holds
k in dom (while=0 (a,I))
let I be Program of SCM+FSA; :: thesis: for k being Element of NAT st k < (card I) + 6 holds
k in dom (while=0 (a,I))
let k be Element of NAT ; :: thesis: ( k < (card I) + 6 implies k in dom (while=0 (a,I)) )
assume A1: k < (card I) + 6 ; :: thesis: k in dom (while=0 (a,I))
card (while=0 (a,I)) = (card I) + 6 by Th4;
hence k in dom (while=0 (a,I)) by A1, AFINSQ_1:70; :: thesis: verum