let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for i being parahalting Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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 +* (Initialized (Macro i));
set pI = P +* (Macro i);
A1: Macro i c= P +* (Macro i) by FUNCT_4:26;
set Is = Initialized s;
set IC1 = IC (Comput ((P +* (Macro i)),(s +* (Initialized (Macro i))),1));
reconsider Mi = Macro i as parahalting Program of SCM+FSA ;
A2: Initialize Mi c= s +* (Initialized (Macro i)) by FUNCT_4:26, SCMFSA6B:8;
A3: IC (Comput ((P +* (Macro i)),(s +* (Initialized (Macro i))),1)) in dom Mi by SCMFSA6B:def 2, A2, FUNCT_4:26;
A4: Initialized Mi c= s +* (Initialized (Macro i)) by FUNCT_4:26;

A5: now

set Y = NAT ;
set X = (Data-Locations SCM+FSA) \/ {(IC )};
assume A6: Result ((P +* Mi),(s +* (Initialized (Macro i)))) = Exec (i,(s +* (Initialized (Macro i)))) ; :: thesis: Exec (i,(Initialized s)) = IExec (Mi,P,s)
A7: s +* ((intloc 0) .--> 1),(s +* Mi) +* ((intloc 0) .--> 1) equal_outside NAT by FUNCT_7:106, FUNCT_7:132;
A8: Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:15;
A9: Initialized Mi = Initialize (Mi +* ((intloc 0) .--> 1)) by FUNCT_4:15;
s +* (Initialized (Macro i)) = s +* (Mi +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:15
.= (s +* Mi) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= Initialize ((s +* Mi) +* ((intloc 0) .--> 1)) by FUNCT_4:15 ;
then Initialized s,s +* (Initialized (Macro i)) equal_outside NAT by A7, FUNCT_7:106, A8, A9;
then (Initialized s) | ((Data-Locations SCM+FSA) \/ {(IC )}) = (s +* (Initialized (Macro i))) | ((Data-Locations SCM+FSA) \/ {(IC )}) by COMPOS_1:175;
then A10: (Exec (i,(Initialized s))) | ((Data-Locations SCM+FSA) \/ {(IC )}) = (Exec (i,(s +* (Initialized (Macro i))))) | ((Data-Locations SCM+FSA) \/ {(IC )}) by AMISTD_2:65;
A11: NAT /\ (((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT) c= NAT /\ (((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT) ;
A12: dom (IExec (Mi,P,s)) = the carrier of SCM+FSA by PARTFUN1:def 4;
A13: dom (Exec (i,(Initialized s))) = the carrier of SCM+FSA by PARTFUN1:def 4;
A14: the carrier of SCM+FSA = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:160;
A15: dom s = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172;

now

thus dom ((Exec (i,(Initialized s))) | NAT) = (dom s) /\ NAT by A13, A15, RELAT_1:90, A14; :: thesis: for x being set st x in dom ((Exec (i,(Initialized s))) | NAT) holds
((Exec (i,(Initialized s))) | NAT) . x = s . x
let x be set ; :: thesis: ( x in dom ((Exec (i,(Initialized s))) | NAT) implies ((Exec (i,(Initialized s))) | NAT) . x = s . x )
assume x in dom ((Exec (i,(Initialized s))) | NAT) ; :: thesis: ((Exec (i,(Initialized s))) | NAT) . x = s . x
then A16: x in NAT /\ (((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT) by A13, RELAT_1:90, A14;
then reconsider x9 = x as Element of NAT by XBOOLE_1:21;
x in NAT by A16, XBOOLE_1:21;
hence ((Exec (i,(Initialized s))) | NAT) . x = (Exec (i,(Initialized s))) . x by FUNCT_1:72
.= (Initialized s) . x9 by AMI_1:def 13
.= s . x by Th3 ;
:: thesis: verum

end;

then A17: (Exec (i,(Initialized s))) | NAT = s | NAT by FUNCT_1:68;
dom (Exec (i,(s +* (Initialized (Macro i))))) = the carrier of SCM+FSA by PARTFUN1:def 4;
then A18: (IExec (Mi,P,s)) | NAT = s | NAT by A6, A15, A11, FUNCT_4:93, A14;
(Data-Locations SCM+FSA) \/ {(IC )} misses NAT

proof

assume (Data-Locations SCM+FSA) \/ {(IC )} meets NAT ; :: thesis: contradiction
then consider x being set such that
A19: x in (Data-Locations SCM+FSA) \/ {(IC )} and
A20: x in NAT by XBOOLE_0:3;
A21: ( x in Int-Locations \/ FinSeq-Locations or x in {(IC )} ) by A19, XBOOLE_0:def 3, SCMFSA_2:127;

per cases ( x in Int-Locations or x in FinSeq-Locations or x = IC ) by A21, TARSKI:def 1, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: contradiction

hence contradiction by A20, SCMFSA_2:13, XBOOLE_0:3; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: contradiction

hence contradiction by A20, SCMFSA_2:14, XBOOLE_0:3; :: thesis: verum

end;

suppose A22: x = IC ; :: thesis: contradiction

reconsider x = x as Element of NAT by A20;
x = IC by A22;
hence contradiction by COMPOS_1:3; :: thesis: verum

end;

end;

end;

then (Data-Locations SCM+FSA) \/ {(IC )} misses dom (s | NAT) by RELAT_1:87, XBOOLE_1:63;
then (IExec (Mi,P,s)) | ((Data-Locations SCM+FSA) \/ {(IC )}) = (Exec (i,(s +* (Initialized (Macro i))))) | ((Data-Locations SCM+FSA) \/ {(IC )}) by A6, FUNCT_4:76;
then A23: (Exec (i,(Initialized s))) | (((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT) = (IExec (Mi,P,s)) | (((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT) by A10, A18, A17, RELAT_1:185;
thus Exec (i,(Initialized s)) = (Exec (i,(Initialized s))) | (((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT) by A13, RELAT_1:98, A14
.= IExec (Mi,P,s) by A12, A23, RELAT_1:98, A14 ; :: thesis: verum

end;

A24: 1 in dom Mi by COMPOS_1:147;
A25: 0 in dom Mi by COMPOS_1:147;
A26: Mi . 0 = i by COMPOS_1:148;
A27: (P +* Mi) /. (IC (s +* (Initialized (Macro i)))) = (P +* Mi) . (IC (s +* (Initialized (Macro i)))) by PBOOLE:158;
A28: Comput ((P +* Mi),(s +* (Initialized (Macro i))),(0 + 1)) = Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialized (Macro i))),0))) by EXTPRO_1:4
.= Following ((P +* Mi),(s +* (Initialized (Macro i)))) by EXTPRO_1:3
.= Exec (((P +* (Macro i)) . 0),(s +* (Initialized (Macro i)))) by A27, FUNCT_4:26, SCMFSA6B:34
.= Exec (i,(s +* (Initialized (Macro i)))) by A26, GRFUNC_1:8, A1, A25 ;

per cases ( IC (Comput ((P +* (Macro i)),(s +* (Initialized (Macro i))),1)) = 0 or IC (Comput ((P +* (Macro i)),(s +* (Initialized (Macro i))),1)) = 1 ) by A3, COMPOS_1:147;

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

then A30: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialized (Macro i))),1))) = (P +* Mi) . 0 by PBOOLE:158
.= i by A26, FUNCT_4:14, A25 ;
succ (IC (s +* (Initialized (Macro i)))) = succ 0 by FUNCT_4:26, SCMFSA6B:34
.= 1 ;
then A31: InsCode i in {0,6,7,8} by A28, A29, SCMFSA6A:23;

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:122;
then P +* Mi halts_on s +* (Initialized (Macro i)) by A30, EXTPRO_1:30;
hence Exec (i,(Initialized s)) = IExec ((Macro i),P,s) by A5, A28, A30, A32, EXTPRO_1:def 8; :: 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 +* (Initialized (Macro i))) . b₁ = (Exec (i,(s +* (Initialized (Macro i))))) . b₁

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

suppose InsCode i = 6 ; :: thesis: (s +* (Initialized (Macro i))) . b₁ = (Exec (i,(s +* (Initialized (Macro i))))) . b₁

then ex l being Element of NAT st i = goto l by SCMFSA_2:59;
hence (s +* (Initialized (Macro i))) . a = (Exec (i,(s +* (Initialized (Macro i))))) . a by SCMFSA_2:95; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (s +* (Initialized (Macro i))) . b₁ = (Exec (i,(s +* (Initialized (Macro i))))) . b₁

then ex l being Element of NAT ex b being Int-Location st i = b =0_goto l by SCMFSA_2:60;
hence (s +* (Initialized (Macro i))) . a = (Exec (i,(s +* (Initialized (Macro i))))) . a by SCMFSA_2:96; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: (s +* (Initialized (Macro i))) . b₁ = (Exec (i,(s +* (Initialized (Macro i))))) . b₁

then ex l being Element of NAT ex b being Int-Location st i = b >0_goto l by SCMFSA_2:61;
hence (s +* (Initialized (Macro i))) . a = (Exec (i,(s +* (Initialized (Macro i))))) . a by SCMFSA_2:97; :: thesis: verum

end;

end;

end;

A35: for l being Element of NAT holds (s +* (Initialized (Macro i))) . l = (Exec (i,(s +* (Initialized (Macro i))))) . l by AMI_1:def 13;

A36: now

let f be FinSeq-Location ; :: thesis: (s +* (Initialized (Macro i))) . b₁ = (Exec (i,(s +* (Initialized (Macro i))))) . b₁

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

suppose InsCode i = 6 ; :: thesis: (s +* (Initialized (Macro i))) . b₁ = (Exec (i,(s +* (Initialized (Macro i))))) . b₁

then ex l being Element of NAT st i = goto l by SCMFSA_2:59;
hence (s +* (Initialized (Macro i))) . f = (Exec (i,(s +* (Initialized (Macro i))))) . f by SCMFSA_2:95; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (s +* (Initialized (Macro i))) . b₁ = (Exec (i,(s +* (Initialized (Macro i))))) . b₁

then ex l being Element of NAT ex a being Int-Location st i = a =0_goto l by SCMFSA_2:60;
hence (s +* (Initialized (Macro i))) . f = (Exec (i,(s +* (Initialized (Macro i))))) . f by SCMFSA_2:96; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: (s +* (Initialized (Macro i))) . b₁ = (Exec (i,(s +* (Initialized (Macro i))))) . b₁

then ex l being Element of NAT ex a being Int-Location st i = a >0_goto l by SCMFSA_2:61;
hence (s +* (Initialized (Macro i))) . f = (Exec (i,(s +* (Initialized (Macro i))))) . f by SCMFSA_2:97; :: thesis: verum

end;

end;

end;

IC (s +* (Initialized (Macro i))) = IC (Exec (i,(s +* (Initialized (Macro i))))) by A28, A29, FUNCT_4:26, SCMFSA6B:34;
then A37: s +* (Initialized (Macro i)) = Exec (i,(s +* (Initialized (Macro i)))) by A34, A36, A35, SCMFSA_2:86;
A38: Following ((P +* Mi),(s +* (Initialized (Macro i)))) = Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialized (Macro i))),0))) by EXTPRO_1:3
.= Exec (i,(s +* (Initialized (Macro i)))) by A28, EXTPRO_1:4 ;

now

let n be Element of NAT ; :: thesis: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialized (Macro i))),n))) <> halt SCM+FSA
Comput ((P +* Mi),(s +* (Initialized (Macro i))),n) = s +* (Initialized (Macro i)) by A37, A38, EXTPRO_1:27
.= Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialized (Macro i))),0))) by A37, A38, EXTPRO_1:3
.= Comput ((P +* Mi),(s +* (Initialized (Macro i))),(0 + 1)) by EXTPRO_1:4 ;
hence CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialized (Macro i))),n))) <> halt SCM+FSA by A30, A33, SCMFSA_2:124; :: thesis: verum

end;

then A39: not P +* Mi halts_on s +* (Initialized (Macro i)) by EXTPRO_1:30;
A40: ProgramPart (Initialized Mi) = Mi by SCMFSA6A:33;
Mi c= P +* Mi by FUNCT_4:26;
hence Exec (i,(Initialized s)) = IExec ((Macro i),P,s) by A4, EXTPRO_1:def 10, A39, A40; :: thesis: verum

end;

end;

end;

end;

suppose A41: IC (Comput ((P +* (Macro i)),(s +* (Initialized (Macro i))),1)) = 1 ; :: thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)

A42: Mi c= Initialized Mi by SCMFSA6A:26;
(Initialized Mi) . 1 = halt SCM+FSA by SCMFSA6B:33;
then A43: Mi . 1 = halt SCM+FSA by A42, A24, GRFUNC_1:8;
A44: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialized (Macro i))),1))) = (P +* Mi) . 1 by A41, PBOOLE:158
.= halt SCM+FSA by A43, GRFUNC_1:8, A1, A24 ;
then P +* Mi halts_on s +* (Initialized (Macro i)) by EXTPRO_1:30;
hence Exec (i,(Initialized s)) = IExec ((Macro i),P,s) by A5, A28, A44, EXTPRO_1:def 8; :: thesis: verum

end;

end;