let s be State of SCMPDS ; :: thesis: for i being parahalting Instruction of SCMPDS holds Exec i,(Initialize s) = IExec (Load i),s
set SA0 = Start-At 0 ,SCMPDS ;
let i be parahalting Instruction of SCMPDS ; :: thesis: Exec i,(Initialize s) = IExec (Load i),s
set Li = Load i;
set Mi = stop (Load i);
set sI = (Initialize s) +* (stop (Load i));
set Is = Initialize s;
I1: (Initialize s) +* (stop (Load i)) = s +* (Initialize (stop (Load i))) by SCMPDS_4:5;
set IC1 = IC (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1);
A1: ProgramPart ((Initialize s) +* (stop (Load i))) halts_on (Initialize s) +* (stop (Load i)) by I1, FUNCT_4:26, SCMPDS_4:63;
A2: 1 in dom (Initialize (stop (Load i))) by Th13;
A3: 0 in dom (Initialize (stop (Load i))) by Th13;

A4: now

set Y = NAT ;
set X = SCM-Data-Loc \/ {(IC SCMPDS )};
assume A5: Result (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))) = Exec i,((Initialize s) +* (stop (Load i))) ; :: thesis: Exec i,(Initialize s) = IExec (Load i),s
Initialize s,(Initialize s) +* (stop (Load i)) equal_outside NAT by FUNCT_7:132;
then (Initialize s) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = ((Initialize s) +* (stop (Load i))) | (SCM-Data-Loc \/ {(IC SCMPDS )}) by Th41;
then A6: (Exec i,(Initialize s)) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec i,((Initialize s) +* (stop (Load i)))) | (SCM-Data-Loc \/ {(IC SCMPDS )}) by SCMPDS_3:7;
A7: NAT /\ ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) c= NAT /\ ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) ;
A8: dom (IExec (Load i),s) = the carrier of SCMPDS by PARTFUN1:def 4;
A9: dom (Exec i,(Initialize s)) = the carrier of SCMPDS by PARTFUN1:def 4;
A10: dom s = (SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT by PARTFUN1:def 4, SCMPDS_3:5;

now

thus dom ((Exec i,(Initialize s)) | NAT ) = (dom s) /\ NAT by A9, A10, RELAT_1:90, SCMPDS_3:5; :: 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 A11: x in NAT /\ ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) by A9, RELAT_1:90, SCMPDS_3:5;
then x is Element of NAT by XBOOLE_1:21;
then reconsider x9 = x as Element of NAT ;
x in NAT by A11, XBOOLE_1:21;
hence ((Exec i,(Initialize s)) | NAT ) . x = (Exec i,(Initialize s)) . x by FUNCT_1:72
.= (Initialize s) . x9 by AMI_1:def 13
.= s . x by Th40 ;
:: thesis: verum

end;

then A12: (Exec i,(Initialize s)) | NAT = s | NAT by FUNCT_1:68;
dom (Exec i,((Initialize s) +* (stop (Load i)))) = the carrier of SCMPDS by PARTFUN1:def 4;
then A13: (IExec (Load i),s) | NAT = s | NAT by A5, A10, A7, FUNCT_4:93, SCMPDS_3:5;
SCM-Data-Loc \/ {(IC SCMPDS )} misses NAT

proof

assume SCM-Data-Loc \/ {(IC SCMPDS )} meets NAT ; :: thesis: contradiction
then consider x being set such that
A14: x in SCM-Data-Loc \/ {(IC SCMPDS )} and
A15: x in NAT by XBOOLE_0:3;
A16: ( x in SCM-Data-Loc or x in {(IC SCMPDS )} ) by A14, XBOOLE_0:def 3;

per cases ( x in SCM-Data-Loc or x = IC SCMPDS ) by A16, TARSKI:def 1;

suppose x in SCM-Data-Loc ; :: thesis: contradiction

hence contradiction by A15, AMI_2:29, XBOOLE_0:3; :: thesis: verum

end;

suppose x = IC SCMPDS ; :: thesis: contradiction

then reconsider l = IC SCMPDS as Element of NAT by A15;
l = IC SCMPDS ;
hence contradiction by COMPOS_1:3; :: thesis: verum

end;

end;

end;

then SCM-Data-Loc \/ {(IC SCMPDS )} misses dom (s | NAT ) by RELAT_1:87, XBOOLE_1:63;
then (IExec (Load i),s) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec i,((Initialize s) +* (stop (Load i)))) | (SCM-Data-Loc \/ {(IC SCMPDS )}) by A5, FUNCT_4:76;
then A17: (Exec i,(Initialize s)) | ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) = (IExec (Load i),s) | ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) by A6, A13, A12, RELAT_1:185;
thus Exec i,(Initialize s) = (Exec i,(Initialize s)) | ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) by A9, RELAT_1:98, SCMPDS_3:5
.= IExec (Load i),s by A8, A17, RELAT_1:98, SCMPDS_3:5 ; :: thesis: verum

end;

A18: (Initialize (stop (Load i))) . 1 = halt SCMPDS by Th13;
A19: (Initialize (stop (Load i))) . 0 = i by Th13;
A20: Initialize (stop (Load i)) c= (Initialize s) +* (stop (Load i)) by I1, FUNCT_4:26;
then A21: IC (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) in dom (stop (Load i)) by SCMPDS_4:def 9;
Y: (ProgramPart ((Initialize s) +* (stop (Load i)))) /. (IC ((Initialize s) +* (stop (Load i)))) = ((Initialize s) +* (stop (Load i))) . (IC ((Initialize s) +* (stop (Load i)))) by COMPOS_1:38;
A22: Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),(0 + 1) = Following (ProgramPart ((Initialize s) +* (stop (Load i)))),(Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),0 ) by AMI_1:14
.= Following (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))) by AMI_1:13
.= Exec (((Initialize s) +* (stop (Load i))) . 0 ),((Initialize s) +* (stop (Load i))) by Th18, Y, I1, FUNCT_4:26
.= Exec i,((Initialize s) +* (stop (Load i))) by A3, A19, A20, GRFUNC_1:8 ;

per cases ( IC (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) = 0 or IC (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) = 1 ) by A21, Th11;

suppose A23: IC (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) = 0 ; :: thesis: Exec i,(Initialize s) = IExec (Load i),s

set Ni = InsCode i;
succ (IC ((Initialize s) +* (stop (Load i)))) = succ 0 by Th18, I1, FUNCT_4:26
.= 1 ;
then A24: InsCode i in {0 ,1,4,5,6} by A22, A23, SCMPDS_4:6;
TX: ProgramPart ((Initialize s) +* (stop (Load i))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) by AMI_1:123;
Y: (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1)) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1)) = (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) . (IC (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1)) by COMPOS_1:38;
A25: CurInstr (ProgramPart ((Initialize s) +* (stop (Load i)))),(Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) = ((Initialize s) +* (stop (Load i))) . 0 by A22, A23, Y, TX, AMI_1:def 13
.= i by A3, A19, A20, GRFUNC_1:8 ;
A26: InsCode i <> 1 by Th26;

hereby :: thesis: verum

per cases ( i = halt SCMPDS or i <> halt SCMPDS ) ;

suppose i = halt SCMPDS ; :: thesis: Exec i,(Initialize s) = IExec (Load i),s

hence Exec i,(Initialize s) = IExec (Load i),s by A1, A4, A22, A25, AMI_1:def 22; :: thesis: verum

end;

suppose A27: i <> halt SCMPDS ; :: thesis: Exec i,(Initialize s) = IExec (Load i),s

A28: for loc being Element of NAT holds ((Initialize s) +* (stop (Load i))) . loc = (Exec i,((Initialize s) +* (stop (Load i)))) . loc by AMI_1:def 13;

A29: now

let b be Int_position ; :: thesis: ((Initialize s) +* (stop (Load i))) . b₁ = (Exec i,((Initialize s) +* (stop (Load i)))) . b₁

per cases ( InsCode i = 0 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 ) by A24, A26, ENUMSET1:def 3;

suppose InsCode i = 0 ; :: thesis: ((Initialize s) +* (stop (Load i))) . b₁ = (Exec i,((Initialize s) +* (stop (Load i)))) . b₁

then ex k1 being Integer st i = goto k1 by SCMPDS_2:35;
hence ((Initialize s) +* (stop (Load i))) . b = (Exec i,((Initialize s) +* (stop (Load i)))) . b by SCMPDS_2:66; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: ((Initialize s) +* (stop (Load i))) . b₁ = (Exec i,((Initialize s) +* (stop (Load i)))) . b₁

then ex a being Int_position ex k1, k2 being Integer st i = a,k1 <>0_goto k2 by SCMPDS_2:39;
hence ((Initialize s) +* (stop (Load i))) . b = (Exec i,((Initialize s) +* (stop (Load i)))) . b by SCMPDS_2:67; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: ((Initialize s) +* (stop (Load i))) . b₁ = (Exec i,((Initialize s) +* (stop (Load i)))) . b₁

then ex a being Int_position ex k1, k2 being Integer st i = a,k1 <=0_goto k2 by SCMPDS_2:40;
hence ((Initialize s) +* (stop (Load i))) . b = (Exec i,((Initialize s) +* (stop (Load i)))) . b by SCMPDS_2:68; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: ((Initialize s) +* (stop (Load i))) . b₁ = (Exec i,((Initialize s) +* (stop (Load i)))) . b₁

then ex a being Int_position ex k1, k2 being Integer st i = a,k1 >=0_goto k2 by SCMPDS_2:41;
hence ((Initialize s) +* (stop (Load i))) . b = (Exec i,((Initialize s) +* (stop (Load i)))) . b by SCMPDS_2:69; :: thesis: verum

end;

end;

end;

A30: Following (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))) = Following (ProgramPart ((Initialize s) +* (stop (Load i)))),(Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),0 ) by AMI_1:13
.= Exec i,((Initialize s) +* (stop (Load i))) by A22, AMI_1:14 ;
A31: IC ((Initialize s) +* (stop (Load i))) = IC (Exec i,((Initialize s) +* (stop (Load i)))) by A22, A23, Th18, I1, FUNCT_4:26;
then A32: (Initialize s) +* (stop (Load i)) = Exec i,((Initialize s) +* (stop (Load i))) by A29, A28, SCMPDS_2:54;

now

let n be Element of NAT ; :: thesis: CurInstr (ProgramPart ((Initialize s) +* (stop (Load i)))),(Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),n) <> halt SCMPDS
Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),n = (Initialize s) +* (stop (Load i)) by A31, A29, A28, A30, AMI_1:130, SCMPDS_2:54
.= Following (ProgramPart ((Initialize s) +* (stop (Load i)))),(Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),0 ) by A32, A30, AMI_1:13
.= Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),(0 + 1) by AMI_1:14 ;
hence CurInstr (ProgramPart ((Initialize s) +* (stop (Load i)))),(Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),n) <> halt SCMPDS by A25, A27; :: thesis: verum

end;

then not ProgramPart ((Initialize s) +* (stop (Load i))) halts_on (Initialize s) +* (stop (Load i)) by AMI_1:146;
hence Exec i,(Initialize s) = IExec (Load i),s by I1, FUNCT_4:26, SCMPDS_4:63; :: thesis: verum

end;

end;

end;

end;

suppose S: IC (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) = 1 ; :: thesis: Exec i,(Initialize s) = IExec (Load i),s

TX: ProgramPart ((Initialize s) +* (stop (Load i))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) by AMI_1:123;
(ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1)) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1)) = (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) . (IC (Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1)) by COMPOS_1:38;
then CurInstr (ProgramPart ((Initialize s) +* (stop (Load i)))),(Comput (ProgramPart ((Initialize s) +* (stop (Load i)))),((Initialize s) +* (stop (Load i))),1) = ((Initialize s) +* (stop (Load i))) . 1 by A22, S, TX, AMI_1:def 13
.= halt SCMPDS by A2, A18, A20, GRFUNC_1:8 ;
hence Exec i,(Initialize s) = IExec (Load i),s by A1, A4, A22, AMI_1:def 22; :: thesis: verum

end;

end;