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 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 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 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 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 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 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 ;
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 ) = (IC (Comput (P2,s2,i))) + 1 by A10, A7, A8, A12, SCMPDS_2:57
.= ICplusConst ((Comput (P2,s2,i)),1) by Th9 ;
hence contradiction by A6, A3, A9, A5, A14, Th7; :: 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 ) = (IC (Comput (P1,s1,i))) + 1 by A4, A8, A15, SCMPDS_2:57
.= ICplusConst ((Comput (P1,s1,i)),1) by Th9 ;
hence contradiction by A6, A3, A9, A5, A17, Th7; :: 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