begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
theorem Th7:
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
begin
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT holds
(
IC (Comput (ProgramPart s1),s1,i) = IC (Comput (ProgramPart s2),s2,i) &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) )
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = a,
k1 := b,
k2 &
a in dom p &
DataLoc ((Comput (ProgramPart s1),s1,i) . a),
k1 in dom p holds
(Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . b),k2) = (Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . b),k2)
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = AddTo a,
k1,
b,
k2 &
a in dom p &
DataLoc ((Comput (ProgramPart s1),s1,i) . a),
k1 in dom p holds
(Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . b),k2) = (Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . b),k2)
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = SubFrom a,
k1,
b,
k2 &
a in dom p &
DataLoc ((Comput (ProgramPart s1),s1,i) . a),
k1 in dom p holds
(Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . b),k2) = (Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . b),k2)
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = MultBy a,
k1,
b,
k2 &
a in dom p &
DataLoc ((Comput (ProgramPart s1),s1,i) . a),
k1 in dom p holds
((Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . a),k1)) * ((Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . b),k2)) = ((Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . a),k1)) * ((Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . b),k2))
theorem
for
p being non
NAT -defined autonomic FinPartState of
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 )
theorem
for
p being non
NAT -defined autonomic FinPartState of
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 )
theorem
for
p being non
NAT -defined autonomic FinPartState of
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 )