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

begin

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

canceled;

theorem Th3: :: SCM_1:3

for s being State of SCM st ex k being Element of NAT st s . (IC (Comput (ProgramPart s),s,k)) = halt SCM holds
ProgramPart s halts_on s

proof end;

theorem Th4: :: SCM_1:4

for s being State of SCM
for k being Element of NAT st s . (IC (Comput (ProgramPart s),s,k)) = halt SCM holds
Result s = Comput (ProgramPart s),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 <> n & IC SCM <> dl. n & 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 by FINSEQ_3:27;
hence ( n + 1 in dom p & p . (n + 1) in rng p ) by FUNCT_1:def 5; :: thesis: verum

end;

Lm29: 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 A1: p . (n + 1) in rng p by Lm1;
rng p c= x by FINSEQ_1:def 4;
hence p . (n + 1) in x by A1; :: thesis: verum

end;

Lm1: now

let p be XFinSequence; :: thesis: for n being Element of NAT st n < len p holds
( n in dom p & p . n in rng p )
let n be Element of NAT ; :: thesis: ( n < len p implies ( n in dom p & p . n in rng p ) )
assume n < len p ; :: thesis: ( n in dom p & p . n in rng p )
hence n in dom p by NAT_1:45; :: thesis: p . n in rng p
hence p . n 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 XFinSequence of x st n < len p holds
p . n in x
let x be set ; :: thesis: for p being XFinSequence of x st n < len p holds
p . n in x
let p be XFinSequence of x; :: thesis: ( n < len p implies p . n in x )
assume n < len p ; :: thesis: p . n in x
then A1: p . n in rng p by Lm1;
rng p c= x by RELAT_1:def 19;
hence p . n in x by A1; :: thesis: verum

end;

definition

let I be XFinSequence 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 & ( for k being Element of NAT st k < len I holds
it . (ps + k) = I . k ) & ( 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 & ( for k being Element of NAT st k < len I holds
b₁ . (ps + k) = I . k ) & ( 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 XFinSequence 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 & ( for k being Element of NAT st k < len I holds
b₆ . (ps + k) = I . k ) & ( 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 & s . 0 = I1 & s . 1 = I2 & s . 2 = I3 & s . 3 = I4 & s . 4 = I5 & s . 5 = I6 & s . 6 = I7 & s . 7 = I8 & s . 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 & s . 0 = I1 & s . 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 (Comput (ProgramPart s),s,k)) <> halt SCM & s . (IC (Comput (ProgramPart s),s,(k + 1))) = halt SCM iff ( LifeSpan s = k + 1 & ProgramPart s halts_on s ) )

proof end;

theorem Th17: :: SCM_1:17

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

proof end;

Lm3: for k being Element of NAT
for s being State of SCM holds Comput (ProgramPart s),s,(k + 1) = Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)

proof end;

Lm4: now

let k, n be Element of NAT ; :: thesis: for s being State of SCM
for a, b being Data-Location st IC (Comput (ProgramPart s),s,k) = n & ( s . n = a := b or s . n = AddTo a,b or s . n = SubFrom a,b or s . n = MultBy a,b or ( a <> b & s . n = Divide a,b ) ) holds
( Comput (ProgramPart s),s,(k + 1) = Exec (s . n),(Comput (ProgramPart s),s,k) & IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 )
let s be State of SCM ; :: thesis: for a, b being Data-Location st IC (Comput (ProgramPart s),s,k) = n & ( s . n = a := b or s . n = AddTo a,b or s . n = SubFrom a,b or s . n = MultBy a,b or ( a <> b & s . n = Divide a,b ) ) holds
( Comput (ProgramPart s),s,(k + 1) = Exec (s . n),(Comput (ProgramPart s),s,k) & IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 )
let a, b be Data-Location ; :: thesis: ( IC (Comput (ProgramPart s),s,k) = n & ( s . n = a := b or s . n = AddTo a,b or s . n = SubFrom a,b or s . n = MultBy a,b or ( a <> b & s . n = Divide a,b ) ) implies ( Comput (ProgramPart s),s,(k + 1) = Exec (s . n),(Comput (ProgramPart s),s,k) & IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 ) )
assume A1: IC (Comput (ProgramPart s),s,k) = n ; :: thesis: ( ( s . n = a := b or s . n = AddTo a,b or s . n = SubFrom a,b or s . n = MultBy a,b or ( a <> b & s . n = Divide a,b ) ) implies ( Comput (ProgramPart s),s,(k + 1) = Exec (s . n),(Comput (ProgramPart s),s,k) & IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 ) )
set csk1 = Comput (ProgramPart s),s,(k + 1);
set csk = Comput (ProgramPart s),s,k;
assume A2: ( s . n = a := b or s . n = AddTo a,b or s . n = SubFrom a,b or s . n = MultBy a,b or ( a <> b & s . n = Divide a,b ) ) ; :: thesis: ( Comput (ProgramPart s),s,(k + 1) = Exec (s . n),(Comput (ProgramPart s),s,k) & IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 )
Y: (ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by AMI_1:150;
thus Comput (ProgramPart s),s,(k + 1) = Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) by Lm3
.= Exec (s . n),(Comput (ProgramPart s),s,k) by A1, AMI_1:54, Y ; :: thesis: IC (Comput (ProgramPart s),s,(k + 1)) = n + 1
hence IC (Comput (ProgramPart s),s,(k + 1)) = succ (IC (Comput (ProgramPart s),s,k)) by A2, AMI_3:8, AMI_3:9, AMI_3:10, AMI_3:11, AMI_3:12
.= 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 (Comput (ProgramPart s),s,k) = n & s . n = a := b holds
( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = (Comput (ProgramPart s),s,k) . b & ( for d being Data-Location st d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 (Comput (ProgramPart s),s,k) = n & s . n = AddTo a,b holds
( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) + ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 (Comput (ProgramPart s),s,k) = n & s . n = SubFrom a,b holds
( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) - ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 (Comput (ProgramPart s),s,k) = n & s . n = MultBy a,b holds
( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) * ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 (Comput (ProgramPart s),s,k) = n & s . n = Divide a,b & a <> b holds
( IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 & (Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) div ((Comput (ProgramPart s),s,k) . b) & (Comput (ProgramPart s),s,(k + 1)) . b = ((Comput (ProgramPart s),s,k) . a) mod ((Comput (ProgramPart s),s,k) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 Element of NAT st IC (Comput (ProgramPart s),s,k) = n & s . n = SCM-goto il holds
( IC (Comput (ProgramPart s),s,(k + 1)) = il & ( for d being Data-Location holds (Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 Element of NAT st IC (Comput (ProgramPart s),s,k) = n & s . n = a =0_goto il holds
( ( (Comput (ProgramPart s),s,k) . a = 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = il ) & ( (Comput (ProgramPart s),s,k) . a <> 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 ) & ( for d being Data-Location holds (Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 Element of NAT st IC (Comput (ProgramPart s),s,k) = n & s . n = a >0_goto il holds
( ( (Comput (ProgramPart s),s,k) . a > 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = il ) & ( (Comput (ProgramPart s),s,k) . a <= 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 ) & ( for d being Data-Location holds (Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 Element of NAT holds (SCM-goto i) `1 = 6 ) & ( for a being Data-Location
for i being Element of NAT holds (a =0_goto i) `1 = 7 ) & ( for a being Data-Location
for i being Element of NAT 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 = Comput (ProgramPart s1),s1,k & LifeSpan s2 = c & ProgramPart s2 halts_on s2 & 0 < c holds
LifeSpan s1 = k + c

proof end;

theorem :: SCM_1:29

for s1 being State of SCM
for k being Element of NAT st ProgramPart s1 halts_on Comput (ProgramPart s1),s1,k holds
Result (Comput (ProgramPart s1),s1,k) = 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 & s . 0 = I1 & s . 1 = I2 & s . 2 = I3 & s . 3 = I4 & s . 4 = I5 & s . 5 = I6 & s . 6 = I7 & s . 7 = I8 & s . 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
( ProgramPart s halts_on s & 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
( ProgramPart s halts_on s & 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
( ProgramPart s halts_on s & 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
( ProgramPart s halts_on s & 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
( ProgramPart s halts_on s & 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
( ProgramPart s halts_on s & 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 ,<%(SCM-goto 1)%> ^ <%(halt SCM )%>,<*i1*> ^ <*i2*> holds
( ProgramPart s halts_on s & 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 1)%> ^ <%(halt SCM )%>,<*i1*> ^ <*i2*> holds
( ProgramPart s halts_on s & 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 1)%> ^ <%(halt SCM )%>,<*i1*> ^ <*i2*> holds
( ProgramPart s halts_on s & LifeSpan s = 1 & ( for d being Data-Location holds (Result s) . d = s . d ) )

proof end;