let s be State of SCM+FSA ; :: thesis: for i being parahalting Instruction of SCM+FSA holds Exec i,(Initialize s) = IExec (Macro i),s
let i be parahalting Instruction of SCM+FSA ; :: thesis: Exec i,(Initialize s) = IExec (Macro i),s
set Mi = Macro i;
set sI = s +* (Initialized (Macro i));
set Is = Initialize s;
set IC1 = IC (Computation (s +* (Initialized (Macro i))),1);
reconsider Mi' = Macro i as parahalting Program of SCM+FSA ;
A2: ( insloc 0 in dom (Initialized (Macro i)) & (Initialized (Macro i)) . (insloc 0 ) = i ) by SCMFSA6B:31, SCMFSA6B:33;
Macro i c= Initialized (Macro i) by SCMFSA6A:26;
then ( dom (Macro i) c= dom (Initialized (Macro i)) & insloc 1 in dom (Macro i) ) by RELAT_1:25, SCMFSA6B:32;
then A3: ( insloc 1 in dom (Initialized (Macro i)) & (Initialized (Macro i)) . (insloc 1) = halt SCM+FSA ) by SCMFSA6B:33;
A4: Initialized (Macro i) c= s +* (Initialized (Macro i)) by FUNCT_4:26;

A5: now

assume A6: Result (s +* (Initialized (Macro i))) = Exec i,(s +* (Initialized (Macro i))) ; :: thesis: Exec i,(Initialize s) = IExec (Macro i),s
set X = (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )};
set Y = NAT ;
A7: dom (Exec i,(Initialize s)) = the carrier of SCM+FSA by AMI_1:79;
A8: dom (IExec (Macro i),s) = the carrier of SCM+FSA by AMI_1:79;
A9: s +* (Initialized (Macro i)) = s +* ((Macro i) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) by FUNCT_4:15
.= (s +* (Macro i)) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= ((s +* (Macro i)) +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 )) by FUNCT_4:15 ;
s +* ((intloc 0 ) .--> 1),(s +* (Macro i)) +* ((intloc 0 ) .--> 1) equal_outside NAT by AMI_1:120, FUNCT_7:106;
then Initialize s,s +* (Initialized (Macro i)) equal_outside NAT by A9, FUNCT_7:106;
then (Initialize s) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (s +* (Initialized (Macro i))) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by Th4;
then A10: (Exec i,(Initialize s)) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec i,(s +* (Initialized (Macro i)))) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by SCMFSA_3:4;
(Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} misses NAT

proof

assume (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} meets NAT ; :: thesis: contradiction
then consider x being set such that
A11: ( x in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} & x in NAT ) by XBOOLE_0:3;
A12: ( x in Int-Locations \/ FinSeq-Locations or x in {(IC SCM+FSA )} ) by A11, XBOOLE_0:def 3;

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

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

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

end;

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

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

end;

suppose A13: x = IC SCM+FSA ; :: thesis: contradiction

reconsider x = x as Instruction-Location of SCM+FSA by A11, AMI_1:def 4;
x = IC SCM+FSA by A13;
hence contradiction by AMI_1:48; :: thesis: verum

end;

end;

end;

then A14: (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} misses dom (s | NAT ) by RELAT_1:87, XBOOLE_1:63;
A15: dom (Exec i,(s +* (Initialized (Macro i)))) = the carrier of SCM+FSA by AMI_1:79;
A16: dom s = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:79, SCMFSA_2:8;
A17: NAT /\ (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) c= NAT /\ (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) ;
A18: (IExec (Macro i),s) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec i,(s +* (Initialized (Macro i)))) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) by A6, A14, FUNCT_4:76;
A19: (IExec (Macro i),s) | NAT = s | NAT by A6, A15, A16, A17, FUNCT_4:93, SCMFSA_2:8;

now

thus dom ((Exec i,(Initialize s)) | NAT ) = (dom s) /\ NAT by A7, A16, RELAT_1:90, SCMFSA_2:8; :: thesis: for x being set st x in dom ((Exec i,(Initialize s)) | NAT ) holds
((Exec i,(Initialize s)) | NAT ) . x = s . x
let x be set ; :: thesis: ( x in dom ((Exec i,(Initialize s)) | NAT ) implies ((Exec i,(Initialize s)) | NAT ) . x = s . x )
assume x in dom ((Exec i,(Initialize s)) | NAT ) ; :: thesis: ((Exec i,(Initialize s)) | NAT ) . x = s . x
then A20: x in NAT /\ (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) by A7, RELAT_1:90, SCMFSA_2:8;
then A21: x in NAT by XBOOLE_1:21;
x in NAT by A20, XBOOLE_1:21;
then reconsider x' = x as Instruction-Location of SCM+FSA by AMI_1:def 4;
thus ((Exec i,(Initialize s)) | NAT ) . x = (Exec i,(Initialize s)) . x by A21, FUNCT_1:72
.= (Initialize s) . x' by AMI_1:def 13
.= s . x by Th3 ; :: thesis: verum

end;

then (Exec i,(Initialize s)) | NAT = s | NAT by FUNCT_1:68;
then A22: (Exec i,(Initialize s)) | (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) = (IExec (Macro i),s) | (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) by A10, A18, A19, RELAT_1:185;
thus Exec i,(Initialize s) = (Exec i,(Initialize s)) | (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) by A7, RELAT_1:98, SCMFSA_2:8
.= IExec (Macro i),s by A8, A22, RELAT_1:98, SCMFSA_2:8 ; :: thesis: verum

end;

A23: Computation (s +* (Initialized (Macro i))),(0 + 1) = Following (Computation (s +* (Initialized (Macro i))),0 ) by AMI_1:14
.= Following (s +* (Initialized (Macro i))) by AMI_1:13
.= Exec ((s +* (Initialized (Macro i))) . (insloc 0 )),(s +* (Initialized (Macro i))) by FUNCT_4:26, SCMFSA6B:34
.= Exec i,(s +* (Initialized (Macro i))) by A2, A4, GRFUNC_1:8 ;
(Macro i) +* (Start-At (insloc 0 )) c= s +* (Initialized (Macro i)) by FUNCT_4:26, SCMFSA6B:8;
then A24: IC (Computation (s +* (Initialized (Macro i))),1) in dom Mi' by SCMFSA6B:def 2;

per cases ( IC (Computation (s +* (Initialized (Macro i))),1) = insloc 0 or IC (Computation (s +* (Initialized (Macro i))),1) = insloc 1 ) by A24, SCMFSA6B:32;

suppose A25: IC (Computation (s +* (Initialized (Macro i))),1) = insloc 0 ; :: thesis: Exec i,(Initialize s) = IExec (Macro i),s

then A26: CurInstr (Computation (s +* (Initialized (Macro i))),1) = (s +* (Initialized (Macro i))) . (insloc 0 ) by A23, AMI_1:def 13
.= i by A2, A4, GRFUNC_1:8 ;
Next (IC (s +* (Initialized (Macro i)))) = Next (insloc 0 ) by FUNCT_4:26, SCMFSA6B:34
.= insloc 1 ;
then A27: InsCode i in {0 ,6,7,8} by A23, A25, SCMFSA6A:23;

hereby :: thesis: verum

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

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

then A28: i = halt SCM+FSA by SCMFSA_2:122;
then s +* (Initialized (Macro i)) is halting by A26, AMI_1:def 20;
hence Exec i,(Initialize s) = IExec (Macro i),s by A5, A23, A26, A28, AMI_1:def 22; :: thesis: verum

end;

suppose A29: ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) ; :: thesis: Exec i,(Initialize s) = IExec (Macro i),s

A30: IC (s +* (Initialized (Macro i))) = IC (Exec i,(s +* (Initialized (Macro i)))) by A23, A25, FUNCT_4:26, SCMFSA6B:34;

A31: 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 A29;

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

then consider l being Instruction-Location of SCM+FSA such that
A32: i = goto l by SCMFSA_2:59;
thus (s +* (Initialized (Macro i))) . a = (Exec i,(s +* (Initialized (Macro i)))) . a by A32, SCMFSA_2:95; :: thesis: verum

end;

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

then consider l being Instruction-Location of SCM+FSA , b being Int-Location such that
A33: i = b =0_goto l by SCMFSA_2:60;
thus (s +* (Initialized (Macro i))) . a = (Exec i,(s +* (Initialized (Macro i)))) . a by A33, SCMFSA_2:96; :: thesis: verum

end;

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

then consider l being Instruction-Location of SCM+FSA , b being Int-Location such that
A34: i = b >0_goto l by SCMFSA_2:61;
thus (s +* (Initialized (Macro i))) . a = (Exec i,(s +* (Initialized (Macro i)))) . a by A34, SCMFSA_2:97; :: thesis: verum

end;

end;

end;

A35: 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 A29;

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

then consider l being Instruction-Location of SCM+FSA such that
A36: i = goto l by SCMFSA_2:59;
thus (s +* (Initialized (Macro i))) . f = (Exec i,(s +* (Initialized (Macro i)))) . f by A36, SCMFSA_2:95; :: thesis: verum

end;

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

then consider l being Instruction-Location of SCM+FSA , a being Int-Location such that
A37: i = a =0_goto l by SCMFSA_2:60;
thus (s +* (Initialized (Macro i))) . f = (Exec i,(s +* (Initialized (Macro i)))) . f by A37, SCMFSA_2:96; :: thesis: verum

end;

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

then consider l being Instruction-Location of SCM+FSA , a being Int-Location such that
A38: i = a >0_goto l by SCMFSA_2:61;
thus (s +* (Initialized (Macro i))) . f = (Exec i,(s +* (Initialized (Macro i)))) . f by A38, SCMFSA_2:97; :: thesis: verum

end;

end;

end;

for l being Instruction-Location of SCM+FSA holds (s +* (Initialized (Macro i))) . l = (Exec i,(s +* (Initialized (Macro i)))) . l by AMI_1:def 13;
then A39: s +* (Initialized (Macro i)) = Exec i,(s +* (Initialized (Macro i))) by A30, A31, A35, SCMFSA_2:86;
A40: Following (s +* (Initialized (Macro i))) = Following (Computation (s +* (Initialized (Macro i))),0 ) by AMI_1:13
.= Exec i,(s +* (Initialized (Macro i))) by A23, AMI_1:14 ;

now

let n be Element of NAT ; :: thesis: CurInstr (Computation (s +* (Initialized (Macro i))),n) <> halt SCM+FSA
Computation (s +* (Initialized (Macro i))),n = s +* (Initialized (Macro i)) by A39, A40, AMI_1:132
.= Following (Computation (s +* (Initialized (Macro i))),0 ) by A39, A40, AMI_1:13
.= Computation (s +* (Initialized (Macro i))),(0 + 1) by AMI_1:14 ;
hence CurInstr (Computation (s +* (Initialized (Macro i))),n) <> halt SCM+FSA by A26, A29, SCMFSA_2:124; :: thesis: verum

end;

then not s +* (Initialized (Macro i)) is halting by AMI_1:def 20;
hence Exec i,(Initialize s) = IExec (Macro i),s by A4, AMI_1:def 26; :: thesis: verum

end;

end;

end;

end;

suppose IC (Computation (s +* (Initialized (Macro i))),1) = insloc 1 ; :: thesis: Exec i,(Initialize s) = IExec (Macro i),s

then A41: CurInstr (Computation (s +* (Initialized (Macro i))),1) = (s +* (Initialized (Macro i))) . (insloc 1) by A23, AMI_1:def 13
.= halt SCM+FSA by A3, A4, GRFUNC_1:8 ;
then s +* (Initialized (Macro i)) is halting by AMI_1:def 20;
hence Exec i,(Initialize s) = IExec (Macro i),s by A5, A23, A41, AMI_1:def 22; :: thesis: verum

end;

end;