:: Development of Terminology for {\bf SCM}
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users
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
theorem Th4: :: SCM_1:4
theorem :: SCM_1:5
canceled;
theorem :: SCM_1:6
canceled;
theorem Th7: :: SCM_1:7
:: deftheorem Def1 defines State-consisting SCM_1:def 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 )
theorem Th15: :: SCM_1:15
theorem Th16: :: SCM_1:16
theorem Th17: :: SCM_1:17
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)
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
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 ) )
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 ) )
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 ) )
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 ) )
theorem Th23: :: SCM_1:23
theorem Th24: :: SCM_1:24
theorem Th25: :: SCM_1:25
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
theorem :: SCM_1:29
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*>
theorem :: SCM_1:31
theorem :: SCM_1:32
theorem :: SCM_1:33
theorem :: SCM_1:34
theorem :: SCM_1:35
theorem :: SCM_1:36
theorem :: SCM_1:37
theorem :: SCM_1:38
theorem :: SCM_1:39