let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for i being sequential Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
let P be Instruction-Sequence of SCM+FSA; :: thesis: for i being sequential Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
let i be sequential Instruction of SCM+FSA; :: thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
set Mi = Macro i;
set sI = s +* (Initialize ((intloc 0) .--> 1));
set pI = P +* (Macro i);
A1: Macro i c= P +* (Macro i) by FUNCT_4:25;
set Is = Initialized s;
set IC1 = IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1));
reconsider Mi = Macro i as parahalting Program of SCM+FSA ;
IC (s +* (Initialize ((intloc 0) .--> 1))) = 0 by MEMSTR_0:def 11;
then IC (s +* (Initialize ((intloc 0) .--> 1))) in dom Mi by AFINSQ_1:65;
then A2: IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) in dom Mi by A1, AMISTD_1:21;
A3: 1 in dom Mi by COMPOS_1:60;
A4: 0 in dom Mi by COMPOS_1:60;
A5: Mi . 0 = i by COMPOS_1:58;
A6: IC (s +* (Initialize ((intloc 0) .--> 1))) = 0 by MEMSTR_0:def 11;
A7: Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),(0 + 1)) = Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),0))) by EXTPRO_1:3
.= Exec (((P +* (Macro i)) . 0),(s +* (Initialize ((intloc 0) .--> 1)))) by A6, PBOOLE:143
.= Exec (i,(s +* (Initialize ((intloc 0) .--> 1)))) by A5, A1, A4, GRFUNC_1:2 ;

per cases ( IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 0 or IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 1 ) by A2, COMPOS_1:60;

suppose A8: IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 0 ; :: thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)

then A9: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) = (P +* Mi) . 0 by PBOOLE:143
.= i by A5, A4, FUNCT_4:13 ;
IC (s +* (Initialize ((intloc 0) .--> 1))) = 0 by A6;
then A10: InsCode i in {0,6,7,8} by A7, A8, SCMFSA6A:3;

hereby :: thesis: verum

per cases ( InsCode i = 0 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A10, ENUMSET1:def 2;

suppose InsCode i = 0 ; :: thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)

then A11: i = halt SCM+FSA by SCMFSA_2:95;
then P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1)) by A9, EXTPRO_1:29;
hence Exec (i,(Initialized s)) = IExec ((Macro i),P,s) by A7, A9, A11, EXTPRO_1:def 9; :: thesis: verum

end;

suppose A12: ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) ; :: thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)

A13: now :: thesis: for a being Int-Location holds (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a

let a be Int-Location; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

per cases ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A12;

suppose InsCode i = 6 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Nat st i = goto l by SCMFSA_2:35;
hence (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a ; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Nat ex b being Int-Location st i = b =0_goto l by SCMFSA_2:36;
hence (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a ; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Nat ex b being Int-Location st i = b >0_goto l by SCMFSA_2:37;
hence (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a ; :: thesis: verum

end;

end;

end;

A14: now :: thesis: for f being FinSeq-Location holds (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f

let f be FinSeq-Location ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

per cases ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A12;

suppose InsCode i = 6 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Nat st i = goto l by SCMFSA_2:35;
hence (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f ; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Nat ex a being Int-Location st i = a =0_goto l by SCMFSA_2:36;
hence (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f ; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Nat ex a being Int-Location st i = a >0_goto l by SCMFSA_2:37;
hence (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f ; :: thesis: verum

end;

end;

end;

A15: Following ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1)))) = Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),0)))
.= Exec (i,(s +* (Initialize ((intloc 0) .--> 1)))) by A7, EXTPRO_1:3 ;
A16: InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
for n being Nat holds CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),n))) <> halt SCM+FSA by A9, A12, A13, A14, A7, A8, A6, A15, A16, AMISTD_2:11, SCMFSA_2:104;
then A17: not P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1)) ;
Mi c= P +* Mi by FUNCT_4:25;
hence Exec (i,(Initialized s)) = IExec ((Macro i),P,s) by A17, AMISTD_1:def 11; :: thesis: verum

end;

end;

end;

end;

suppose A18: IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 1 ; :: thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)

A19: Mi . 1 = halt SCM+FSA by COMPOS_1:59;
A20: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) = (P +* Mi) . 1 by A18, PBOOLE:143
.= halt SCM+FSA by A19, A1, A3, GRFUNC_1:2 ;
then P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:29;
hence Exec (i,(Initialized s)) = IExec ((Macro i),P,s) by A7, A20, EXTPRO_1:def 9; :: thesis: verum

end;

end;