let s be State of SCMPDS ; :: thesis: for i being parahalting Instruction of SCMPDS holds Exec i,(Initialized s) = IExec (Load i),s
let i be parahalting Instruction of SCMPDS ; :: thesis: Exec i,(Initialized s) = IExec (Load i),s
set Li = Load i;
set Mi = stop (Load i);
set sI = s +* (Initialized (stop (Load i)));
set Is = Initialized s;
set SA0 = Start-At (inspos 0 );
set IC1 = IC (Computation (s +* (Initialized (stop (Load i)))),1);
A1: ( inspos 0 in dom (Initialized (stop (Load i))) & (Initialized (stop (Load i))) . (inspos 0 ) = i ) by Th13;
A2: ( inspos 1 in dom (Initialized (stop (Load i))) & (Initialized (stop (Load i))) . (inspos 1) = halt SCMPDS ) by Th13;
A3: Initialized (stop (Load i)) c= s +* (Initialized (stop (Load i))) by FUNCT_4:26;
A4: s +* (Initialized (stop (Load i))) is halting by FUNCT_4:26, SCMPDS_4:63;

A5: now

assume A6: Result (s +* (Initialized (stop (Load i)))) = Exec i,(s +* (Initialized (stop (Load i)))) ; :: thesis: Exec i,(Initialized s) = IExec (Load i),s
set X = SCM-Data-Loc \/ {(IC SCMPDS )};
set Y = NAT ;
A7: dom (Exec i,(Initialized s)) = the carrier of SCMPDS by AMI_1:79;
A8: dom (IExec (Load i),s) = the carrier of SCMPDS by AMI_1:79;
s +* (Initialized (stop (Load i))) = (s +* (stop (Load i))) +* (Start-At (inspos 0 )) by FUNCT_4:15;
then Initialized s,s +* (Initialized (stop (Load i))) equal_outside NAT by AMI_1:120, FUNCT_7:106;
then (Initialized s) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (s +* (Initialized (stop (Load i)))) | (SCM-Data-Loc \/ {(IC SCMPDS )}) by Th41;
then A9: (Exec i,(Initialized s)) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec i,(s +* (Initialized (stop (Load i))))) | (SCM-Data-Loc \/ {(IC SCMPDS )}) by SCMPDS_3:7;
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
A10: ( x in SCM-Data-Loc \/ {(IC SCMPDS )} & x in NAT ) by XBOOLE_0:3;
A11: ( x in SCM-Data-Loc or x in {(IC SCMPDS )} ) by A10, XBOOLE_0:def 3;

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

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

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

end;

suppose x = IC SCMPDS ; :: thesis: contradiction

then reconsider l = IC SCMPDS as Instruction-Location of SCMPDS by A10, AMI_1:def 4;
l = IC SCMPDS ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

end;

end;

then A12: SCM-Data-Loc \/ {(IC SCMPDS )} misses dom (s | NAT ) by RELAT_1:87, XBOOLE_1:63;
A13: dom (Exec i,(s +* (Initialized (stop (Load i))))) = the carrier of SCMPDS by AMI_1:79;
A14: dom s = (SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT by AMI_1:79, SCMPDS_3:5;
A15: NAT /\ ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) c= NAT /\ ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) ;
A16: (IExec (Load i),s) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec i,(s +* (Initialized (stop (Load i))))) | (SCM-Data-Loc \/ {(IC SCMPDS )}) by A6, A12, FUNCT_4:76;
A17: (IExec (Load i),s) | NAT = s | NAT by A6, A13, A14, A15, FUNCT_4:93, SCMPDS_3:5;

now

thus dom ((Exec i,(Initialized s)) | NAT ) = (dom s) /\ NAT by A7, A14, RELAT_1:90, SCMPDS_3:5; :: 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 A18: x in NAT /\ ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) by A7, RELAT_1:90, SCMPDS_3:5;
then A19: x in NAT by XBOOLE_1:21;
x is Element of NAT by A18, XBOOLE_1:21;
then reconsider x' = x as Instruction-Location of SCMPDS by AMI_1:def 4;
thus ((Exec i,(Initialized s)) | NAT ) . x = (Exec i,(Initialized s)) . x by A19, FUNCT_1:72
.= (Initialized s) . x' by AMI_1:def 13
.= s . x by Th40 ; :: thesis: verum

end;

then (Exec i,(Initialized s)) | NAT = s | NAT by FUNCT_1:68;
then A20: (Exec i,(Initialized s)) | ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) = (IExec (Load i),s) | ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) by A9, A16, A17, RELAT_1:185;
thus Exec i,(Initialized s) = (Exec i,(Initialized s)) | ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) by A7, RELAT_1:98, SCMPDS_3:5
.= IExec (Load i),s by A8, A20, RELAT_1:98, SCMPDS_3:5 ; :: thesis: verum

end;

A21: Computation (s +* (Initialized (stop (Load i)))),(0 + 1) = Following (Computation (s +* (Initialized (stop (Load i)))),0 ) by AMI_1:14
.= Following (s +* (Initialized (stop (Load i)))) by AMI_1:13
.= Exec ((s +* (Initialized (stop (Load i)))) . (inspos 0 )),(s +* (Initialized (stop (Load i)))) by Th18, FUNCT_4:26
.= Exec i,(s +* (Initialized (stop (Load i)))) by A1, A3, GRFUNC_1:8 ;
A22: IC (Computation (s +* (Initialized (stop (Load i)))),1) in dom (stop (Load i)) by A3, SCMPDS_4:def 9;

per cases ( IC (Computation (s +* (Initialized (stop (Load i)))),1) = inspos 0 or IC (Computation (s +* (Initialized (stop (Load i)))),1) = inspos 1 ) by A22, Th11;

suppose A23: IC (Computation (s +* (Initialized (stop (Load i)))),1) = inspos 0 ; :: thesis: Exec i,(Initialized s) = IExec (Load i),s

then A24: CurInstr (Computation (s +* (Initialized (stop (Load i)))),1) = (s +* (Initialized (stop (Load i)))) . (inspos 0 ) by A21, AMI_1:def 13
.= i by A1, A3, GRFUNC_1:8 ;
A25: Next (IC (s +* (Initialized (stop (Load i))))) = Next (inspos 0 ) by Th18, FUNCT_4:26
.= inspos 1 ;
set Ni = InsCode i;
A26: InsCode i in {0 ,1,4,5,6} by A21, A23, A25, SCMPDS_4:6;
A27: InsCode i <> 1 by Th26;

hereby :: thesis: verum

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

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

hence Exec i,(Initialized s) = IExec (Load i),s by A4, A5, A21, A24, AMI_1:def 22; :: thesis: verum

end;

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

A29: IC (s +* (Initialized (stop (Load i)))) = IC (Exec i,(s +* (Initialized (stop (Load i))))) by A21, A23, Th18, FUNCT_4:26;

A30: now

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

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

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

then consider k1 being Integer such that
A31: i = goto k1 by SCMPDS_2:35;
thus (s +* (Initialized (stop (Load i)))) . b = (Exec i,(s +* (Initialized (stop (Load i))))) . b by A31, SCMPDS_2:66; :: thesis: verum

end;

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

then consider a being Int_position , k1, k2 being Integer such that
A32: i = a,k1 <>0_goto k2 by SCMPDS_2:39;
thus (s +* (Initialized (stop (Load i)))) . b = (Exec i,(s +* (Initialized (stop (Load i))))) . b by A32, SCMPDS_2:67; :: thesis: verum

end;

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

then consider a being Int_position , k1, k2 being Integer such that
A33: i = a,k1 <=0_goto k2 by SCMPDS_2:40;
thus (s +* (Initialized (stop (Load i)))) . b = (Exec i,(s +* (Initialized (stop (Load i))))) . b by A33, SCMPDS_2:68; :: thesis: verum

end;

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

then consider a being Int_position , k1, k2 being Integer such that
A34: i = a,k1 >=0_goto k2 by SCMPDS_2:41;
thus (s +* (Initialized (stop (Load i)))) . b = (Exec i,(s +* (Initialized (stop (Load i))))) . b by A34, SCMPDS_2:69; :: thesis: verum

end;

end;

end;

B35: for loc being Instruction-Location of SCMPDS holds (s +* (Initialized (stop (Load i)))) . loc = (Exec i,(s +* (Initialized (stop (Load i))))) . loc by AMI_1:def 13;
then A35: s +* (Initialized (stop (Load i))) = Exec i,(s +* (Initialized (stop (Load i)))) by A29, A30, SCMPDS_2:54;
A36: Following (s +* (Initialized (stop (Load i)))) = Following (Computation (s +* (Initialized (stop (Load i)))),0 ) by AMI_1:13
.= Exec i,(s +* (Initialized (stop (Load i)))) by A21, AMI_1:14 ;

now

let n be Element of NAT ; :: thesis: CurInstr (Computation (s +* (Initialized (stop (Load i)))),n) <> halt SCMPDS
Computation (s +* (Initialized (stop (Load i)))),n = s +* (Initialized (stop (Load i))) by B35, A36, A29, A30, AMI_1:130, SCMPDS_2:54
.= Following (Computation (s +* (Initialized (stop (Load i)))),0 ) by A35, A36, AMI_1:13
.= Computation (s +* (Initialized (stop (Load i)))),(0 + 1) by AMI_1:14 ;
hence CurInstr (Computation (s +* (Initialized (stop (Load i)))),n) <> halt SCMPDS by A24, A28; :: thesis: verum

end;

then not s +* (Initialized (stop (Load i))) is halting by AMI_1:def 20;
hence Exec i,(Initialized s) = IExec (Load i),s by FUNCT_4:26, SCMPDS_4:63; :: thesis: verum

end;

end;

end;

end;

suppose IC (Computation (s +* (Initialized (stop (Load i)))),1) = inspos 1 ; :: thesis: Exec i,(Initialized s) = IExec (Load i),s

then CurInstr (Computation (s +* (Initialized (stop (Load i)))),1) = (s +* (Initialized (stop (Load i)))) . (inspos 1) by A21, AMI_1:def 13
.= halt SCMPDS by A2, A3, GRFUNC_1:8 ;
hence Exec i,(Initialized s) = IExec (Load i),s by A4, A5, A21, AMI_1:def 22; :: thesis: verum

end;

end;