let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for i being parahalting 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 parahalting Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
let i be parahalting 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 ;
A3: IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) in dom Mi by A1, AMISTD_1:def 10;
A24: 1 in dom Mi by COMPOS_1:60;
A25: 0 in dom Mi by COMPOS_1:60;
A26: Mi . 0 = i by COMPOS_1:58;
XX: IC (s +* (Initialize ((intloc 0) .--> 1))) = 0 by MEMSTR_0:def 8;
A28: 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
.= Following ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1)))) by EXTPRO_1:2
.= Exec (((P +* (Macro i)) . 0),(s +* (Initialize ((intloc 0) .--> 1)))) by XX, PBOOLE:143
.= Exec (i,(s +* (Initialize ((intloc 0) .--> 1)))) by A26, A1, A25, 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 A3, COMPOS_1:60;

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

then A30: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) = (P +* Mi) . 0 by PBOOLE:143
.= i by A26, A25, FUNCT_4:13 ;
succ (IC (s +* (Initialize ((intloc 0) .--> 1)))) = 1 by XX;
then A31: InsCode i in {0,6,7,8} by A28, A29, SCMFSA6A:3;

hereby :: thesis: verum

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

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

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

end;

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

A34: now

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

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

then ex l being Element of NAT st i = goto l by SCMFSA_2:35;
hence (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a by SCMFSA_2:69; :: 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 Element of 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 by SCMFSA_2:70; :: 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 Element of 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 by SCMFSA_2:71; :: thesis: verum

end;

end;

end;

A36: now

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

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

then ex l being Element of NAT st i = goto l by SCMFSA_2:35;
hence (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f by SCMFSA_2:69; :: 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 Element of 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 by SCMFSA_2:70; :: 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 Element of 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 by SCMFSA_2:71; :: thesis: verum

end;

end;

end;

A38: Following ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1)))) = Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),0))) by EXTPRO_1:2
.= Exec (i,(s +* (Initialize ((intloc 0) .--> 1)))) by A28, EXTPRO_1:3 ;
for n being Element of NAT holds CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),n))) <> halt SCM+FSA by A30, A33, SCMFSA_2:97, A34, A36, A28, A29, XX, A38, AMISTD_2:11, SCMFSA_2:104;
then A39: not P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:29;
Mi c= P +* Mi by FUNCT_4:25;
hence Exec (i,(Initialized s)) = IExec ((Macro i),P,s) by A39, AMISTD_1:def 11; :: thesis: verum

end;

end;

end;

end;

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

A43: Mi . 1 = halt SCM+FSA by COMPOS_1:59;
A44: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) = (P +* Mi) . 1 by A41, PBOOLE:143
.= halt SCM+FSA by A43, A1, A24, 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 A28, A44, EXTPRO_1:def 9; :: thesis: verum

end;

end;