let s be State of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for i being parahalting Instruction of SCMPDS holds Exec (i,(Initialize s)) = IExec ((Load i),P,s)
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for i being parahalting Instruction of SCMPDS holds Exec (i,(Initialize s)) = IExec ((Load i),P,s)
let i be parahalting Instruction of SCMPDS; :: thesis: Exec (i,(Initialize s)) = IExec ((Load i),P,s)
set Li = Load i;
set Mi = stop (Load i);
set sI = Initialize s;
set PI = P +* (stop (Load i));
set Is = Initialize s;
set IC1 = IC (Comput ((P +* (stop (Load i))),(Initialize s),1));
A2: P +* (stop (Load i)) halts_on Initialize s by FUNCT_4:26, SCMPDS_4:def 10;
A3: 1 in dom (stop (Load i)) by Th9;
A4: 0 in dom (stop (Load i)) by Th9;

A5: now

set Y = NAT ;
set X = SCM-Data-Loc \/ {(IC )};
assume A6: Result ((P +* (stop (Load i))),(Initialize s)) = Exec (i,(Initialize s)) ; :: thesis: Exec (i,(Initialize s)) = IExec ((Load i),P,s)
A8: NAT /\ ((SCM-Data-Loc \/ {(IC )}) \/ NAT) c= NAT /\ ((SCM-Data-Loc \/ {(IC )}) \/ NAT) ;
A9: dom (Exec (i,(Initialize s))) = the carrier of SCMPDS by PARTFUN1:def 4;
A10: dom s = the carrier of SCMPDS by PARTFUN1:def 4;
then dom s = (SCM-Data-Loc \/ {(IC )}) \/ NAT by COMPOS_1:160, SCMPDS_2:100;
then A11: dom s = (SCM-Data-Loc \/ {(IC )}) \/ NAT ;

now

thus A12: dom ((Exec (i,(Initialize s))) | NAT) = (dom s) /\ NAT by A9, A10, RELAT_1:90; :: 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 x in (dom s) /\ NAT by A12;
then A13: x in NAT /\ ((SCM-Data-Loc \/ {(IC )}) \/ NAT) by A11;
then reconsider x9 = x as Element of NAT by XBOOLE_1:21;
x in NAT by A13, 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 A14: (Exec (i,(Initialize s))) | NAT = s | NAT by FUNCT_1:68;
dom (Exec (i,(Initialize s))) = the carrier of SCMPDS by PARTFUN1:def 4;
then dom (Exec (i,(Initialize s))) = (SCM-Data-Loc \/ {(IC )}) \/ NAT by COMPOS_1:160, SCMPDS_2:100;
then A15: (IExec ((Load i),P,s)) | NAT = s | NAT by A6, A11, A8, FUNCT_4:93;
SCM-Data-Loc \/ {(IC )} misses NAT

proof

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

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

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

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

end;

suppose x = IC ; :: thesis: contradiction

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

end;

end;

end;

then SCM-Data-Loc \/ {(IC )} misses dom (s | NAT) by RELAT_1:87, XBOOLE_1:63;
then (IExec ((Load i),P,s)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (i,(Initialize s))) | (SCM-Data-Loc \/ {(IC )}) by A6, FUNCT_4:76;
then A19: (Exec (i,(Initialize s))) | ((SCM-Data-Loc \/ {(IC )}) \/ NAT) = (IExec ((Load i),P,s)) | ((SCM-Data-Loc \/ {(IC )}) \/ NAT) by A15, A14, RELAT_1:185;
dom (IExec ((Load i),P,s)) = the carrier of SCMPDS by PARTFUN1:def 4;
then A20: dom (IExec ((Load i),P,s)) = (SCM-Data-Loc \/ {(IC )}) \/ NAT by COMPOS_1:160, SCMPDS_2:100;
A21: dom (Exec (i,(Initialize s))) = the carrier of SCMPDS by PARTFUN1:def 4;
dom (Exec (i,(Initialize s))) = (SCM-Data-Loc \/ {(IC )}) \/ NAT by A21, COMPOS_1:160, SCMPDS_2:100;
hence Exec (i,(Initialize s)) = (Exec (i,(Initialize s))) | ((SCM-Data-Loc \/ {(IC )}) \/ NAT) by RELAT_1:98
.= (IExec ((Load i),P,s)) | ((SCM-Data-Loc \/ {(IC )}) \/ NAT) by A19
.= IExec ((Load i),P,s) by A20, RELAT_1:98 ;
:: thesis: verum

end;

A22: (stop (Load i)) . 1 = halt SCMPDS by Th10;
A23: (stop (Load i)) . 0 = i by Th10;
A24: stop (Load i) c= P +* (stop (Load i)) by FUNCT_4:26;
A25: IC (Comput ((P +* (stop (Load i))),(Initialize s),1)) in dom (stop (Load i)) by FUNCT_4:26, SCMPDS_4:def 9;
A26: (P +* (stop (Load i))) /. (IC (Initialize s)) = (P +* (stop (Load i))) . (IC (Initialize s)) by PBOOLE:158;
A27: Comput ((P +* (stop (Load i))),(Initialize s),(0 + 1)) = Following ((P +* (stop (Load i))),(Comput ((P +* (stop (Load i))),(Initialize s),0))) by EXTPRO_1:4
.= Following ((P +* (stop (Load i))),(Initialize s)) by EXTPRO_1:3
.= Exec (((P +* (stop (Load i))) . 0),(Initialize s)) by A26, COMPOS_1:223
.= Exec (i,(Initialize s)) by A4, A23, A24, GRFUNC_1:8 ;

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

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

set Ni = InsCode i;
succ (IC (Initialize s)) = succ 0 by COMPOS_1:223
.= 1 ;
then A29: InsCode i in {0,1,4,5,6} by A27, A28, SCMPDS_4:6;
A30: CurInstr ((P +* (stop (Load i))),(Comput ((P +* (stop (Load i))),(Initialize s),1))) = (P +* (stop (Load i))) . 0 by A28, PBOOLE:158
.= i by A4, A23, A24, GRFUNC_1:8 ;
A31: 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),P,s)

hence Exec (i,(Initialize s)) = IExec ((Load i),P,s) by A2, A5, A27, A30, EXTPRO_1:def 8; :: thesis: verum

end;

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

A33: for loc being Element of NAT holds (Initialize s) . loc = (Exec (i,(Initialize s))) . loc by AMI_1:def 13;

A34: now

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

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

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

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

end;

suppose InsCode i = 4 ; :: thesis: (Initialize s) . b₁ = (Exec (i,(Initialize s))) . 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) . b = (Exec (i,(Initialize s))) . b by SCMPDS_2:67; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: (Initialize s) . b₁ = (Exec (i,(Initialize s))) . 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) . b = (Exec (i,(Initialize s))) . b by SCMPDS_2:68; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: (Initialize s) . b₁ = (Exec (i,(Initialize s))) . 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) . b = (Exec (i,(Initialize s))) . b by SCMPDS_2:69; :: thesis: verum

end;

end;

end;

A35: Following ((P +* (stop (Load i))),(Initialize s)) = Following ((P +* (stop (Load i))),(Comput ((P +* (stop (Load i))),(Initialize s),0))) by EXTPRO_1:3
.= Exec (i,(Initialize s)) by A27, EXTPRO_1:4 ;
A36: IC (Initialize s) = IC (Exec (i,(Initialize s))) by A27, A28, COMPOS_1:223;
then A37: Initialize s = Exec (i,(Initialize s)) by A34, A33, SCMPDS_2:54;

now

let n be Element of NAT ; :: thesis: CurInstr ((P +* (stop (Load i))),(Comput ((P +* (stop (Load i))),(Initialize s),n))) <> halt SCMPDS
Comput ((P +* (stop (Load i))),(Initialize s),n) = Initialize s by A36, A34, A33, A35, EXTPRO_1:27, SCMPDS_2:54
.= Following ((P +* (stop (Load i))),(Comput ((P +* (stop (Load i))),(Initialize s),0))) by A37, A35, EXTPRO_1:3
.= Comput ((P +* (stop (Load i))),(Initialize s),(0 + 1)) by EXTPRO_1:4 ;
hence CurInstr ((P +* (stop (Load i))),(Comput ((P +* (stop (Load i))),(Initialize s),n))) <> halt SCMPDS by A30, A32; :: thesis: verum

end;

then not P +* (stop (Load i)) halts_on Initialize s by EXTPRO_1:30;
hence Exec (i,(Initialize s)) = IExec ((Load i),P,s) by FUNCT_4:26, SCMPDS_4:def 10; :: thesis: verum

end;

end;

end;

end;

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

CurInstr ((P +* (stop (Load i))),(Comput ((P +* (stop (Load i))),(Initialize s),1))) = (P +* (stop (Load i))) . 1 by A38, PBOOLE:158
.= halt SCMPDS by A3, A22, A24, GRFUNC_1:8 ;
hence Exec (i,(Initialize s)) = IExec ((Load i),P,s) by A2, A5, A27, EXTPRO_1:def 8; :: thesis: verum

end;

end;