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 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 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 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 AMI_1:14
.= Following (ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))) by AMI_1:13
.= 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, AMI_1:146;
hence Exec i,(Initialized s) = IExec (Macro i),s by A5, A24, 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,(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 AMI_1:13
.= Exec i,(s +* (Initialized (Macro i))) by A24, AMI_1:14 ;

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, AMI_1:130
.= Following (ProgramPart (s +* (Initialized (Macro i)))),(Comput (ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),0 ) by A33, A34, AMI_1:13
.= Comput (ProgramPart (s +* (Initialized (Macro i)))),(s +* (Initialized (Macro i))),(0 + 1) by AMI_1:14 ;
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 AMI_1:146;
hence Exec i,(Initialized s) = IExec (Macro i),s by A4, AMI_1:def 26; :: 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 AMI_1:146;
hence Exec i,(Initialized s) = IExec (Macro i),s by A5, A24, A35, AMI_1:def 22; :: thesis: verum

end;

end;