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 A5, XREAL_1:233 ;

then (n + 1) - 1 < LastLoc (I +* (n,i)) by A4, XREAL_1:14;

then n < LastLoc I by A3;

then (I +* (n,i)) . (LastLoc (I +* (n,i))) = I . (LastLoc I) by A3, FUNCT_7:32

.= halt SCM+FSA by COMPOS_1:def 14 ;

then A6: I +* (n,i) is halt-ending ;

I +* (n,i) is unique-halt

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 A5, XREAL_1:233 ;

then (n + 1) - 1 < LastLoc (I +* (n,i)) by A4, XREAL_1:14;

then n < LastLoc I by A3;

then (I +* (n,i)) . (LastLoc (I +* (n,i))) = I . (LastLoc I) by A3, FUNCT_7:32

.= halt SCM+FSA by COMPOS_1:def 14 ;

then A6: I +* (n,i) is halt-ending ;

I +* (n,i) is unique-halt

proof

hence
I +* (n,i) is MacroInstruction of SCM+FSA
by A6; :: thesis: verum
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))

end;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

hence
f = LastLoc (I +* (n,i))
by A2, A8, A3, COMPOS_1:def 15; :: thesis: verumassume A9:
I . f <> halt SCM+FSA
; :: thesis: contradiction

end;per cases
( f = n or f <> n )
;

end;

suppose
f = n
; :: thesis: contradiction

then
(I +* (n,i)) . f = i
by FUNCT_7:31, A8, A2;

hence contradiction by A7, COMPOS_0:def 12; :: thesis: verum

end;hence contradiction by A7, COMPOS_0:def 12; :: thesis: verum