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

registration

let i1 be Integer;

cluster <%i1%> -> INT -valued ;

coherence
<%i1%> is INT -valued ;
let i2 be Integer;

cluster <%i1,i2%> -> INT -valued ;

coherence
<%i1,i2%> is INT -valued ;
let i3 be Integer;

cluster <%i1,i2,i3%> -> INT -valued ;

coherence
<%i1,i2,i3%> is INT -valued ;
let i4 be Integer;

cluster <%i1,i2,i3,i4%> -> INT -valued ;

coherence
<%i1,i2,i3,i4%> is INT -valued ;

end;

definition

let D be XFinSequence of INT ;

mode State-consisting of D -> State of SCM means :Def1: :: SCM_1:def 1
for k being Element of NAT st k < len D holds
it . (dl. k) = D . k;

existence
ex b₁ being State of SCM st
for k being Element of NAT st k < len D holds
b₁ . (dl. k) = D . k

proof end;

end;

:: deftheorem Def1 defines State-consisting SCM_1:def 1 :
for D being XFinSequence of INT
for b₂ being State of SCM holds
( b₂ is State-consisting of D iff for k being Element of NAT st k < len D holds
b₂ . (dl. k) = D . k );

registration

let D be XFinSequence of INT ;
let il be Element of NAT ;

cluster V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total il -started for State-consisting of D;

existence
ex b₁ being State-consisting of D st b₁ is il -started

proof end;

end;

theorem :: SCM_1:1

for i1, i2, i3, i4 being Integer
for il being Element of NAT
for s being b₅ -started State-consisting of <%i1,i2,i3,i4%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 )

proof end;

theorem Th2: :: SCM_1:2

for i1, i2 being Integer
for il being Element of NAT
for s being b₃ -started State-consisting of <%i1,i2%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 )

proof end;

theorem Th3: :: SCM_1:3

for I1, I2 being Instruction of SCM
for F being NAT -defined the InstructionsF of SCM -valued total Function st <%I1%> ^ <%I2%> c= F holds
( F . 0 = I1 & F . 1 = I2 )

proof end;

Lm1: for F being NAT -defined the InstructionsF of SCM -valued total Function
for k being 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;

Lm2: now :: thesis: for F being NAT -defined the InstructionsF 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 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 F be NAT -defined the InstructionsF 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 2;
thus Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm1
.= Exec ((F . n),(Comput (F,s,k))) by A1, A3, PARTFUN1:def 6 ; :: thesis: IC (Comput (F,s,(k + 1))) = n + 1
hence IC (Comput (F,s,(k + 1))) = (IC (Comput (F,s,k))) + 1 by A2, AMI_3:2, AMI_3:3, AMI_3:4, AMI_3:5, AMI_3:6
.= n + 1 by A1 ;
:: thesis: verum

end;

theorem Th4: :: SCM_1:4

for F being NAT -defined the InstructionsF 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 Th5: :: SCM_1:5

for F being NAT -defined the InstructionsF 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 Th6: :: SCM_1:6

for F being NAT -defined the InstructionsF 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 Th7: :: SCM_1:7

for F being NAT -defined the InstructionsF 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 Th8: :: SCM_1:8

for F being NAT -defined the InstructionsF 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 Th9: :: SCM_1:9

for F being NAT -defined the InstructionsF 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 Th10: :: SCM_1:10

for F being NAT -defined the InstructionsF of SCM -valued total Function
for k, n being 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 Th11: :: SCM_1:11

for F being NAT -defined the InstructionsF 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 Th12: :: SCM_1:12

( (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:26;

theorem :: SCM_1:13

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 <%i1,i2,i3,i4%>

proof end;

:: Empty program

theorem :: SCM_1:14

for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(halt SCM)%> c= F holds
for s being 0 -started State-consisting of <*> INT holds
( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )

proof end;

:: Assignment

theorem :: SCM_1:15

for F being NAT -defined the InstructionsF 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 <%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;

:: Adding two integers

theorem :: SCM_1:16

for F being NAT -defined the InstructionsF 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 <%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;

:: Subtracting two integers

theorem :: SCM_1:17

for F being NAT -defined the InstructionsF 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 <%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;

:: Multiplying two integers

theorem :: SCM_1:18

for F being NAT -defined the InstructionsF 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 <%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;

:: Dividing two integers

theorem :: SCM_1:19

for F being NAT -defined the InstructionsF 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 <%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;

:: Unconditional jump

theorem :: SCM_1:20

for F being NAT -defined the InstructionsF 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 <%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;

:: Jump at zero

theorem :: SCM_1:21

for F being NAT -defined the InstructionsF 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 <%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;

:: Jump at greater than zero

theorem :: SCM_1:22

for F being NAT -defined the InstructionsF 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 <%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:23

for s being State of SCM holds s is State-consisting of <*> INT

proof end;