:: Computation and Program Shift in the SCMPDS Computer
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: SCMPDS_3:1
canceled;
theorem Th2: :: SCMPDS_3:2
theorem Th3: :: SCMPDS_3:3
theorem Th4: :: SCMPDS_3:4
theorem :: SCMPDS_3:5
theorem :: SCMPDS_3:6
theorem Th7: :: SCMPDS_3:7
theorem :: SCMPDS_3:8
theorem :: SCMPDS_3:9
canceled;
theorem :: SCMPDS_3:10
canceled;
theorem :: SCMPDS_3:11
canceled;
theorem :: SCMPDS_3:12
canceled;
theorem :: SCMPDS_3:13
theorem :: SCMPDS_3:14
theorem :: SCMPDS_3:15
theorem Th16: :: SCMPDS_3:16
theorem Th17: :: SCMPDS_3:17
theorem Th18: :: SCMPDS_3:18
theorem Th19: :: SCMPDS_3:19
theorem Th20: :: SCMPDS_3:20
theorem :: SCMPDS_3:21
theorem Th22: :: SCMPDS_3:22
theorem Th23: :: SCMPDS_3:23
theorem :: SCMPDS_3:24
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (Computation s1,i) = a,
k1 := b,
k2 &
a in dom p &
DataLoc ((Computation s1,i) . a),
k1 in dom p holds
(Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2) = (Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2)
theorem :: SCMPDS_3:25
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (Computation s1,i) = AddTo a,
k1,
b,
k2 &
a in dom p &
DataLoc ((Computation s1,i) . a),
k1 in dom p holds
(Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2) = (Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2)
theorem :: SCMPDS_3:26
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (Computation s1,i) = SubFrom a,
k1,
b,
k2 &
a in dom p &
DataLoc ((Computation s1,i) . a),
k1 in dom p holds
(Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2) = (Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2)
theorem :: SCMPDS_3:27
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i being
Element of
NAT for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (Computation s1,i) = MultBy a,
k1,
b,
k2 &
a in dom p &
DataLoc ((Computation s1,i) . a),
k1 in dom p holds
((Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1)) * ((Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2)) = ((Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1)) * ((Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2))
theorem :: SCMPDS_3:28
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i,
m being
Element of
NAT for
a being
Int_position for
k1,
k2 being
Integer st
CurInstr (Computation s1,i) = a,
k1 <>0_goto k2 &
m = IC (Computation s1,i) &
m + k2 >= 0 &
k2 <> 1 holds
(
(Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) = 0 iff
(Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) = 0 )
theorem :: SCMPDS_3:29
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i,
m being
Element of
NAT for
a being
Int_position for
k1,
k2 being
Integer st
CurInstr (Computation s1,i) = a,
k1 <=0_goto k2 &
m = IC (Computation s1,i) &
m + k2 >= 0 &
k2 <> 1 holds
(
(Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) > 0 iff
(Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) > 0 )
theorem :: SCMPDS_3:30
for
p being non
NAT -defined autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 holds
for
i,
m being
Element of
NAT for
a being
Int_position for
k1,
k2 being
Integer st
CurInstr (Computation s1,i) = a,
k1 >=0_goto k2 &
m = IC (Computation s1,i) &
m + k2 >= 0 &
k2 <> 1 holds
(
(Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 iff
(Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) < 0 )
:: deftheorem SCMPDS_3:def 1 :
canceled;
:: deftheorem defines inspos SCMPDS_3:def 2 :