let a be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA

for k being Nat st k < 5 holds

k in dom (while>0 (a,I))

let I be MacroInstruction of SCM+FSA ; :: thesis: for k being Nat st k < 5 holds

k in dom (while>0 (a,I))

let k be Nat; :: thesis: ( k < 5 implies k in dom (while>0 (a,I)) )

A1: 5 <= (card I) + 5 by NAT_1:11;

A2: card (while>0 (a,I)) = (card I) + 5 by Th4;

assume k < 5 ; :: thesis: k in dom (while>0 (a,I))

then k < (card I) + 5 by A1, XXREAL_0:2;

hence k in dom (while>0 (a,I)) by A2, AFINSQ_1:66; :: thesis: verum

for k being Nat st k < 5 holds

k in dom (while>0 (a,I))

let I be MacroInstruction of SCM+FSA ; :: thesis: for k being Nat st k < 5 holds

k in dom (while>0 (a,I))

let k be Nat; :: thesis: ( k < 5 implies k in dom (while>0 (a,I)) )

A1: 5 <= (card I) + 5 by NAT_1:11;

A2: card (while>0 (a,I)) = (card I) + 5 by Th4;

assume k < 5 ; :: thesis: k in dom (while>0 (a,I))

then k < (card I) + 5 by A1, XXREAL_0:2;

hence k in dom (while>0 (a,I)) by A2, AFINSQ_1:66; :: thesis: verum