let I be MacroInstruction of SCM+FSA ; :: thesis: for i being No-StopCode Instruction of SCM+FSA
for n being Nat st n + 1 < card I holds
I +* (n,i) is MacroInstruction of SCM+FSA

let i be No-StopCode Instruction of SCM+FSA; :: thesis: for n being Nat st n + 1 < card I holds
I +* (n,i) is MacroInstruction of SCM+FSA

let n be Nat; :: thesis: ( n + 1 < card I implies I +* (n,i) is MacroInstruction of SCM+FSA )
assume A1: n + 1 < card I ; :: thesis: I +* (n,i) is MacroInstruction of SCM+FSA
set F = I +* (n,i);
A2: dom (I +* (n,i)) = dom I by FUNCT_7:30;
then A3: LastLoc (I +* (n,i)) = LastLoc I ;
A4: n + 1 < card (I +* (n,i)) by A1, A2;
A5: card (I +* (n,i)) >= 0 + 1 by NAT_1:13;
LastLoc (I +* (n,i)) = (card (I +* (n,i))) -' 1 by AFINSQ_1:70
.= (card (I +* (n,i))) - 1 by ;
then (n + 1) - 1 < LastLoc (I +* (n,i)) by ;
then n < LastLoc I by A3;
then (I +* (n,i)) . (LastLoc (I +* (n,i))) = I . () by
.= halt SCM+FSA by COMPOS_1:def 14 ;
then A6: I +* (n,i) is halt-ending ;
I +* (n,i) is unique-halt
proof
let f be Nat; :: according to COMPOS_1:def 15 :: thesis: ( not (I +* (n,i)) . f = halt SCM+FSA or not f in dom (I +* (n,i)) or f = LastLoc (I +* (n,i)) )
assume that
A7: (I +* (n,i)) . f = halt SCM+FSA and
A8: f in dom (I +* (n,i)) ; :: thesis: f = LastLoc (I +* (n,i))
now :: thesis: not I . f <> halt SCM+FSA
assume A9: I . f <> halt SCM+FSA ; :: thesis: contradiction
per cases ( f = n or f <> n ) ;
suppose f <> n ; :: thesis: contradiction
end;
end;
end;
hence f = LastLoc (I +* (n,i)) by ; :: thesis: verum
end;
hence I +* (n,i) is MacroInstruction of SCM+FSA by A6; :: thesis: verum