let P1, P2 be Instruction-Sequence of SCMPDS; 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; 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; 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; ( 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 )
; 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; 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; 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; ( 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 )
; ( (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 ( (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
;
contradictionA14:
(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 ) =
(IC (Comput (P2,s2,i))) + 1
by A10, A7, A8, A12, SCMPDS_2:55
.=
ICplusConst (
(Comput (P2,s2,i)),1)
by Th9
;
hence
contradiction
by A6, A3, A9, A5, A14, Th7;
verum end;
now ( (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
;
contradictionA17:
(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 ) =
(IC (Comput (P1,s1,i))) + 1
by A4, A8, A15, SCMPDS_2:55
.=
ICplusConst (
(Comput (P1,s1,i)),1)
by Th9
;
hence
contradiction
by A6, A3, A9, A5, A17, Th7;
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; verum