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

A10: now

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

end;

now

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

end;

hence ( (Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . a),k1) > 0 iff (Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . a),k1) > 0 ) by A10; :: thesis: verum