let p be non NAT -defined autonomic FinPartState of ; :: thesis: for s1, s2 being State of st p c= s1 & p c= s2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (Computation s1,i) = a,k1 >=0_goto k2 & m = IC (Computation s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 iff (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) < 0 )
let s1, s2 be State of ; :: thesis: ( p c= s1 & p c= s2 implies for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (Computation s1,i) = a,k1 >=0_goto k2 & m = IC (Computation s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 iff (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) < 0 ) )
assume A1: ( p c= s1 & p c= s2 ) ; :: thesis: for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (Computation s1,i) = a,k1 >=0_goto k2 & m = IC (Computation s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 iff (Computation s2,i) . (DataLoc ((Computation 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 (Computation s1,i) = a,k1 >=0_goto k2 & m = IC (Computation s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 iff (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) < 0 )
let a be Int_position ; :: thesis: for k1, k2 being Integer st CurInstr (Computation s1,i) = a,k1 >=0_goto k2 & m = IC (Computation s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 iff (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) < 0 )
let k1, k2 be Integer; :: thesis: ( CurInstr (Computation s1,i) = a,k1 >=0_goto k2 & m = IC (Computation s1,i) & m + k2 >= 0 & k2 <> 1 implies ( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 iff (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) < 0 ) )
set Cs1i = Computation s1,i;
set Cs2i = Computation s2,i;
set Cs1i1 = Computation s1,(i + 1);
set Cs2i1 = Computation s2,(i + 1);
A2: ( IC (Computation s1,i) = IC (Computation s2,i) & (Computation s1,(i + 1)) | (dom p) = (Computation s2,(i + 1)) | (dom p) ) by A1, Th23, AMI_1:def 25;
set I = CurInstr (Computation s1,i);
A3: Computation s1,(i + 1) = Following (Computation s1,i) by AMI_1:14
.= Exec (CurInstr (Computation s1,i)),(Computation s1,i) ;
A4: m + 1 >= 0 by NAT_1:2;
A5: ( ((Computation s1,(i + 1)) | (dom p)) . (IC SCMPDS ) = (Computation s1,(i + 1)) . (IC SCMPDS ) & ((Computation s2,(i + 1)) | (dom p)) . (IC SCMPDS ) = (Computation s2,(i + 1)) . (IC SCMPDS ) ) by Th17, FUNCT_1:72;
A6: Computation s2,(i + 1) = Following (Computation s2,i) by AMI_1:14
.= Exec (CurInstr (Computation s2,i)),(Computation s2,i) ;
assume that
A7: CurInstr (Computation s1,i) = a,k1 >=0_goto k2 and
A8: ( m = IC (Computation s1,i) & m + k2 >= 0 & k2 <> 1 ) ; :: thesis: ( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 iff (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) < 0 )
A9: CurInstr (Computation s1,i) = CurInstr (Computation s2,i) by A1, Th23;

A10: now

assume that
A11: (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) < 0 and
A12: (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) >= 0 ; :: thesis: contradiction
A13: (Computation s1,(i + 1)) . (IC SCMPDS ) = ICplusConst (Computation s1,i),k2 by A3, A7, A12, SCMPDS_2:69;
(Computation s2,(i + 1)) . (IC SCMPDS ) = Next (IC (Computation s2,i)) by A9, A6, A7, A11, SCMPDS_2:69
.= ICplusConst (Computation s2,i),1 by Th20 ;
hence contradiction by A5, A2, A8, A4, A13, Th18; :: thesis: verum

end;

now

assume that
A14: (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 and
A15: (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) >= 0 ; :: thesis: contradiction
A16: (Computation s2,(i + 1)) . (IC SCMPDS ) = ICplusConst (Computation s2,i),k2 by A9, A6, A7, A15, SCMPDS_2:69;
(Computation s1,(i + 1)) . (IC SCMPDS ) = Next (IC (Computation s1,i)) by A3, A7, A14, SCMPDS_2:69
.= ICplusConst (Computation s1,i),1 by Th20 ;
hence contradiction by A5, A2, A8, A4, A16, Th18; :: thesis: verum

end;

hence ( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 iff (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) < 0 ) by A10; :: thesis: verum