begin
theorem
canceled;
theorem
canceled;
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 &
s . 0 = I1 &
s . 1
= I2 &
s . 2
= I3 &
s . 3
= I4 &
s . 4
= I5 &
s . 5
= I6 &
s . 6
= I7 &
s . 7
= I8 &
s . 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 Comput (ProgramPart s),s,(k + 1) = Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),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 (Comput (ProgramPart s),s,k) = n & ( s . n = a := b or s . n = AddTo a,b or s . n = SubFrom a,b or s . n = MultBy a,b or ( a <> b & s . n = Divide a,b ) ) holds
( Comput (ProgramPart s),s,(k + 1) = Exec (s . n),(Comput (ProgramPart s),s,k) & IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 )let s be
State of
SCM ;
for a, b being Data-Location st IC (Comput (ProgramPart s),s,k) = n & ( s . n = a := b or s . n = AddTo a,b or s . n = SubFrom a,b or s . n = MultBy a,b or ( a <> b & s . n = Divide a,b ) ) holds
( Comput (ProgramPart s),s,(k + 1) = Exec (s . n),(Comput (ProgramPart s),s,k) & IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 )let a,
b be
Data-Location ;
( IC (Comput (ProgramPart s),s,k) = n & ( s . n = a := b or s . n = AddTo a,b or s . n = SubFrom a,b or s . n = MultBy a,b or ( a <> b & s . n = Divide a,b ) ) implies ( Comput (ProgramPart s),s,(k + 1) = Exec (s . n),(Comput (ProgramPart s),s,k) & IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 ) )assume A1:
IC (Comput (ProgramPart s),s,k) = n
;
( ( s . n = a := b or s . n = AddTo a,b or s . n = SubFrom a,b or s . n = MultBy a,b or ( a <> b & s . n = Divide a,b ) ) implies ( Comput (ProgramPart s),s,(k + 1) = Exec (s . n),(Comput (ProgramPart s),s,k) & IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 ) )set csk1 =
Comput (ProgramPart s),
s,
(k + 1);
set csk =
Comput (ProgramPart s),
s,
k;
assume A2:
(
s . n = a := b or
s . n = AddTo a,
b or
s . n = SubFrom a,
b or
s . n = MultBy a,
b or (
a <> b &
s . n = Divide a,
b ) )
;
( Comput (ProgramPart s),s,(k + 1) = Exec (s . n),(Comput (ProgramPart s),s,k) & IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 )Y:
(ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k))
by AMI_1:150;
thus Comput (ProgramPart s),
s,
(k + 1) =
Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)),
(Comput (ProgramPart s),s,k)
by Lm3
.=
Exec (s . n),
(Comput (ProgramPart s),s,k)
by A1, Y, AMI_1:54
;
IC (Comput (ProgramPart s),s,(k + 1)) = n + 1hence IC (Comput (ProgramPart s),s,(k + 1)) =
succ (IC (Comput (ProgramPart s),s,k))
by A2, AMI_3:8, AMI_3:9, AMI_3:10, AMI_3:11, AMI_3:12
.=
n + 1
by A1
;
verum
end;
theorem Th18:
for
k,
n being
Element of
NAT for
s being
State of
SCM for
a,
b being
Data-Location st
IC (Comput (ProgramPart s),s,k) = n &
s . n = a := b holds
(
IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 &
(Comput (ProgramPart s),s,(k + 1)) . a = (Comput (ProgramPart s),s,k) . b & ( for
d being
Data-Location st
d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
theorem Th19:
for
k,
n being
Element of
NAT for
s being
State of
SCM for
a,
b being
Data-Location st
IC (Comput (ProgramPart s),s,k) = n &
s . n = AddTo a,
b holds
(
IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 &
(Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) + ((Comput (ProgramPart s),s,k) . b) & ( for
d being
Data-Location st
d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 (Comput (ProgramPart s),s,k) = n &
s . n = SubFrom a,
b holds
(
IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 &
(Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) - ((Comput (ProgramPart s),s,k) . b) & ( for
d being
Data-Location st
d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 (Comput (ProgramPart s),s,k) = n &
s . n = MultBy a,
b holds
(
IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 &
(Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) * ((Comput (ProgramPart s),s,k) . b) & ( for
d being
Data-Location st
d <> a holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),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 (Comput (ProgramPart s),s,k) = n &
s . n = Divide a,
b &
a <> b holds
(
IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 &
(Comput (ProgramPart s),s,(k + 1)) . a = ((Comput (ProgramPart s),s,k) . a) div ((Comput (ProgramPart s),s,k) . b) &
(Comput (ProgramPart s),s,(k + 1)) . b = ((Comput (ProgramPart s),s,k) . a) mod ((Comput (ProgramPart s),s,k) . b) & ( for
d being
Data-Location st
d <> a &
d <> b holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
theorem Th23:
theorem Th24:
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 (ProgramPart s),s,k) = n &
s . n = a =0_goto il holds
( (
(Comput (ProgramPart s),s,k) . a = 0 implies
IC (Comput (ProgramPart s),s,(k + 1)) = il ) & (
(Comput (ProgramPart s),s,k) . a <> 0 implies
IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 ) & ( for
d being
Data-Location holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
theorem Th25:
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 (ProgramPart s),s,k) = n &
s . n = a >0_goto il holds
( (
(Comput (ProgramPart s),s,k) . a > 0 implies
IC (Comput (ProgramPart s),s,(k + 1)) = il ) & (
(Comput (ProgramPart s),s,k) . a <= 0 implies
IC (Comput (ProgramPart s),s,(k + 1)) = n + 1 ) & ( for
d being
Data-Location holds
(Comput (ProgramPart s),s,(k + 1)) . d = (Comput (ProgramPart s),s,k) . d ) )
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
Element of
NAT holds
(SCM-goto i) `1 = 6 ) & ( for
a being
Data-Location for
i being
Element of
NAT holds
(a =0_goto i) `1 = 7 ) & ( for
a being
Data-Location for
i being
Element of
NAT 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 &
s . 0 = I1 &
s . 1
= I2 &
s . 2
= I3 &
s . 3
= I4 &
s . 4
= I5 &
s . 5
= I6 &
s . 6
= I7 &
s . 7
= I8 &
s . 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
for
i1,
i2 being
Integer for
s being
State-consisting of
0 ,
0 ,
0 ,
<%(Divide (dl. 0 ),(dl. 1))%> ^ <%(halt SCM )%>,
<*i1*> ^ <*i2*> holds
(
ProgramPart s halts_on s &
LifeSpan (ProgramPart s),
s = 1 &
(Result (ProgramPart s),s) . (dl. 0 ) = i1 div i2 &
(Result (ProgramPart s),s) . (dl. 1) = i1 mod i2 & ( for
d being
Data-Location st
d <> dl. 0 &
d <> dl. 1 holds
(Result (ProgramPart s),s) . d = s . d ) )
theorem
theorem
theorem