begin
Lm1:
for a, A being set st A /\ {a} <> {} holds
a in A
begin
theorem Th1:
theorem
theorem Th3:
theorem
theorem
theorem
theorem Th7:
theorem
theorem Th9:
theorem
theorem
canceled;
theorem
theorem Th13:
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
begin
theorem Th34:
theorem Th35:
for
k being
natural number for
R being
good Ring for
s1,
s2,
s being
State of st not
R is
trivial holds
for
p being
autonomic FinPartState of st
IC (SCM R) in dom p &
p c= s1 &
Relocated p,
k c= s2 &
s = s1 +* (DataPart s2) holds
for
i being
Element of
NAT holds
(
(IC (Computation s1,i)) + k = IC (Computation s2,i) &
IncAddr (CurInstr (Computation s1,i)),
k = CurInstr (Computation s2,i) &
(Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) &
DataPart (Computation s,i) = DataPart (Computation s2,i) )
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem