let s be State of SCM+FSA; :: thesis: for i being parahalting Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),s)
let i be parahalting Instruction of SCM+FSA; :: thesis: Exec (i,(Initialized s)) = IExec ((Macro i),s)
set Mi = Macro i;
set sI = s +* (Initialized (Macro i));
set Is = Initialized s;
set IC1 = IC (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1));
reconsider Mi9 = Macro i as parahalting Program of SCM+FSA ;
A1: 0 in dom (Initialized (Macro i)) by COMPOS_1:146, SCMFSA6B:31;
(Macro i) +* (Start-At (0,SCM+FSA)) c= s +* (Initialized (Macro i)) by FUNCT_4:26, SCMFSA6B:8;
then A2: IC (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1)) in dom Mi9 by SCMFSA6B:def 2;
A3: (Initialized (Macro i)) . 1 = halt SCM+FSA by COMPOS_1:148, SCMFSA6B:33;
A4: Initialized (Macro i) c= s +* (Initialized (Macro i)) by FUNCT_4:26;

A5: now

set Y = NAT ;
set X = (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)};
assume A6: Result ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i)))) = Exec (i,(s +* (Initialized (Macro i)))) ; :: thesis: Exec (i,(Initialized s)) = IExec ((Macro i),s)
A7: s +* ((intloc 0) .--> 1),(s +* (Macro i)) +* ((intloc 0) .--> 1) equal_outside NAT by FUNCT_7:106, FUNCT_7:132;
s +* (Initialized (Macro i)) = s +* ((Macro i) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) by FUNCT_4:15
.= (s +* (Macro i)) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= ((s +* (Macro i)) +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) by FUNCT_4:15 ;
then Initialized s,s +* (Initialized (Macro i)) equal_outside NAT by A7, FUNCT_7:106;
then (Initialized s) | ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) = (s +* (Initialized (Macro i))) | ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) by Th4;
then A8: (Exec (i,(Initialized 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;
A9: NAT /\ (((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) c= NAT /\ (((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) ;
A10: dom (IExec ((Macro i),s)) = the carrier of SCM+FSA by PARTFUN1:def 4;
A11: dom (Exec (i,(Initialized s))) = the carrier of SCM+FSA by PARTFUN1:def 4;
A12: dom s = ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT by PARTFUN1:def 4, SCMFSA_2:8;

now

thus dom ((Exec (i,(Initialized s))) | NAT) = (dom s) /\ NAT by A11, A12, RELAT_1:90, SCMFSA_2:8; :: 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 A13: x in NAT /\ (((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) by A11, RELAT_1:90, SCMFSA_2:8;
then x in NAT by XBOOLE_1:21;
then reconsider x9 = x as Element of NAT ;
x in NAT by A13, 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 A14: (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 A15: (IExec ((Macro i),s)) | NAT = s | NAT by A6, A12, A9, FUNCT_4:93, SCMFSA_2:8;
(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
A16: x in (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)} and
A17: x in NAT by XBOOLE_0:3;
A18: ( x in Int-Locations \/ FinSeq-Locations or x in {(IC SCM+FSA)} ) by A16, XBOOLE_0:def 3;

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

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

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

end;

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

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

end;

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

reconsider x = x as Element of NAT by A17;
x = IC SCM+FSA by A19;
hence contradiction by COMPOS_1:3; :: thesis: verum

end;

end;

end;

then (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)} misses dom (s | NAT) by RELAT_1:87, XBOOLE_1:63;
then (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, FUNCT_4:76;
then A20: (Exec (i,(Initialized s))) | (((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) = (IExec ((Macro i),s)) | (((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) by A8, A15, A14, RELAT_1:185;
thus Exec (i,(Initialized s)) = (Exec (i,(Initialized s))) | (((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) by A11, RELAT_1:98, SCMFSA_2:8
.= IExec ((Macro i),s) by A10, A20, RELAT_1:98, SCMFSA_2:8 ; :: thesis: verum

end;

Macro i c= Initialized (Macro i) by SCMFSA6A:26;
then A21: dom (Macro i) c= dom (Initialized (Macro i)) by RELAT_1:25;
A22: 1 in dom (Macro i) by SCMFSA6B:32;
A23: (Initialized (Macro i)) . 0 = i by COMPOS_1:148, SCMFSA6B:33;
Y: (ProgramPart (s +* (Initialized (Macro i)))) /. (IC (s +* (Initialized (Macro i)))) = (s +* (Initialized (Macro i))) . (IC (s +* (Initialized (Macro i)))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1))) /. (IC (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1))) = (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1)) . (IC (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1))) by COMPOS_1:38;
A24: Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),(0 + 1)) = Following ((ProgramPart (s +* (Initialized (Macro i)))),(Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),0))) by EXTPRO_1:4
.= Following ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i)))) by EXTPRO_1:3
.= Exec (((s +* (Initialized (Macro i))) . 0),(s +* (Initialized (Macro i)))) by Y, FUNCT_4:26, SCMFSA6B:34
.= Exec (i,(s +* (Initialized (Macro i)))) by A1, A23, A4, GRFUNC_1:8 ;
TX: ProgramPart (s +* (Initialized (Macro i))) = ProgramPart (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1)) by AMI_1:123;

per cases ( IC (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1)) = 0 or IC (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1)) = 1 ) by A2, SCMFSA6B:32;

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

then A26: CurInstr ((ProgramPart (s +* (Initialized (Macro i)))),(Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1))) = (s +* (Initialized (Macro i))) . 0 by A24, Z, TX, AMI_1:def 13
.= i by A1, A23, A4, GRFUNC_1:8 ;
succ (IC (s +* (Initialized (Macro i)))) = succ 0 by FUNCT_4:26, SCMFSA6B:34
.= 1 ;
then A27: InsCode i in {0,6,7,8} by A24, 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,(Initialized s)) = IExec ((Macro i),s)

then A28: i = halt SCM+FSA by SCMFSA_2:122;
then ProgramPart (s +* (Initialized (Macro i))) halts_on s +* (Initialized (Macro i)) by A26, EXTPRO_1:30;
hence Exec (i,(Initialized s)) = IExec ((Macro i),s) by A5, A24, A26, A28, EXTPRO_1:def 8; :: thesis: verum

end;

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

A30: 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 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;

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

A32: 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 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 A24, A25, FUNCT_4:26, SCMFSA6B:34;
then A33: s +* (Initialized (Macro i)) = Exec (i,(s +* (Initialized (Macro i)))) by A30, A32, A31, SCMFSA_2:86;
A34: Following ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i)))) = Following ((ProgramPart (s +* (Initialized (Macro i)))),(Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),0))) by EXTPRO_1:3
.= Exec (i,(s +* (Initialized (Macro i)))) by A24, EXTPRO_1:4 ;

now

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

end;

then not ProgramPart (s +* (Initialized (Macro i))) halts_on s +* (Initialized (Macro i)) by EXTPRO_1:30;
hence Exec (i,(Initialized s)) = IExec ((Macro i),s) by A4, EXTPRO_1:def 10; :: thesis: verum

end;

end;

end;

end;

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

(ProgramPart (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1))) /. (IC (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1))) = (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1)) . (IC (Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1))) by COMPOS_1:38;
then A35: CurInstr ((ProgramPart (s +* (Initialized (Macro i)))),(Comput ((ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),1))) = (s +* (Initialized (Macro i))) . 1 by A24, S, TX, AMI_1:def 13
.= halt SCM+FSA by A21, A22, A3, A4, GRFUNC_1:8 ;
then ProgramPart (s +* (Initialized (Macro i))) halts_on s +* (Initialized (Macro i)) by EXTPRO_1:30;
hence Exec (i,(Initialized s)) = IExec ((Macro i),s) by A5, A24, A35, EXTPRO_1:def 8; :: thesis: verum

end;

end;