:: Development of Terminology for {\bf SCM}
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users

definition

let i be Integer;
:: original: <*
redefine func <*i*> -> FinSequence of INT ;
coherence
<*i*> is FinSequence of INT

proof end;

end;

theorem :: SCM_1:1

canceled;

theorem :: SCM_1:2

for s being State of SCM
for k being Nat
for p being finite PartFunc of NAT ,the Instructions of SCM st IC (Comput p,s,k) in dom p holds
( CurInstr p,(Comput p,s,k) = p . (IC (Comput p,s,k)) & CurInstr p,(Comput p,s,k) = p . ((Comput p,s,k) . NAT ) ) by SCMNORM:def 4, AMI_3:4;

theorem Th3: :: SCM_1:3

for s being State of SCM st ex k being Element of NAT st s . (IC (Computation s,k)) = halt SCM holds
s is halting

proof end;

theorem Th4: :: SCM_1:4

for s being State of SCM
for k being Element of NAT st s . (IC (Computation s,k)) = halt SCM holds
Result s = Computation s,k

proof end;

theorem :: SCM_1:5

canceled;

theorem :: SCM_1:6

canceled;

theorem Th7: :: SCM_1:7

for n, m being Element of NAT holds
( IC SCM <> il. n & IC SCM <> dl. n & il. n <> dl. m ) by AMI_3:56, AMI_3:57;

Lm1: now

let p be FinSequence; :: thesis: for n being Element of NAT st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
let n be Element of NAT ; :: thesis: ( n < len p implies ( n + 1 in dom p & p . (n + 1) in rng p ) )
assume n < len p ; :: thesis: ( n + 1 in dom p & p . (n + 1) in rng p )
then ( n + 1 >= 0 + 1 & n + 1 <= len p ) by NAT_1:13;
then ( n + 1 in dom p & dom p = Seg (len p) ) by FINSEQ_1:def 3, FINSEQ_3:27;
hence ( n + 1 in dom p & p . (n + 1) in rng p ) by FUNCT_1:def 5; :: thesis: verum

end;

Lm2: now

let n be Element of NAT ; :: thesis: for x being set
for p being FinSequence of x st n < len p holds
p . (n + 1) in x
let x be set ; :: thesis: for p being FinSequence of x st n < len p holds
p . (n + 1) in x
let p be FinSequence of x; :: thesis: ( n < len p implies p . (n + 1) in x )
assume n < len p ; :: thesis: p . (n + 1) in x
then ( p . (n + 1) in rng p & rng p c= x ) by Lm1, FINSEQ_1:def 4;
hence p . (n + 1) in x ; :: thesis: verum

end;

definition

let I be FinSequence of the Instructions of SCM ;
let D be FinSequence of INT ;
let il, ps, ds be Element of NAT ;
mode State-consisting of il,ps,ds,I,D -> State of SCM means :Def1: :: SCM_1:def 1
( IC it = il. il & ( for k being Element of NAT st k < len I holds
it . (il. (ps + k)) = I . (k + 1) ) & ( for k being Element of NAT st k < len D holds
it . (dl. (ds + k)) = D . (k + 1) ) );
existence
ex b₁ being State of SCM st
( IC b₁ = il. il & ( for k being Element of NAT st k < len I holds
b₁ . (il. (ps + k)) = I . (k + 1) ) & ( for k being Element of NAT st k < len D holds
b₁ . (dl. (ds + k)) = D . (k + 1) ) )

proof end;

end;

:: deftheorem Def1 defines State-consisting SCM_1:def 1 :

for I being FinSequence of the Instructions of SCM
for D being FinSequence of INT
for il, ps, ds being Element of NAT
for b₆ being State of SCM holds
( b₆ is State-consisting of il,ps,ds,I,D iff ( IC b₆ = il. il & ( for k being Element of NAT st k < len I holds
b₆ . (il. (ps + k)) = I . (k + 1) ) & ( for k being Element of NAT st k < len D holds
b₆ . (dl. (ds + k)) = D . (k + 1) ) ) );

theorem :: SCM_1:8

canceled;

theorem :: SCM_1:9

canceled;

theorem :: SCM_1:10

canceled;

theorem :: SCM_1:11

canceled;

theorem :: SCM_1:12

canceled;

theorem :: SCM_1:13

canceled;

theorem :: SCM_1:14

for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM
for i1, i2, i3, i4 being Integer
for il being Element of NAT
for s being State-consisting of il, 0 , 0 ,(((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> holds
( IC s = il. il & s . (il. 0 ) = I1 & s . (il. 1) = I2 & s . (il. 2) = I3 & s . (il. 3) = I4 & s . (il. 4) = I5 & s . (il. 5) = I6 & s . (il. 6) = I7 & s . (il. 7) = I8 & s . (il. 8) = I9 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 )

proof end;

theorem Th15: :: SCM_1:15

for I1, I2 being Instruction of SCM
for i1, i2 being Integer
for il being Element of NAT
for s being State-consisting of il, 0 , 0 ,<*I1*> ^ <*I2*>,<*i1*> ^ <*i2*> holds
( IC s = il. il & s . (il. 0 ) = I1 & s . (il. 1) = I2 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 )

proof end;

theorem Th16: :: SCM_1:16

for s being State of SCM
for k being Element of NAT holds
( s . (IC (Computation s,k)) <> halt SCM & s . (IC (Computation s,(k + 1))) = halt SCM iff ( LifeSpan s = k + 1 & s is halting ) )

proof end;

theorem Th17: :: SCM_1:17

for s being State of SCM
for k being Element of NAT st IC (Computation s,k) <> IC (Computation s,(k + 1)) & s . (IC (Computation s,(k + 1))) = halt SCM holds
LifeSpan s = k + 1

proof end;

Lm4: for k being Element of NAT
for s being State of SCM holds Computation s,(k + 1) = Exec (CurInstr (Computation s,k)),(Computation s,k)

proof end;

Lm5: now

let k, n be Element of NAT ; :: thesis: for s being State of SCM
for a, b being Data-Location st IC (Computation s,k) = il. n & ( s . (il. n) = a := b or s . (il. n) = AddTo a,b or s . (il. n) = SubFrom a,b or s . (il. n) = MultBy a,b or ( a <> b & s . (il. n) = Divide a,b ) ) holds
( Computation s,(k + 1) = Exec (s . (il. n)),(Computation s,k) & IC (Computation s,(k + 1)) = il. (n + 1) )
let s be State of SCM ; :: thesis: for a, b being Data-Location st IC (Computation s,k) = il. n & ( s . (il. n) = a := b or s . (il. n) = AddTo a,b or s . (il. n) = SubFrom a,b or s . (il. n) = MultBy a,b or ( a <> b & s . (il. n) = Divide a,b ) ) holds
( Computation s,(k + 1) = Exec (s . (il. n)),(Computation s,k) & IC (Computation s,(k + 1)) = il. (n + 1) )
let a, b be Data-Location ; :: thesis: ( IC (Computation s,k) = il. n & ( s . (il. n) = a := b or s . (il. n) = AddTo a,b or s . (il. n) = SubFrom a,b or s . (il. n) = MultBy a,b or ( a <> b & s . (il. n) = Divide a,b ) ) implies ( Computation s,(k + 1) = Exec (s . (il. n)),(Computation s,k) & IC (Computation s,(k + 1)) = il. (n + 1) ) )
assume A1: IC (Computation s,k) = il. n ; :: thesis: ( ( s . (il. n) = a := b or s . (il. n) = AddTo a,b or s . (il. n) = SubFrom a,b or s . (il. n) = MultBy a,b or ( a <> b & s . (il. n) = Divide a,b ) ) implies ( Computation s,(k + 1) = Exec (s . (il. n)),(Computation s,k) & IC (Computation s,(k + 1)) = il. (n + 1) ) )
set csk = Computation s,k;
set csk1 = Computation s,(k + 1);
assume A2: ( s . (il. n) = a := b or s . (il. n) = AddTo a,b or s . (il. n) = SubFrom a,b or s . (il. n) = MultBy a,b or ( a <> b & s . (il. n) = Divide a,b ) ) ; :: thesis: ( Computation s,(k + 1) = Exec (s . (il. n)),(Computation s,k) & IC (Computation s,(k + 1)) = il. (n + 1) )
thus Computation s,(k + 1) = Exec (CurInstr (Computation s,k)),(Computation s,k) by Lm4
.= Exec (s . (il. n)),(Computation s,k) by A1, AMI_1:54 ; :: thesis: IC (Computation s,(k + 1)) = il. (n + 1)
hence IC (Computation s,(k + 1)) = Next (IC (Computation s,k)) by A2, AMI_3:8, AMI_3:9, AMI_3:10, AMI_3:11, AMI_3:12
.= il. (n + 1) by A1 ;
:: thesis: verum

end;

theorem Th18: :: SCM_1:18

for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Computation s,k) = il. n & s . (il. n) = a := b holds
( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = (Computation s,k) . b & ( for d being Data-Location st d <> a holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) )

proof end;

theorem Th19: :: SCM_1:19

for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Computation s,k) = il. n & s . (il. n) = AddTo a,b holds
( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) + ((Computation s,k) . b) & ( for d being Data-Location st d <> a holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) )

proof end;

theorem Th20: :: SCM_1:20

for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Computation s,k) = il. n & s . (il. n) = SubFrom a,b holds
( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) - ((Computation s,k) . b) & ( for d being Data-Location st d <> a holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) )

proof end;

theorem Th21: :: SCM_1:21

for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Computation s,k) = il. n & s . (il. n) = MultBy a,b holds
( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) * ((Computation s,k) . b) & ( for d being Data-Location st d <> a holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) )

proof end;

theorem Th22: :: SCM_1:22

for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Computation s,k) = il. n & s . (il. n) = Divide a,b & a <> b holds
( IC (Computation s,(k + 1)) = il. (n + 1) & (Computation s,(k + 1)) . a = ((Computation s,k) . a) div ((Computation s,k) . b) & (Computation s,(k + 1)) . b = ((Computation s,k) . a) mod ((Computation s,k) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Computation s,(k + 1)) . d = (Computation s,k) . d ) )

proof end;

theorem Th23: :: SCM_1:23

for k, n being Element of NAT
for s being State of SCM
for il being Instruction-Location of SCM st IC (Computation s,k) = il. n & s . (il. n) = goto il holds
( IC (Computation s,(k + 1)) = il & ( for d being Data-Location holds (Computation s,(k + 1)) . d = (Computation s,k) . d ) )

proof end;

theorem Th24: :: SCM_1:24

for k, n being Element of NAT
for s being State of SCM
for a being Data-Location
for il being Instruction-Location of SCM st IC (Computation s,k) = il. n & s . (il. n) = a =0_goto il holds
( ( (Computation s,k) . a = 0 implies IC (Computation s,(k + 1)) = il ) & ( (Computation s,k) . a <> 0 implies IC (Computation s,(k + 1)) = il. (n + 1) ) & ( for d being Data-Location holds (Computation s,(k + 1)) . d = (Computation s,k) . d ) )

proof end;

theorem Th25: :: SCM_1:25

for k, n being Element of NAT
for s being State of SCM
for a being Data-Location
for il being Instruction-Location of SCM st IC (Computation s,k) = il. n & s . (il. n) = a >0_goto il holds
( ( (Computation s,k) . a > 0 implies IC (Computation s,(k + 1)) = il ) & ( (Computation s,k) . a <= 0 implies IC (Computation s,(k + 1)) = il. (n + 1) ) & ( for d being Data-Location holds (Computation s,(k + 1)) . d = (Computation s,k) . d ) )

proof end;

theorem Th26: :: SCM_1:26

( (halt SCM ) `1 = 0 & ( for a, b being Data-Location holds (a := b) `1 = 1 ) & ( for a, b being Data-Location holds (AddTo a,b) `1 = 2 ) & ( for a, b being Data-Location holds (SubFrom a,b) `1 = 3 ) & ( for a, b being Data-Location holds (MultBy a,b) `1 = 4 ) & ( for a, b being Data-Location holds (Divide a,b) `1 = 5 ) & ( for i being Instruction-Location of SCM holds (goto i) `1 = 6 ) & ( for a being Data-Location
for i being Instruction-Location of SCM holds (a =0_goto i) `1 = 7 ) & ( for a being Data-Location
for i being Instruction-Location of SCM holds (a >0_goto i) `1 = 8 ) ) by AMI_3:71, MCART_1:7;

theorem :: SCM_1:27

canceled;

theorem :: SCM_1:28

for s1, s2 being State of SCM
for k, c being Element of NAT st s2 = Computation s1,k & LifeSpan s2 = c & s2 is halting & 0 < c holds
LifeSpan s1 = k + c

proof end;

theorem :: SCM_1:29

for s1, s2 being State of SCM
for k being Element of NAT st s2 = Computation s1,k & s2 is halting holds
Result s2 = Result s1

proof end;

theorem :: SCM_1:30

for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM
for i1, i2, i3, i4 being Integer
for il being Element of NAT
for s being State of SCM st IC s = il. il & s . (il. 0 ) = I1 & s . (il. 1) = I2 & s . (il. 2) = I3 & s . (il. 3) = I4 & s . (il. 4) = I5 & s . (il. 5) = I6 & s . (il. 6) = I7 & s . (il. 7) = I8 & s . (il. 8) = I9 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds
s is State-consisting of il, 0 , 0 ,(((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>

proof end;

theorem :: SCM_1:31

for s being State-consisting of 0 , 0 , 0 ,<*(halt SCM )*>, <*> INT holds
( s is halting & LifeSpan s = 0 & Result s = s )

proof end;

theorem :: SCM_1:32

for i1, i2 being Integer
for s being State-consisting of 0 , 0 , 0 ,<*((dl. 0 ) := (dl. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & LifeSpan s = 1 & (Result s) . (dl. 0 ) = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:33

for i1, i2 being Integer
for s being State-consisting of 0 , 0 , 0 ,<*(AddTo (dl. 0 ),(dl. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & LifeSpan s = 1 & (Result s) . (dl. 0 ) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:34

for i1, i2 being Integer
for s being State-consisting of 0 , 0 , 0 ,<*(SubFrom (dl. 0 ),(dl. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & LifeSpan s = 1 & (Result s) . (dl. 0 ) = i1 - i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:35

for i1, i2 being Integer
for s being State-consisting of 0 , 0 , 0 ,<*(MultBy (dl. 0 ),(dl. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & LifeSpan s = 1 & (Result s) . (dl. 0 ) = i1 * i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:36

for i1, i2 being Integer
for s being State-consisting of 0 , 0 , 0 ,<*(Divide (dl. 0 ),(dl. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & LifeSpan s = 1 & (Result s) . (dl. 0 ) = i1 div i2 & (Result s) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:37

for i1, i2 being Integer
for s being State-consisting of 0 , 0 , 0 ,<*(goto (il. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & LifeSpan s = 1 & ( for d being Data-Location holds (Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:38

for i1, i2 being Integer
for s being State-consisting of 0 , 0 , 0 ,<*((dl. 0 ) =0_goto (il. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & LifeSpan s = 1 & ( for d being Data-Location holds (Result s) . d = s . d ) )

proof end;

theorem :: SCM_1:39

for i1, i2 being Integer
for s being State-consisting of 0 , 0 , 0 ,<*((dl. 0 ) >0_goto (il. 1))*> ^ <*(halt SCM )*>,<*i1*> ^ <*i2*> holds
( s is halting & LifeSpan s = 1 & ( for d being Data-Location holds (Result s) . d = s . d ) )

proof end;