begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
theorem Th7:
theorem
begin
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:
theorem
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS 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 (Computation s1,i) = a,
k1 := b,
k2 &
a in dom p &
DataLoc ((Computation s1,i) . a),
k1 in dom p holds
(Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2) = (Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2)
theorem
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS 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 (Computation s1,i) = AddTo a,
k1,
b,
k2 &
a in dom p &
DataLoc ((Computation s1,i) . a),
k1 in dom p holds
(Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2) = (Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2)
theorem
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS 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 (Computation s1,i) = SubFrom a,
k1,
b,
k2 &
a in dom p &
DataLoc ((Computation s1,i) . a),
k1 in dom p holds
(Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2) = (Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2)
theorem
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS 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 (Computation s1,i) = MultBy a,
k1,
b,
k2 &
a in dom p &
DataLoc ((Computation s1,i) . a),
k1 in dom p holds
((Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1)) * ((Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2)) = ((Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1)) * ((Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2))
theorem
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS 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 (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 )
theorem
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS 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 (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 )
theorem
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS 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 (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 )
begin
:: deftheorem SCMPDS_3:def 1 :
canceled;
:: deftheorem defines inspos SCMPDS_3:def 2 :