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:
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT holds
(
IC (Comput (ProgramPart s1),s1,i) = IC (Comput (ProgramPart s2),s2,i) &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) )
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Int-Location st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da := db &
da in dom p holds
(Comput (ProgramPart s1),s1,i) . db = (Comput (ProgramPart s2),s2,i) . db
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Int-Location st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,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+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Int-Location st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,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+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Int-Location st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,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+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Int-Location st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,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+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da,
db being
Int-Location st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,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+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da being
Int-Location for
loc being
Element of
NAT st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,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+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da being
Int-Location for
loc being
Element of
NAT st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,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+FSA 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 (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da := f,
db &
da in dom p holds
for
k1,
k2 being
Element of
NAT st
k1 = abs ((Comput (ProgramPart s1),s1,i) . db) &
k2 = abs ((Comput (ProgramPart s2),s2,i) . db) holds
((Comput (ProgramPart s1),s1,i) . f) /. k1 = ((Comput (ProgramPart s2),s2,i) . f) /. k2
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM+FSA 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 (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = f,
db := da &
f in dom p holds
for
k1,
k2 being
Element of
NAT st
k1 = abs ((Comput (ProgramPart s1),s1,i) . db) &
k2 = abs ((Comput (ProgramPart s2),s2,i) . db) holds
((Comput (ProgramPart s1),s1,i) . f) +* k1,
((Comput (ProgramPart s1),s1,i) . da) = ((Comput (ProgramPart s2),s2,i) . f) +* k2,
((Comput (ProgramPart s2),s2,i) . da)
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da being
Int-Location for
f being
FinSeq-Location st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = da :=len f &
da in dom p holds
len ((Comput (ProgramPart s1),s1,i) . f) = len ((Comput (ProgramPart s2),s2,i) . f)
theorem
for
p being non
NAT -defined autonomic FinPartState of
for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
da being
Int-Location for
f being
FinSeq-Location st
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),
(Comput (ProgramPart s1),s1,i) = f :=<0,...,0> da &
f in dom p holds
for
k1,
k2 being
Element of
NAT st
k1 = abs ((Comput (ProgramPart s1),s1,i) . da) &
k2 = abs ((Comput (ProgramPart s2),s2,i) . da) holds
k1 |-> 0 = k2 |-> 0