begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th18:
theorem
canceled;
theorem Th20:
theorem
canceled;
theorem Th22:
theorem
theorem
theorem
canceled;
theorem
theorem
theorem Th28:
theorem
canceled;
theorem
theorem
theorem
:: deftheorem AMI_5:def 1 :
canceled;
:: deftheorem defines @ AMI_5:def 2 :
for I being Instruction of SCM holds @ I = I;
:: deftheorem AMI_5:def 3 :
canceled;
:: deftheorem defines @ AMI_5:def 4 :
for loc being Element of SCM-Data-Loc holds loc @ = loc;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th36:
theorem Th37:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem
theorem
theorem
theorem Th58:
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
begin
theorem
canceled;
theorem
canceled;
theorem Th83:
theorem Th84:
theorem
theorem Th86:
theorem Th87:
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
I being
Instruction of
SCM st
I = CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) holds
(
IC (Comput (ProgramPart s1),s1,i) = IC (Comput (ProgramPart s2),s2,i) &
I = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,i) )
theorem
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Data-Location for
I being
Instruction of
SCM st
I = CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) &
I = AddTo da,
db &
da in dom p holds
((Comput (ProgramPart s1),s1,i) . da) + ((Comput (ProgramPart s1),s1,i) . db) = ((Comput (ProgramPart s2),s2,i) . da) + ((Comput (ProgramPart s2),s2,i) . db)
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Data-Location for
I being
Instruction of
SCM st
I = CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) &
I = SubFrom da,
db &
da in dom p holds
((Comput (ProgramPart s1),s1,i) . da) - ((Comput (ProgramPart s1),s1,i) . db) = ((Comput (ProgramPart s2),s2,i) . da) - ((Comput (ProgramPart s2),s2,i) . db)
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Data-Location for
I being
Instruction of
SCM st
I = CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) &
I = MultBy da,
db &
da in dom p holds
((Comput (ProgramPart s1),s1,i) . da) * ((Comput (ProgramPart s1),s1,i) . db) = ((Comput (ProgramPart s2),s2,i) . da) * ((Comput (ProgramPart s2),s2,i) . db)
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Data-Location for
I being
Instruction of
SCM st
I = CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) &
I = Divide da,
db &
da in dom p &
da <> db holds
((Comput (ProgramPart s1),s1,i) . da) div ((Comput (ProgramPart s1),s1,i) . db) = ((Comput (ProgramPart s2),s2,i) . da) div ((Comput (ProgramPart s2),s2,i) . db)
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Data-Location for
I being
Instruction of
SCM st
I = CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) &
I = Divide da,
db &
db in dom p holds
((Comput (ProgramPart s1),s1,i) . da) mod ((Comput (ProgramPart s1),s1,i) . db) = ((Comput (ProgramPart s2),s2,i) . da) mod ((Comput (ProgramPart s2),s2,i) . db)
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da being
Data-Location for
loc being
Element of
NAT for
I being
Instruction of
SCM st
I = CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) &
I = da =0_goto loc &
loc <> succ (IC (Comput (ProgramPart s1),s1,i)) holds
(
(Comput (ProgramPart s1),s1,i) . da = 0 iff
(Comput (ProgramPart s2),s2,i) . da = 0 )
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da being
Data-Location for
loc being
Element of
NAT for
I being
Instruction of
SCM st
I = CurInstr (ProgramPart s1),
(Comput (ProgramPart s1),s1,i) &
I = da >0_goto loc &
loc <> succ (IC (Comput (ProgramPart s1),s1,i)) holds
(
(Comput (ProgramPart s1),s1,i) . da > 0 iff
(Comput (ProgramPart s2),s2,i) . da > 0 )