let a be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA
for k being Nat st k < 5 holds
(card I) + k in dom (while>0 (a,I))
let I be MacroInstruction of SCM+FSA ; :: thesis: for k being Nat st k < 5 holds
(card I) + k in dom (while>0 (a,I))
let k be Nat; :: thesis: ( k < 5 implies (card I) + k in dom (while>0 (a,I)) )
assume A1: k < 5 ; :: thesis: (card I) + k in dom (while>0 (a,I))
card (while>0 (a,I)) = (card I) + 5 by Th4;
hence (card I) + k in dom (while>0 (a,I)) by A1, AFINSQ_1:66, XREAL_1:6; :: thesis: verum