begin
theorem
theorem
theorem
theorem Th4:
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
begin
theorem
canceled;
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Int-Location for
f being
FinSeq-Location st
CurInstr (Computation s1,i) = f,
db := da &
f in dom p holds
for
k1,
k2 being
Element of
NAT st
k1 = abs ((Computation s1,i) . db) &
k2 = abs ((Computation s2,i) . db) holds
((Computation s1,i) . f) +* k1,
((Computation s1,i) . da) = ((Computation s2,i) . f) +* k2,
((Computation s2,i) . da)
theorem
theorem