begin
theorem
canceled;
theorem
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 AMI_3:4, SCMNORM:def 4;
theorem Th3:
theorem Th4:
theorem
canceled;
theorem
canceled;
theorem Th7:
:: deftheorem Def1 defines State-consisting SCM_1:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
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:
theorem Th16:
theorem Th17:
Lm3:
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)
Lm4:
now
let k,
n be
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 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 ;
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 ;
( 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
;
( ( 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 csk1 =
Computation s,
(k + 1);
set csk =
Computation s,
k;
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 ) )
;
( 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 Lm3
.=
Exec (s . (il. n)),
(Computation s,k)
by A1, AMI_1:54
;
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
;
verum
end;
theorem Th18:
theorem Th19:
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:
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:
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:
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:
theorem Th24:
theorem Th25:
theorem Th26:
(
(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
canceled;
theorem
theorem
theorem
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
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem