:: Development of Terminology for {\bf SCM}
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993-2011 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;

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;

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 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;

definition
let D be FinSequence of INT ;
let ds be Element of NAT ;
mode State-consisting of ds,D -> State of SCM means :Def1: :: SCM_1:def 1
 for k being Element of NAT st k < len D holds
it . (dl. (ds + k)) = D . (k + 1);
existence
ex b1 being State of SCM st
for k being Element of NAT st k < len D holds
b1 . (dl. (ds + k)) = D . (k + 1)
proof end;
end;

:: deftheorem Def1 defines State-consisting SCM_1:def 1 :
for D being FinSequence of INT
for ds being Element of NAT
for b3 being State of SCM holds
( b3 is State-consisting of ds,D iff for k being Element of NAT st k < len D holds
b3 . (dl. (ds + k)) = D . (k + 1) );

registration
let D be FinSequence of INT ;
let il, ds be Element of NAT ;
cluster Relation-like the carrier of SCM -defined Function-like the Object-Kind of SCM -compatible total il -started State-consisting of ds,D;
existence
ex b1 being State-consisting of ds,D st b1 is il -started
proof end;
end;

theorem :: SCM_1:1
canceled;

theorem :: SCM_1:2
canceled;

theorem :: SCM_1:3
canceled;

theorem :: SCM_1:4
canceled;

theorem :: SCM_1:5
canceled;

theorem :: SCM_1:6
canceled;

theorem :: SCM_1:7
canceled;

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
for i1, i2, i3, i4 being Integer
for il being Element of NAT
for s being b5 -started State-consisting of 0 ,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 )
proof end;

theorem Th14: :: SCM_1:14
for i1, i2 being Integer
for il being Element of NAT
for s being b3 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
proof end;

theorem Th15: :: SCM_1:15
for I1, I2 being Instruction of SCM
for F being NAT -defined the Instructions of SCM -valued total Function st <%I1%> ^ <%I2%> c= F holds
( F . 0 = I1 & F . 1 = I2 )
proof end;

Lm3: for F being NAT -defined the Instructions of SCM -valued total Function
for k being Element of NAT
for s being State of SCM holds Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k)))
proof end;

Lm4: now
let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis: for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds
( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )
let k, n be Element of NAT ; :: thesis: for s being State of SCM
for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds
( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )
let s be State of SCM; :: thesis: for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds
( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )
let a, b be Data-Location ; :: thesis: ( IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) implies ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) )
assume A1: IC (Comput (F,s,k)) = n ; :: thesis: ( ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) implies ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) )
set csk1 = Comput (F,s,(k + 1));
set csk = Comput (F,s,k);
assume A2: ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) ; :: thesis: ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 )
A3: dom F = NAT by PARTFUN1:def 4;
thus Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm3
.= Exec ((F . n),(Comput (F,s,k))) by A1, A3, PARTFUN1:def 8 ; :: thesis: IC (Comput (F,s,(k + 1))) = n + 1
hence IC (Comput (F,s,(k + 1))) = succ (IC (Comput (F,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 :: SCM_1:16
canceled;

theorem :: SCM_1:17
canceled;

theorem Th18: :: SCM_1:18
for F being NAT -defined the Instructions of SCM -valued total Function
for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = a := b holds
( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = (Comput (F,s,k)) . b & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
proof end;

theorem Th19: :: SCM_1:19
for F being NAT -defined the Instructions of SCM -valued total Function
for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = AddTo (a,b) holds
( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) + ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
proof end;

theorem Th20: :: SCM_1:20
for F being NAT -defined the Instructions of SCM -valued total Function
for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = SubFrom (a,b) holds
( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
proof end;

theorem Th21: :: SCM_1:21
for F being NAT -defined the Instructions of SCM -valued total Function
for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = MultBy (a,b) holds
( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) * ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
proof end;

theorem Th22: :: SCM_1:22
for F being NAT -defined the Instructions of SCM -valued total Function
for k, n being Element of NAT
for s being State of SCM
for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b holds
( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds
(Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
proof end;

theorem Th23: :: SCM_1:23
for F being NAT -defined the Instructions of SCM -valued total Function
for k, n being Element of NAT
for s being State of SCM
for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = SCM-goto il holds
( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
proof end;

theorem Th24: :: SCM_1:24
for F being NAT -defined the Instructions of SCM -valued total Function
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 (F,s,k)) = n & F . n = a =0_goto il holds
( ( (Comput (F,s,k)) . a = 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <> 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
proof end;

theorem Th25: :: SCM_1:25
for F being NAT -defined the Instructions of SCM -valued total Function
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 (F,s,k)) = n & F . n = a >0_goto il holds
( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )
proof end;

theorem Th26: :: SCM_1:26
( (halt SCM) `1_3 = 0 & ( for a, b being Data-Location holds (a := b) `1_3 = 1 ) & ( for a, b being Data-Location holds (AddTo (a,b)) `1_3 = 2 ) & ( for a, b being Data-Location holds (SubFrom (a,b)) `1_3 = 3 ) & ( for a, b being Data-Location holds (MultBy (a,b)) `1_3 = 4 ) & ( for a, b being Data-Location holds (Divide (a,b)) `1_3 = 5 ) & ( for i being Element of NAT holds (SCM-goto i) `1_3 = 6 ) & ( for a being Data-Location
for i being Element of NAT holds (a =0_goto i) `1_3 = 7 ) & ( for a being Data-Location
for i being Element of NAT holds (a >0_goto i) `1_3 = 8 ) ) by AMI_3:71, RECDEF_2:def 1;

theorem :: SCM_1:27
canceled;

theorem :: SCM_1:28
canceled;

theorem :: SCM_1:29
canceled;

theorem :: SCM_1:30
for i1, i2, i3, i4 being Integer
for s being State of SCM st s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds
s is State-consisting of 0 ,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>
proof end;

theorem :: SCM_1:31
for F being NAT -defined the Instructions of SCM -valued total Function st <%(halt SCM)%> c= F holds
for s being 0 -started State-consisting of 0 , <*> INT holds
( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )
proof end;

theorem :: SCM_1:32
for F being NAT -defined the Instructions of SCM -valued total Function st <%((dl. 0) := (dl. 1))%> ^ <%(halt SCM)%> c= F holds
for i1, i2 being Integer
for s being 0 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
proof end;

theorem :: SCM_1:33
for F being NAT -defined the Instructions of SCM -valued total Function st <%(AddTo ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds
for i1, i2 being Integer
for s being 0 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
proof end;

theorem :: SCM_1:34
for F being NAT -defined the Instructions of SCM -valued total Function st <%(SubFrom ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds
for i1, i2 being Integer
for s being 0 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 - i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
proof end;

theorem :: SCM_1:35
for F being NAT -defined the Instructions of SCM -valued total Function st <%(MultBy ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds
for i1, i2 being Integer
for s being 0 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 * i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
proof end;

theorem :: SCM_1:36
for F being NAT -defined the Instructions of SCM -valued total Function st <%(Divide ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds
for i1, i2 being Integer
for s being 0 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 div i2 & (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds
(Result (F,s)) . d = s . d ) )
proof end;

theorem :: SCM_1:37
for F being NAT -defined the Instructions of SCM -valued total Function st <%(SCM-goto 1)%> ^ <%(halt SCM)%> c= F holds
for i1, i2 being Integer
for s being 0 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )
proof end;

theorem :: SCM_1:38
for F being NAT -defined the Instructions of SCM -valued total Function st <%((dl. 0) =0_goto 1)%> ^ <%(halt SCM)%> c= F holds
for i1, i2 being Integer
for s being 0 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )
proof end;

theorem :: SCM_1:39
for F being NAT -defined the Instructions of SCM -valued total Function st <%((dl. 0) >0_goto 1)%> ^ <%(halt SCM)%> c= F holds
for i1, i2 being Integer
for s being 0 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) )
proof end;

theorem :: SCM_1:40
for s being State of SCM
for n being Element of NAT holds s is State-consisting of n, <*> INT
proof end;