:: SCMPDS_3 semantic presentation
theorem Th1: :: SCMPDS_3:1
for
b1 being
natural number holds
( not
b1 <= 13 or
b1 = 0 or
b1 = 1 or
b1 = 2 or
b1 = 3 or
b1 = 4 or
b1 = 5 or
b1 = 6 or
b1 = 7 or
b1 = 8 or
b1 = 9 or
b1 = 10 or
b1 = 11 or
b1 = 12 or
b1 = 13 )
theorem Th2: :: SCMPDS_3:2
theorem Th3: :: SCMPDS_3:3
theorem Th4: :: SCMPDS_3:4
theorem Th5: :: SCMPDS_3:5
theorem Th6: :: SCMPDS_3:6
theorem Th7: :: SCMPDS_3:7
theorem Th8: :: SCMPDS_3:8
theorem Th9: :: SCMPDS_3:9
theorem Th10: :: SCMPDS_3:10
theorem Th11: :: SCMPDS_3:11
theorem Th12: :: SCMPDS_3:12
theorem Th13: :: SCMPDS_3:13
theorem Th14: :: SCMPDS_3:14
theorem Th15: :: 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 Th21: :: SCMPDS_3:21
theorem Th22: :: SCMPDS_3:22
theorem Th23: :: SCMPDS_3:23
theorem Th24: :: SCMPDS_3:24
theorem Th25: :: SCMPDS_3:25
theorem Th26: :: SCMPDS_3:26
theorem Th27: :: SCMPDS_3:27
for
b1 being
autonomic non
programmed FinPartState of
SCMPDS for
b2,
b3 being
State of
SCMPDS st
b1 c= b2 &
b1 c= b3 holds
for
b4 being
Nat for
b5,
b6 being
Integer for
b7,
b8 being
Int_position st
CurInstr ((Computation b2) . b4) = MultBy b7,
b5,
b8,
b6 &
b7 in dom b1 &
DataLoc (((Computation b2) . b4) . b7),
b5 in dom b1 holds
(((Computation b2) . b4) . (DataLoc (((Computation b2) . b4) . b7),b5)) * (((Computation b2) . b4) . (DataLoc (((Computation b2) . b4) . b8),b6)) = (((Computation b3) . b4) . (DataLoc (((Computation b3) . b4) . b7),b5)) * (((Computation b3) . b4) . (DataLoc (((Computation b3) . b4) . b8),b6))
theorem Th28: :: SCMPDS_3:28
theorem Th29: :: SCMPDS_3:29
theorem Th30: :: SCMPDS_3:30
:: deftheorem Def1 SCMPDS_3:def 1 :
canceled;
:: deftheorem Def2 defines inspos SCMPDS_3:def 2 :
theorem Th31: :: SCMPDS_3:31
theorem Th32: :: SCMPDS_3:32
:: deftheorem Def3 defines + SCMPDS_3:def 3 :
:: deftheorem Def4 defines -' SCMPDS_3:def 4 :
theorem Th33: :: SCMPDS_3:33
theorem Th34: :: SCMPDS_3:34
theorem Th35: :: SCMPDS_3:35
theorem Th36: :: SCMPDS_3:36
:: deftheorem Def5 defines initial SCMPDS_3:def 5 :
:: deftheorem Def6 defines SCMPDS-Stop SCMPDS_3:def 6 :
:: deftheorem Def7 defines Shift SCMPDS_3:def 7 :
theorem Th37: :: SCMPDS_3:37
theorem Th38: :: SCMPDS_3:38
theorem Th39: :: SCMPDS_3:39
theorem Th40: :: SCMPDS_3:40
theorem Th41: :: SCMPDS_3:41