begin
Lm1:
for a, A being set st A /\ {a} <> {} holds
a in A
begin
theorem Th1:
theorem
theorem Th3:
theorem
canceled;
theorem
theorem
theorem Th7:
theorem
theorem Th9:
theorem
theorem
canceled;
theorem
theorem Th13:
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
for
j,
k being
natural number for
R being
good Ring for
I being
Instruction of
(SCM R) for
s being
State of
(SCM R) st
IC s = il. (SCM R),
(j + k) holds
Exec I,
(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))
theorem Th24:
theorem Th25:
theorem
theorem Th27:
theorem Th28:
for
n being
Element of
NAT for
R being
good Ring for
s1,
s2 being
State of
(SCM R) st not
R is
trivial holds
for
p being non
NAT -defined autonomic FinPartState of st
p c= s1 &
p c= s2 holds
(
IC (Comput (ProgramPart s1),s1,n) = IC (Comput (ProgramPart s2),s2,n) &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),
(Comput (ProgramPart s1),s1,n) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),
(Comput (ProgramPart s2),s2,n) )
theorem Th29:
for
n being
Element of
NAT for
R being
good Ring for
a,
b being
Data-Location of
R for
s1,
s2 being
State of
(SCM R) st not
R is
trivial holds
for
p being non
NAT -defined autonomic FinPartState of st
p c= s1 &
p c= s2 &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),
(Comput (ProgramPart s1),s1,n) = a := b &
a in dom p holds
(Comput (ProgramPart s1),s1,n) . b = (Comput (ProgramPart s2),s2,n) . b
theorem Th30:
for
n being
Element of
NAT for
R being
good Ring for
a,
b being
Data-Location of
R for
s1,
s2 being
State of
(SCM R) st not
R is
trivial holds
for
p being non
NAT -defined autonomic FinPartState of st
p c= s1 &
p c= s2 &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),
(Comput (ProgramPart s1),s1,n) = AddTo a,
b &
a in dom p holds
((Comput (ProgramPart s1),s1,n) . a) + ((Comput (ProgramPart s1),s1,n) . b) = ((Comput (ProgramPart s2),s2,n) . a) + ((Comput (ProgramPart s2),s2,n) . b)
theorem Th31:
for
n being
Element of
NAT for
R being
good Ring for
a,
b being
Data-Location of
R for
s1,
s2 being
State of
(SCM R) st not
R is
trivial holds
for
p being non
NAT -defined autonomic FinPartState of st
p c= s1 &
p c= s2 &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),
(Comput (ProgramPart s1),s1,n) = SubFrom a,
b &
a in dom p holds
((Comput (ProgramPart s1),s1,n) . a) - ((Comput (ProgramPart s1),s1,n) . b) = ((Comput (ProgramPart s2),s2,n) . a) - ((Comput (ProgramPart s2),s2,n) . b)
theorem Th32:
for
n being
Element of
NAT for
R being
good Ring for
a,
b being
Data-Location of
R for
s1,
s2 being
State of
(SCM R) st not
R is
trivial holds
for
p being non
NAT -defined autonomic FinPartState of st
p c= s1 &
p c= s2 &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),
(Comput (ProgramPart s1),s1,n) = MultBy a,
b &
a in dom p holds
((Comput (ProgramPart s1),s1,n) . a) * ((Comput (ProgramPart s1),s1,n) . b) = ((Comput (ProgramPart s2),s2,n) . a) * ((Comput (ProgramPart s2),s2,n) . b)
theorem Th33:
for
n being
Element of
NAT for
R being
good Ring for
a being
Data-Location of
R for
loc being
Element of
NAT for
s1,
s2 being
State of
(SCM R) st not
R is
trivial holds
for
p being non
NAT -defined autonomic FinPartState of st
p c= s1 &
p c= s2 &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),
(Comput (ProgramPart s1),s1,n) = a =0_goto loc &
loc <> succ (IC (Comput (ProgramPart s1),s1,n)) holds
(
(Comput (ProgramPart s1),s1,n) . a = 0. R iff
(Comput (ProgramPart s2),s2,n) . a = 0. R )
begin
theorem Th34:
theorem Th35:
for
k being
natural number for
R being
good Ring for
s1,
s2,
s being
State of
(SCM R) st not
R is
trivial holds
for
p being
autonomic FinPartState of
(SCM R) 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 (Comput (ProgramPart s1),s1,i)) + k,
(SCM R) = IC (Comput (ProgramPart s2),s2,i) &
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
k = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) &
(Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) &
DataPart (Comput (ProgramPart s),s,i) = DataPart (Comput (ProgramPart s2),s2,i) )
theorem Th36:
theorem
for
k being
natural number for
R being
good Ring for
s being
State of
(SCM R) st not
R is
trivial holds
for
p being
autonomic FinPartState of
(SCM R) st
IC (SCM R) in dom p &
p c= s holds
for
i being
Element of
NAT holds
Comput (ProgramPart (s +* (Relocated p,k))),
(s +* (Relocated p,k)),
i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k,(SCM R)),(SCM R))) +* (ProgramPart (Relocated p,k))
theorem Th38:
for
k being
natural number for
R being
good Ring for
s being
State of
(SCM R) st not
R is
trivial holds
for
p being
autonomic FinPartState of
(SCM R) st
IC (SCM R) in dom p &
Relocated p,
k c= s holds
for
i being
Element of
NAT holds
Comput (ProgramPart s),
s,
i = (((Comput (ProgramPart (s +* p)),(s +* p),i) +* (Start-At ((IC (Comput (ProgramPart (s +* p)),(s +* p),i)) + k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))
theorem Th39:
for
k being
natural number for
R being
good Ring for
p being
FinPartState of
(SCM R) for
s being
State of
(SCM R) st not
R is
trivial &
IC (SCM R) in dom p &
p c= s &
Relocated p,
k is
autonomic holds
for
i being
Element of
NAT holds
Comput (ProgramPart s),
s,
i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k,(SCM R)),(SCM R))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
theorem Th40:
theorem Th41:
theorem