:: Computation in { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 7, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: SCMFSA_3:1
theorem :: SCMFSA_3:2
theorem :: SCMFSA_3:3
theorem Th4: :: SCMFSA_3:4
theorem :: SCMFSA_3:5
canceled;
theorem :: SCMFSA_3:6
canceled;
theorem :: SCMFSA_3:7
canceled;
theorem :: SCMFSA_3:8
canceled;
theorem :: SCMFSA_3:9
canceled;
theorem :: SCMFSA_3:10
theorem :: SCMFSA_3:11
theorem :: SCMFSA_3:12
theorem :: SCMFSA_3:13
canceled;
theorem Th14: :: SCMFSA_3:14
theorem Th15: :: SCMFSA_3:15
theorem :: SCMFSA_3:16
theorem Th17: :: SCMFSA_3:17
theorem Th18: :: SCMFSA_3:18
theorem :: SCMFSA_3:19
theorem :: SCMFSA_3:20
theorem :: SCMFSA_3:21
theorem :: SCMFSA_3:22
theorem :: SCMFSA_3:23
theorem :: SCMFSA_3:24
theorem :: SCMFSA_3:25
theorem :: SCMFSA_3:26
theorem :: SCMFSA_3:27
theorem :: SCMFSA_3:28
for
p being
autonomic non
programmed FinPartState of
SCM+FSA 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 (Computation s1,i) = f,
db := da &
f in dom p holds
for
k1,
k2 being
Element of
NAT st
k1 = abs ((Computation s1,i) . db) &
k2 = abs ((Computation s2,i) . db) holds
((Computation s1,i) . f) +* k1,
((Computation s1,i) . da) = ((Computation s2,i) . f) +* k2,
((Computation s2,i) . da)
theorem :: SCMFSA_3:29
theorem :: SCMFSA_3:30