begin
theorem
canceled;
theorem
for
s being
State of
for
k being
Nat for
p being
finite PartFunc of , 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
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 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
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 ;
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
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
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
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
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
for
i1,
i2,
i3,
i4 being
Integer for
il being
Element of
NAT for
s being
State of 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