:: SCMPDS_3 semantic presentation

begin


theorem :: SCMPDS_3:1
for k1 being Integer
for s1, s2 being State of SCMPDS st IC s1 = IC s2 holds
ICplusConst (s1,k1) = ICplusConst (s2,k1)
proof
let k1 be Integer; ::_thesis: for s1, s2 being State of SCMPDS st IC s1 = IC s2 holds
ICplusConst (s1,k1) = ICplusConst (s2,k1)
let s1, s2 be State of SCMPDS; ::_thesis: ( IC s1 = IC s2 implies ICplusConst (s1,k1) = ICplusConst (s2,k1) )
A1: ex i being Element of NAT st
( i = IC s1 & ICplusConst (s1,k1) = abs (i + k1) ) by SCMPDS_2:def_18;
assume  IC s1 = IC s2 ; ::_thesis: ICplusConst (s1,k1) = ICplusConst (s2,k1)
hence  ICplusConst (s1,k1) = ICplusConst (s2,k1) by A1, SCMPDS_2:def_18; ::_thesis: verum
end;

theorem :: SCMPDS_3:2
for k1 being Integer
for a being Int_position
for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
proof
let k1 be Integer; ::_thesis: for a being Int_position
for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let a be Int_position; ::_thesis: for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let s1, s2 be State of SCMPDS; ::_thesis: ( DataPart s1 = DataPart s2 implies s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1)) )
assume A1: DataPart s1 = DataPart s2 ; ::_thesis: s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
A2: a in SCM-Data-Loc by AMI_2:def_16;
then A3: s1 . a = (DataPart s1) . a by FUNCT_1:49, SCMPDS_2:84
.= s2 . a by A1, A2, FUNCT_1:49, SCMPDS_2:84 ;
A4: DataLoc ((s1 . a),k1) in SCM-Data-Loc by AMI_2:def_16;
hence s1 . (DataLoc ((s1 . a),k1)) = (DataPart s1) . (DataLoc ((s1 . a),k1)) by FUNCT_1:49, SCMPDS_2:84
.= s2 . (DataLoc ((s2 . a),k1)) by A1, A4, A3, FUNCT_1:49, SCMPDS_2:84 ;
::_thesis: verum
end;

theorem :: SCMPDS_3:3
for a being Int_position
for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . a = s2 . a
proof
let a be Int_position; ::_thesis: for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . a = s2 . a
let s1, s2 be State of SCMPDS; ::_thesis: ( DataPart s1 = DataPart s2 implies s1 . a = s2 . a )
assume A1: DataPart s1 = DataPart s2 ; ::_thesis: s1 . a = s2 . a
A2: a in SCM-Data-Loc by AMI_2:def_16;
hence s1 . a = (DataPart s1) . a by FUNCT_1:49, SCMPDS_2:84
.= s2 . a by A1, A2, FUNCT_1:49, SCMPDS_2:84 ;
::_thesis: verum
end;

theorem :: SCMPDS_3:4
not IC in SCM-Data-Loc
proof
assume  IC in SCM-Data-Loc ; ::_thesis: contradiction
then  IC is Int_position by AMI_2:def_16;
then  Values (IC ) = INT by SCMPDS_2:5;
hence  contradiction by MEMSTR_0:def_6, NUMBERS:27; ::_thesis: verum
end;

begin

theorem :: SCMPDS_3:5
canceled;

theorem :: SCMPDS_3:6
for s being State of SCMPDS
for iloc being Element of NAT
for a being Int_position holds s . a = (s +* (Start-At (iloc,SCMPDS))) . a
proof
let s be State of SCMPDS; ::_thesis: for iloc being Element of NAT
for a being Int_position holds s . a = (s +* (Start-At (iloc,SCMPDS))) . a
let iloc be Element of NAT ; ::_thesis: for a being Int_position holds s . a = (s +* (Start-At (iloc,SCMPDS))) . a
let a be Int_position; ::_thesis: s . a = (s +* (Start-At (iloc,SCMPDS))) . a
 a in the carrier of SCMPDS ;
then  a in dom s by PARTFUN1:def_2;
then A1: ( dom (Start-At (iloc,SCMPDS)) = {(IC )} & a in (dom s) \/ (dom (Start-At (iloc,SCMPDS))) ) by FUNCOP_1:13, XBOOLE_0:def_3;
 a <> IC by SCMPDS_2:43;
then  not a in {(IC )} by TARSKI:def_1;
hence  s . a = (s +* (Start-At (iloc,SCMPDS))) . a by A1, FUNCT_4:def_1; ::_thesis: verum
end;

theorem :: SCMPDS_3:7
for s, t being State of SCMPDS holds s +* (t | SCM-Data-Loc) is State of SCMPDS ;

begin

definition
let la be Int_position;
let a be Integer;
:: original: .-->
redefine funcla .--> a ->  FinPartState of SCMPDS;
coherence
 la .--> a is FinPartState of SCMPDS
proof
 ( a is Element of INT & Values la = INT ) by INT_1:def_2, SCMPDS_2:5;
hence  la .--> a is FinPartState of SCMPDS ; ::_thesis: verum
end;
end;

registration
cluster SCMPDS  ->  IC-recognized ;
coherence
 SCMPDS is IC-recognized
proof
let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; :: according to AMISTD_5:def_3 ::_thesis: for b1 being set holds
( b1 is empty or IC in dom b1 )
let p be q -autonomic FinPartState of SCMPDS; ::_thesis: ( p is empty or IC in dom p )
assume A1: not p is empty ; ::_thesis: IC in dom p
assume A2: not IC in dom p ; ::_thesis: contradiction
 not IC in dom p by A2;
then A3: dom p misses {(IC )} by ZFMISC_1:50;
 dom p c= {(IC )} \/ (dom (DataPart p)) by MEMSTR_0:32;
then A4: dom p c= dom (DataPart p) by A3, XBOOLE_1:73;
A5: dom (DataPart p) <> {} by A1, A4, XBOOLE_1:3;
 DataPart p c= p by MEMSTR_0:12;
then A6: dom (DataPart p) c= dom p by RELAT_1:11;
 not p is q -autonomic
proof
set il = the Element of NAT \ (dom q);
set d1 = the Element of dom (DataPart p);
A7: the Element of dom (DataPart p) in dom (DataPart p) by A5;
 dom (DataPart p) c= the carrier of SCMPDS by RELAT_1:def_18;
then reconsider d1 = the Element of dom (DataPart p) as Element of SCMPDS by A7;
 not NAT c= dom q ;
then A8: NAT \ (dom q) <> {} by XBOOLE_1:37;
then reconsider il = the Element of NAT \ (dom q) as Element of NAT by XBOOLE_0:def_5;
A9: not il in dom q by A8, XBOOLE_0:def_5;
 dom (DataPart p) c= SCM-Data-Loc by RELAT_1:58, SCMPDS_2:84;
then reconsider d1 = d1 as Int_position by A7, AMI_2:def_16;
 dom (Start-At (il,SCMPDS)) = {(IC )} by FUNCOP_1:13;
then A10: IC in dom (Start-At (il,SCMPDS)) by TARSKI:def_1;
A11: dom p misses {(IC )} by A2, ZFMISC_1:50;
set p2 = p +* (Start-At (il,SCMPDS));
set p1 = p +* (Start-At (il,SCMPDS));
set q2 = q +* (il .--> (d1 := 1));
set q1 = q +* (il .--> (d1 := 0));
A12: dom (il .--> (d1 := 1)) = {il} by FUNCOP_1:13;
then A13: dom q misses dom (il .--> (d1 := 1)) by A9, ZFMISC_1:50;
 dom (il .--> (d1 := 0)) = {il} by FUNCOP_1:13;
then A14: dom q misses dom (il .--> (d1 := 0)) by A9, ZFMISC_1:50;
consider s1 being State of SCMPDS such that
A15: p +* (Start-At (il,SCMPDS)) c= s1 by PBOOLE:141;
consider S1 being Instruction-Sequence of SCMPDS such that
A16: q +* (il .--> (d1 := 0)) c= S1 by PBOOLE:145;
consider s2 being State of SCMPDS such that
A17: p +* (Start-At (il,SCMPDS)) c= s2 by PBOOLE:141;
consider S2 being Instruction-Sequence of SCMPDS such that
A18: q +* (il .--> (d1 := 1)) c= S2 by PBOOLE:145;
take P1 = S1; :: according to EXTPRO_1:def_10 ::_thesis: ex b1 being set st
( q c= P1 & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P1,b2,b4)) | (dom p) = (Comput (b1,b3,b4)) | (dom p) ) )
take P2 = S2; ::_thesis: ( q c= P1 & q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) )
dom (Start-At (il,SCMPDS)) = dom (Start-At (il,SCMPDS))
.= {(IC )} by FUNCOP_1:13
.= {(IC )} ;
then (dom p) /\ (dom (Start-At (il,SCMPDS))) = (dom p) /\ {(IC )}
.= {} by A11, XBOOLE_0:def_7
.= {} ;
then  dom p misses dom (Start-At (il,SCMPDS)) by XBOOLE_0:def_7;
then  p c= p +* (Start-At (il,SCMPDS)) by FUNCT_4:32;
then A19: p c= s1 by A15, XBOOLE_1:1;
 q c= q +* (il .--> (d1 := 0)) by A14, FUNCT_4:32;
hence  q c= P1 by A16, XBOOLE_1:1; ::_thesis: ( q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) )
dom (Start-At (il,SCMPDS)) = dom (Start-At (il,SCMPDS))
.= {(IC )} by FUNCOP_1:13
.= {(IC )} ;
then (dom p) /\ (dom (Start-At (il,SCMPDS))) = (dom p) /\ {(IC )}
.= {} by A11, XBOOLE_0:def_7
.= {} ;
then  dom p misses dom (Start-At (il,SCMPDS)) by XBOOLE_0:def_7;
then  p c= p +* (Start-At (il,SCMPDS)) by FUNCT_4:32;
then A20: p c= s2 by A17, XBOOLE_1:1;
 q c= q +* (il .--> (d1 := 1)) by A13, FUNCT_4:32;
hence  q c= P2 by A18, XBOOLE_1:1; ::_thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) )
take  s1 ; ::_thesis: ex b1 being set st
( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Comput (P1,s1,b2)) | (dom p) = (Comput (P2,b1,b2)) | (dom p) )
take  s2 ; ::_thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (dom p) = (Comput (P2,s2,b1)) | (dom p) )
 p c= s1 by A19;
hence  p c= s1 ; ::_thesis: ( p c= s2 & not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (dom p) = (Comput (P2,s2,b1)) | (dom p) )
thus  p c= s2 by A20; ::_thesis: not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (dom p) = (Comput (P2,s2,b1)) | (dom p)
take  1 ; ::_thesis: not (Comput (P1,s1,1)) | (dom p) = (Comput (P2,s2,1)) | (dom p)
A21: dom (p +* (Start-At (il,SCMPDS))) = (dom p) \/ (dom (Start-At (il,SCMPDS))) by FUNCT_4:def_1;
A22: dom (q +* (il .--> (d1 := 1))) = (dom q) \/ (dom (il .--> (d1 := 1))) by FUNCT_4:def_1;
A23: IC in dom (Start-At (il,SCMPDS)) by A10;
then  IC in dom (p +* (Start-At (il,SCMPDS))) by A21, XBOOLE_0:def_3;
then A24: IC s2 = (p +* (Start-At (il,SCMPDS))) . (IC ) by A17, GRFUNC_1:2
.= (Start-At (il,SCMPDS)) . (IC ) by A23, FUNCT_4:13
.= (Start-At (il,SCMPDS)) . (IC )
.= il by FUNCOP_1:72 ;
 il in dom (il .--> (d1 := 1)) by A12, TARSKI:def_1;
then A25: il in dom (il .--> (d1 := 1)) ;
then  il in dom (q +* (il .--> (d1 := 1))) by A22, XBOOLE_0:def_3;
then A26: S2 . il = (q +* (il .--> (d1 := 1))) . il by A18, GRFUNC_1:2
.= (il .--> (d1 := 1)) . il by A25, FUNCT_4:13
.= (il .--> (d1 := 1)) . il
.= d1 := 1 by FUNCOP_1:72 ;
A27: S2 /. (IC s2) = S2 . (IC s2) by PBOOLE:143;
A28: (Comput (S2,s2,(0 + 1))) . d1 = (Following (S2,(Comput (S2,s2,0)))) . d1 by EXTPRO_1:3
.= (Following (S2,s2)) . d1
.= 1 by A24, A26, A27, SCMPDS_2:45 ;
A29: dom p c= the carrier of SCMPDS by RELAT_1:def_18;
 dom (Comput (S1,s1,1)) = the carrier of SCMPDS by PARTFUN1:def_2;
then A30: dom ((Comput (S1,s1,1)) | (dom p)) = dom p by A29, RELAT_1:62;
A31: dom (p +* (Start-At (il,SCMPDS))) = (dom p) \/ (dom (Start-At (il,SCMPDS))) by FUNCT_4:def_1;
A32: dom (q +* (il .--> (d1 := 0))) = (dom q) \/ (dom (il .--> (d1 := 0))) by FUNCT_4:def_1;
A33: IC in dom (Start-At (il,SCMPDS)) by A10;
then  IC in dom (p +* (Start-At (il,SCMPDS))) by A31, XBOOLE_0:def_3;
then A34: IC s1 = (p +* (Start-At (il,SCMPDS))) . (IC ) by A15, GRFUNC_1:2
.= (Start-At (il,SCMPDS)) . (IC ) by A33, FUNCT_4:13
.= (Start-At (il,SCMPDS)) . (IC )
.= il by FUNCOP_1:72 ;
A35: dom (il .--> (d1 := 0)) = {il} by FUNCOP_1:13;
 il in dom (il .--> (d1 := 0)) by A35, TARSKI:def_1;
then A36: il in dom (il .--> (d1 := 0)) ;
then  il in dom (q +* (il .--> (d1 := 0))) by A32, XBOOLE_0:def_3;
then A37: S1 . il = (q +* (il .--> (d1 := 0))) . il by A16, GRFUNC_1:2
.= (il .--> (d1 := 0)) . il by A36, FUNCT_4:13
.= (il .--> (d1 := 0)) . il
.= d1 := 0 by FUNCOP_1:72 ;
A38: S1 /. (IC s1) = S1 . (IC s1) by PBOOLE:143;
A39: dom (Comput (S2,s2,1)) = the carrier of SCMPDS by PARTFUN1:def_2;
A40: dom ((Comput (S2,s2,1)) | (dom p)) = dom p by A29, A39, RELAT_1:62;
(Comput (S1,s1,(0 + 1))) . d1 = (Following (S1,(Comput (S1,s1,0)))) . d1 by EXTPRO_1:3
.= (Following (S1,s1)) . d1
.= 0 by A34, A37, A38, SCMPDS_2:45 ;
then  ((Comput (S1,s1,1)) | (dom p)) . d1 = 0 by A7, A30, A6, FUNCT_1:47;
hence  not (Comput (P1,s1,1)) | (dom p) = (Comput (P2,s2,1)) | (dom p) by A28, A7, A40, A6, FUNCT_1:47; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;
end;

theorem Th8: :: SCMPDS_3:8
for s1, s2 being State of SCMPDS
for k1, k2, m being Integer st IC s1 = IC s2 & k1 <> k2 & m = IC s1 & m + k1 >= 0 & m + k2 >= 0 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)
proof
let s1, s2 be State of SCMPDS; ::_thesis: for k1, k2, m being Integer st IC s1 = IC s2 & k1 <> k2 & m = IC s1 & m + k1 >= 0 & m + k2 >= 0 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)
let k1, k2, m be Integer; ::_thesis: ( IC s1 = IC s2 & k1 <> k2 & m = IC s1 & m + k1 >= 0 & m + k2 >= 0 implies ICplusConst (s1,k1) <> ICplusConst (s2,k2) )
assume that
A1: IC s1 = IC s2 and
A2: k1 <> k2 and
A3: m = IC s1 and
A4: m + k1 >= 0 and
A5: m + k2 >= 0 ; ::_thesis: ICplusConst (s1,k1) <> ICplusConst (s2,k2)
 ex i being Element of NAT st
( i = IC s1 & ICplusConst (s1,k1) = abs (i + k1) ) by SCMPDS_2:def_18;
then A6: ICplusConst (s1,k1) = m + k1 by A3, A4, ABSVALUE:def_1;
assume A7: ICplusConst (s1,k1) = ICplusConst (s2,k2) ; ::_thesis: contradiction
 ex j being Element of NAT st
( j = IC s2 & ICplusConst (s2,k2) = abs (j + k2) ) by SCMPDS_2:def_18;
then  ICplusConst (s2,k2) = m + k2 by A1, A3, A5, ABSVALUE:def_1;
hence  contradiction by A2, A7, A6; ::_thesis: verum
end;

theorem :: SCMPDS_3:9
for s1, s2 being State of SCMPDS
for k1, k2 being Element of NAT st IC s1 = IC s2 & k1 <> k2 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)
proof
let s1, s2 be State of SCMPDS; ::_thesis: for k1, k2 being Element of NAT st IC s1 = IC s2 & k1 <> k2 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)
let k1, k2 be Element of NAT ; ::_thesis: ( IC s1 = IC s2 & k1 <> k2 implies ICplusConst (s1,k1) <> ICplusConst (s2,k2) )
reconsider m = IC s1 as Element of NAT ;
set mm = m + 2;
 ((m + 2) - 2) + k1 = m + k1 ;
then A1: ((m + 2) - 2) + k1 >= 0 by NAT_1:2;
 ((m + 2) - 2) + k2 = m + k2 ;
then A2: ((m + 2) - 2) + k2 >= 0 by NAT_1:2;
assume  ( IC s1 = IC s2 & k1 <> k2 ) ; ::_thesis: ICplusConst (s1,k1) <> ICplusConst (s2,k2)
hence  ICplusConst (s1,k1) <> ICplusConst (s2,k2) by A1, A2, Th8; ::_thesis: verum
end;

theorem Th10: :: SCMPDS_3:10
for s being State of SCMPDS holds succ (IC s) = ICplusConst (s,1)
proof
let s be State of SCMPDS; ::_thesis: succ (IC s) = ICplusConst (s,1)
consider j being Element of NAT  such that
A1: j = IC s and
A2: ICplusConst (s,1) = abs (j + 1) by SCMPDS_2:def_18;
reconsider mj = IC s as Element of NAT ;
A3: j * 1 >= 0 by NAT_1:2;
 j >= 0 by NAT_1:2;
then  succ (IC s) = (abs mj) + 1 by A1, ABSVALUE:def_1
.= (abs mj) + (abs 1) by ABSVALUE:def_1
.= abs (mj + 1) by A1, A3, ABSVALUE:11 ;
hence  succ (IC s) = ICplusConst (s,1) by A1, A2; ::_thesis: verum
end;

registration
cluster SCMPDS  ->  CurIns-recognized ;
coherence
 SCMPDS is CurIns-recognized
proof
let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; :: according to AMISTD_5:def_4 ::_thesis: for b1 being set
for b2 being set holds
( not b1 c= b2 or for b3 being set holds
( not q c= b3 or for b4 being Element of NAT holds IC (Comput (b3,b2,b4)) in dom q ) )
let p be non empty q -autonomic FinPartState of SCMPDS; ::_thesis: for b1 being set holds
( not p c= b1 or for b2 being set holds
( not q c= b2 or for b3 being Element of NAT holds IC (Comput (b2,b1,b3)) in dom q ) )
let s be State of SCMPDS; ::_thesis: ( not p c= s or for b1 being set holds
( not q c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in dom q ) )
assume A1: p c= s ; ::_thesis: for b1 being set holds
( not q c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in dom q )
let P be Instruction-Sequence of SCMPDS; ::_thesis: ( not q c= P or for b1 being Element of NAT holds IC (Comput (P,s,b1)) in dom q )
assume A2: q c= P ; ::_thesis: for b1 being Element of NAT holds IC (Comput (P,s,b1)) in dom q
let i be Element of NAT ; ::_thesis: IC (Comput (P,s,i)) in dom q
set Csi = Comput (P,s,i);
set loc = IC (Comput (P,s,i));
set loc1 = (IC (Comput (P,s,i))) + 1;
assume  not IC (Comput (P,s,i)) in dom q ; ::_thesis: contradiction
then A3: not IC (Comput (P,s,i)) in dom q ;
set I = the Int_position := 0;
set q1 = q +* ((IC (Comput (P,s,i))) .--> ( the Int_position := 0));
set q2 = q +* ((IC (Comput (P,s,i))) .--> (halt SCMPDS));
reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) as Instruction-Sequence of SCMPDS ;
reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) as Instruction-Sequence of SCMPDS ;
A4: dom ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) = {(IC (Comput (P,s,i)))} by FUNCOP_1:13;
then A5: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) by TARSKI:def_1;
A6: dom ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) = {(IC (Comput (P,s,i)))} by FUNCOP_1:13;
then A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) by TARSKI:def_1;
A8: dom q misses dom ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) by A3, A4, ZFMISC_1:50;
A9: dom q misses dom ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) by A3, A6, ZFMISC_1:50;
A10: q +* ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) c= P1 by A2, FUNCT_4:123;
A11: q +* ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) c= P2 by A2, FUNCT_4:123;
set Cs2i = Comput (P2,s,i);
set Cs1i = Comput (P1,s,i);
 not p is q -autonomic
proof
 ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) . (IC (Comput (P,s,i))) = halt SCMPDS by FUNCOP_1:72;
then A12: P2 . (IC (Comput (P,s,i))) = halt SCMPDS by A5, FUNCT_4:13;
 ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) . (IC (Comput (P,s,i))) = the Int_position := 0 by FUNCOP_1:72;
then A13: P1 . (IC (Comput (P,s,i))) = the Int_position := 0 by A7, FUNCT_4:13;
take  P1 ; :: according to EXTPRO_1:def_10 ::_thesis: ex b1 being set st
( q c= P1 & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P1,b2,b4)) | (dom p) = (Comput (b1,b3,b4)) | (dom p) ) )
take  P2 ; ::_thesis: ( q c= P1 & q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) )
 q c= q +* ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) by A9, FUNCT_4:32;
hence A14: q c= P1 by A10, XBOOLE_1:1; ::_thesis: ( q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) )
 q c= q +* ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) by A8, FUNCT_4:32;
hence A15: q c= P2 by A11, XBOOLE_1:1; ::_thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) )
take  s ; ::_thesis: ex b1 being set st
( p c= s & p c= b1 & not for b2 being Element of NAT holds (Comput (P1,s,b2)) | (dom p) = (Comput (P2,b1,b2)) | (dom p) )
take  s ; ::_thesis: ( p c= s & p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p) )
thus  p c= s by A1; ::_thesis: ( p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p) )
A16: (Comput (P1,s,i)) | (dom p) = (Comput (P,s,i)) | (dom p) by A14, A2, A1, EXTPRO_1:def_10;
thus  p c= s by A1; ::_thesis: not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p)
A17: (Comput (P1,s,i)) | (dom p) = (Comput (P2,s,i)) | (dom p) by A14, A15, A1, EXTPRO_1:def_10;
take k = i + 1; ::_thesis: not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p)
set Cs1k = Comput (P1,s,k);
A18: IC in dom p by AMISTD_5:6;
 IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A18, FUNCT_1:49;
then  IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, A18, FUNCT_1:49;
then A19: CurInstr (P1,(Comput (P1,s,i))) = P1 . (IC (Comput (P,s,i))) by PBOOLE:143
.= the Int_position := 0 by A13 ;
A20: Comput (P1,s,k) = Following (P1,(Comput (P1,s,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s,i)))),(Comput (P1,s,i)))
.= Exec (( the Int_position := 0),(Comput (P1,s,i))) by A19 ;
A21: IC (Exec (( the Int_position := 0),(Comput (P1,s,i)))) = succ (IC (Comput (P1,s,i))) by SCMPDS_2:45;
A22: IC in dom p by AMISTD_5:6;
A23: IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A22, FUNCT_1:49;
then  IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, A22, FUNCT_1:49;
then A24: IC (Comput (P1,s,k)) = succ (IC (Comput (P,s,i))) by A20, A21
.= (IC (Comput (P,s,i))) + 1 ;
set Cs2k = Comput (P2,s,k);
A25: Comput (P2,s,k) = Following (P2,(Comput (P2,s,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s,i)))),(Comput (P2,s,i))) ;
A26: P2 /. (IC (Comput (P2,s,i))) = P2 . (IC (Comput (P2,s,i))) by PBOOLE:143;
 IC (Comput (P2,s,i)) = IC (Comput (P,s,i)) by A16, A23, A17, A22, FUNCT_1:49;
then A27: IC (Comput (P2,s,k)) = IC (Comput (P,s,i)) by A25, A12, A26, EXTPRO_1:def_3;
 ( IC ((Comput (P1,s,k)) | (dom p)) = IC (Comput (P1,s,k)) & IC ((Comput (P2,s,k)) | (dom p)) = IC (Comput (P2,s,k)) ) by A22, FUNCT_1:49;
hence  not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p) by A24, A27; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;
end;

theorem :: SCMPDS_3:11
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
proof
let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let p be non empty q -autonomic FinPartState of SCMPDS; ::_thesis: for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let s1, s2 be State of SCMPDS; ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 implies for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) )
assume that
A1: ( p c= s1 & p c= s2 ) and
A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
A3: ( p c= s1 & p c= s2 ) by A1;
let i be Element of NAT ; ::_thesis: for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let k1, k2 be Integer; ::_thesis: for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let a, b be Int_position; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
assume that
A4: CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) and
A5: a in dom p and
A6: DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p ; ::_thesis: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
 ( a in dom p implies ( ((Comput (P1,s1,i)) | (dom p)) . a = (Comput (P1,s1,i)) . a & ((Comput (P2,s2,i)) | (dom p)) . a = (Comput (P2,s2,i)) . a ) ) by FUNCT_1:49;
then A7: (Comput (P1,s1,i)) . a = (Comput (P2,s2,i)) . a by A5, A2, A3, EXTPRO_1:def_10;
set Cs1i1 = Comput (P1,s1,(i + 1));
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then A8: (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) by A4, SCMPDS_2:47;
set Cs2i1 = Comput (P2,s2,(i + 1));
A9: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
A10: ( DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) ) ) by FUNCT_1:49;
 CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
then  (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) by A9, A4, SCMPDS_2:47;
hence  (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) by A10, A6, A7, A8, A2, A3, EXTPRO_1:def_10; ::_thesis: verum
end;

theorem :: SCMPDS_3:12
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
proof
let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let p be non empty q -autonomic FinPartState of SCMPDS; ::_thesis: for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let s1, s2 be State of SCMPDS; ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 implies for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) )
assume that
A1: ( p c= s1 & p c= s2 ) and
A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
A3: ( p c= s1 & p c= s2 ) by A1;
let i be Element of NAT ; ::_thesis: for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let k1, k2 be Integer; ::_thesis: for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let a, b be Int_position; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
assume that
A4: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) and
A5: a in dom p and
A6: DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p ; ::_thesis: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
 ( a in dom p implies ( ((Comput (P1,s1,i)) | (dom p)) . a = (Comput (P1,s1,i)) . a & ((Comput (P2,s2,i)) | (dom p)) . a = (Comput (P2,s2,i)) . a ) ) by FUNCT_1:49;
then A7: (Comput (P1,s1,i)) . a = (Comput (P2,s2,i)) . a by A5, A2, A3, EXTPRO_1:def_10;
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs1i1 = Comput (P1,s1,(i + 1));
set D11 = (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1));
set D21 = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1));
set C11 = (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1));
set C12 = (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2));
set C21 = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1));
set C22 = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2));
A8: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
 ( DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) ) ) by FUNCT_1:49;
then A9: (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) by A6, A7, A2, A3, EXTPRO_1:def_10;
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then A10: (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) + ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) by A4, SCMPDS_2:49;
 ( DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies ( ((Comput (P1,s1,i)) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) & ((Comput (P2,s2,i)) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) ) ) by FUNCT_1:49;
then A11: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) by A6, A7, A2, A3, EXTPRO_1:def_10;
 CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
then  (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) + ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))) by A8, A4, SCMPDS_2:49;
hence  (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) by A11, A9, A10; ::_thesis: verum
end;

theorem :: SCMPDS_3:13
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
proof
let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let p be non empty q -autonomic FinPartState of SCMPDS; ::_thesis: for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let s1, s2 be State of SCMPDS; ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 implies for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) )
assume that
A1: ( p c= s1 & p c= s2 ) and
A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
A3: ( p c= s1 & p c= s2 ) by A1;
let i be Element of NAT ; ::_thesis: for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let k1, k2 be Integer; ::_thesis: for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let a, b be Int_position; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
assume that
A4: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) and
A5: a in dom p and
A6: DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p ; ::_thesis: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
 ( a in dom p implies ( ((Comput (P1,s1,i)) | (dom p)) . a = (Comput (P1,s1,i)) . a & ((Comput (P2,s2,i)) | (dom p)) . a = (Comput (P2,s2,i)) . a ) ) by FUNCT_1:49;
then A7: (Comput (P1,s1,i)) . a = (Comput (P2,s2,i)) . a by A5, A2, A3, EXTPRO_1:def_10;
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs1i1 = Comput (P1,s1,(i + 1));
set D11 = (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1));
set D21 = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1));
set C11 = (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1));
set C12 = (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2));
set C21 = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1));
set C22 = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2));
A8: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
 ( DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) ) ) by FUNCT_1:49;
then A9: (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) by A6, A7, A2, A3, EXTPRO_1:def_10;
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then A10: (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) - ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) by A4, SCMPDS_2:50;
 ( DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies ( ((Comput (P1,s1,i)) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) & ((Comput (P2,s2,i)) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) ) ) by FUNCT_1:49;
then A11: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) by A6, A7, A2, A3, EXTPRO_1:def_10;
 CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
then  (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) - ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))) by A8, A4, SCMPDS_2:50;
hence  (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) by A11, A9, A10; ::_thesis: verum
end;

theorem :: SCMPDS_3:14
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
proof
let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
let p be non empty q -autonomic FinPartState of SCMPDS; ::_thesis: for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
let s1, s2 be State of SCMPDS; ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 implies for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))) )
assume that
A1: ( p c= s1 & p c= s2 ) and
A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
A3: ( p c= s1 & p c= s2 ) by A1;
let i be Element of NAT ; ::_thesis: for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
let k1, k2 be Integer; ::_thesis: for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
let a, b be Int_position; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
assume that
A4: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) and
A5: a in dom p and
A6: DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p ; ::_thesis: ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
 ( a in dom p implies ( ((Comput (P1,s1,i)) | (dom p)) . a = (Comput (P1,s1,i)) . a & ((Comput (P2,s2,i)) | (dom p)) . a = (Comput (P2,s2,i)) . a ) ) by FUNCT_1:49;
then A7: (Comput (P1,s1,i)) . a = (Comput (P2,s2,i)) . a by A5, A2, A3, EXTPRO_1:def_10;
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs1i1 = Comput (P1,s1,(i + 1));
set D11 = (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1));
set D21 = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1));
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then A8: (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) by A4, SCMPDS_2:51;
A9: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
A10: ( DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) ) ) by FUNCT_1:49;
 CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
then  (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))) by A9, A4, SCMPDS_2:51;
hence  ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))) by A10, A6, A7, A8, A2, A3, EXTPRO_1:def_10; ::_thesis: verum
end;

theorem :: SCMPDS_3:15
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
proof
let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
let p be non empty q -autonomic FinPartState of SCMPDS; ::_thesis: for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
let s1, s2 be State of SCMPDS; ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 implies for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 ) )
assume that
A1: ( p c= s1 & p c= s2 ) and
A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
let i, m be Element of NAT ; ::_thesis: for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
let a be Int_position; ::_thesis: for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
let k1, k2 be Integer; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 implies ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 ) )
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) ) by A1, A2, AMISTD_5:7, EXTPRO_1:def_10;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A4: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A5: m + 1 >= 0 by NAT_1:2;
 IC in dom p by AMISTD_5:6;
then  IC in dom p ;
then A6: ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) = (Comput (P1,s1,(i + 1))) . (IC ) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) = (Comput (P2,s2,(i + 1))) . (IC ) ) by FUNCT_1:49;
A7: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A8: CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 and
A9: ( m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 ) ; ::_thesis: ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
A10: CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
A11: now__::_thesis:_(_(Comput_(P2,s2,i))_._(DataLoc_(((Comput_(P2,s2,i))_._a),k1))_=_0_implies_not_(Comput_(P1,s1,i))_._(DataLoc_(((Comput_(P1,s1,i))_._a),k1))_<>_0_)
assume that
A12: (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 and
A13: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) <> 0 ; ::_thesis: contradiction
A14: (Comput (P1,s1,(i + 1))) . (IC ) = ICplusConst ((Comput (P1,s1,i)),k2) by A4, A8, A13, SCMPDS_2:55;
(Comput (P2,s2,(i + 1))) . (IC ) = succ (IC (Comput (P2,s2,i))) by A10, A7, A8, A12, SCMPDS_2:55
.= ICplusConst ((Comput (P2,s2,i)),1) by Th10 ;
hence  contradiction by A6, A3, A9, A5, A14, Th8; ::_thesis: verum
end;
now__::_thesis:_(_(Comput_(P1,s1,i))_._(DataLoc_(((Comput_(P1,s1,i))_._a),k1))_=_0_implies_not_(Comput_(P2,s2,i))_._(DataLoc_(((Comput_(P2,s2,i))_._a),k1))_<>_0_)
assume that
A15: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 and
A16: (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) <> 0 ; ::_thesis: contradiction
A17: (Comput (P2,s2,(i + 1))) . (IC ) = ICplusConst ((Comput (P2,s2,i)),k2) by A10, A7, A8, A16, SCMPDS_2:55;
(Comput (P1,s1,(i + 1))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A4, A8, A15, SCMPDS_2:55
.= ICplusConst ((Comput (P1,s1,i)),1) by Th10 ;
hence  contradiction by A6, A3, A9, A5, A17, Th8; ::_thesis: verum
end;
hence  ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 ) by A11; ::_thesis: verum
end;

theorem :: SCMPDS_3:16
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 )
proof
let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 )
let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 )
let p be non empty q -autonomic FinPartState of SCMPDS; ::_thesis: for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 )
let s1, s2 be State of SCMPDS; ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 implies for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 ) )
assume that
A1: ( p c= s1 & p c= s2 ) and
A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 )
let i, m be Element of NAT ; ::_thesis: for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 )
let a be Int_position; ::_thesis: for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 )
let k1, k2 be Integer; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 implies ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 ) )
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) ) by A1, A2, AMISTD_5:7, EXTPRO_1:def_10;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A4: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A5: m + 1 >= 0 by NAT_1:2;
 IC in dom p by AMISTD_5:6;
then  IC in dom p ;
then A6: ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) = (Comput (P1,s1,(i + 1))) . (IC ) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) = (Comput (P2,s2,(i + 1))) . (IC ) ) by FUNCT_1:49;
A7: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A8: CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 and
A9: ( m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 ) ; ::_thesis: ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 )
A10: CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
A11: now__::_thesis:_(_(Comput_(P2,s2,i))_._(DataLoc_(((Comput_(P2,s2,i))_._a),k1))_>_0_implies_not_(Comput_(P1,s1,i))_._(DataLoc_(((Comput_(P1,s1,i))_._a),k1))_<=_0_)
assume that
A12: (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 and
A13: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) <= 0 ; ::_thesis: contradiction
A14: (Comput (P1,s1,(i + 1))) . (IC ) = ICplusConst ((Comput (P1,s1,i)),k2) by A4, A8, A13, SCMPDS_2:56;
(Comput (P2,s2,(i + 1))) . (IC ) = succ (IC (Comput (P2,s2,i))) by A10, A7, A8, A12, SCMPDS_2:56
.= ICplusConst ((Comput (P2,s2,i)),1) by Th10 ;
hence  contradiction by A6, A3, A9, A5, A14, Th8; ::_thesis: verum
end;
now__::_thesis:_(_(Comput_(P1,s1,i))_._(DataLoc_(((Comput_(P1,s1,i))_._a),k1))_>_0_implies_not_(Comput_(P2,s2,i))_._(DataLoc_(((Comput_(P2,s2,i))_._a),k1))_<=_0_)
assume that
A15: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 and
A16: (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) <= 0 ; ::_thesis: contradiction
A17: (Comput (P2,s2,(i + 1))) . (IC ) = ICplusConst ((Comput (P2,s2,i)),k2) by A10, A7, A8, A16, SCMPDS_2:56;
(Comput (P1,s1,(i + 1))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A4, A8, A15, SCMPDS_2:56
.= ICplusConst ((Comput (P1,s1,i)),1) by Th10 ;
hence  contradiction by A6, A3, A9, A5, A17, Th8; ::_thesis: verum
end;
hence  ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 ) by A11; ::_thesis: verum
end;

theorem :: SCMPDS_3:17
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )
proof
let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )
let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )
let p be non empty q -autonomic FinPartState of SCMPDS; ::_thesis: for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )
let s1, s2 be State of SCMPDS; ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 implies for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 ) )
assume that
A1: ( p c= s1 & p c= s2 ) and
A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )
let i, m be Element of NAT ; ::_thesis: for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )
let a be Int_position; ::_thesis: for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )
let k1, k2 be Integer; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 implies ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 ) )
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) ) by A1, A2, AMISTD_5:7, EXTPRO_1:def_10;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A4: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A5: m + 1 >= 0 by NAT_1:2;
 IC in dom p by AMISTD_5:6;
then  IC in dom p ;
then A6: ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) = (Comput (P1,s1,(i + 1))) . (IC ) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) = (Comput (P2,s2,(i + 1))) . (IC ) ) by FUNCT_1:49;
A7: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A8: CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 and
A9: ( m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 ) ; ::_thesis: ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )
A10: CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, A2, AMISTD_5:7;
A11: now__::_thesis:_(_(Comput_(P2,s2,i))_._(DataLoc_(((Comput_(P2,s2,i))_._a),k1))_<_0_implies_not_(Comput_(P1,s1,i))_._(DataLoc_(((Comput_(P1,s1,i))_._a),k1))_>=_0_)
assume that
A12: (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 and
A13: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) >= 0 ; ::_thesis: contradiction
A14: (Comput (P1,s1,(i + 1))) . (IC ) = ICplusConst ((Comput (P1,s1,i)),k2) by A4, A8, A13, SCMPDS_2:57;
(Comput (P2,s2,(i + 1))) . (IC ) = succ (IC (Comput (P2,s2,i))) by A10, A7, A8, A12, SCMPDS_2:57
.= ICplusConst ((Comput (P2,s2,i)),1) by Th10 ;
hence  contradiction by A6, A3, A9, A5, A14, Th8; ::_thesis: verum
end;
now__::_thesis:_(_(Comput_(P1,s1,i))_._(DataLoc_(((Comput_(P1,s1,i))_._a),k1))_<_0_implies_not_(Comput_(P2,s2,i))_._(DataLoc_(((Comput_(P2,s2,i))_._a),k1))_>=_0_)
assume that
A15: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 and
A16: (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) >= 0 ; ::_thesis: contradiction
A17: (Comput (P2,s2,(i + 1))) . (IC ) = ICplusConst ((Comput (P2,s2,i)),k2) by A10, A7, A8, A16, SCMPDS_2:57;
(Comput (P1,s1,(i + 1))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A4, A8, A15, SCMPDS_2:57
.= ICplusConst ((Comput (P1,s1,i)),1) by Th10 ;
hence  contradiction by A6, A3, A9, A5, A17, Th8; ::_thesis: verum
end;
hence  ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 ) by A11; ::_thesis: verum
end;