begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem
canceled;
:: deftheorem AMISTD_1:def 1 :
canceled;
:: deftheorem AMISTD_1:def 2 :
canceled;
:: deftheorem defines jump-only AMISTD_1:def 3 :
:: deftheorem defines jump-only AMISTD_1:def 4 :
:: deftheorem defines NIC AMISTD_1:def 5 :
Lm2:
now
let N be non
empty with_non-empty_elements set ;
for S being non empty stored-program IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for i being Element of the Instructions of S
for l being Element of NAT
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (ProgramPart (s +* f)),(s +* f)) in NIC i,llet S be non
empty stored-program IC-Ins-separated steady-programmed definite realistic AMI-Struct of
N;
for i being Element of the Instructions of S
for l being Element of NAT
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (ProgramPart (s +* f)),(s +* f)) in NIC i,llet i be
Element of the
Instructions of
S;
for l being Element of NAT
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (ProgramPart (s +* f)),(s +* f)) in NIC i,llet l be
Element of
NAT ;
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (ProgramPart (s +* f)),(s +* f)) in NIC i,llet s be
State of
S;
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (ProgramPart (s +* f)),(s +* f)) in NIC i,llet f be
FinPartState of
S;
( f = (IC S),l --> l,i implies IC (Following (ProgramPart (s +* f)),(s +* f)) in NIC i,l )assume A1:
f = (IC S),
l --> l,
i
;
IC (Following (ProgramPart (s +* f)),(s +* f)) in NIC i,lreconsider t =
s +* f as
Element of
product the
Object-Kind of
S by PBOOLE:155;
A2:
dom f = {(IC S),l}
by A1, FUNCT_4:65;
then X:
l in dom f
by TARSKI:def 2;
A3:
(ProgramPart t) /. l =
t . l
by AMI_1:150
.=
f . l
by X, FUNCT_4:14
.=
i
by A1, FUNCT_4:66
;
IC S in dom f
by A2, TARSKI:def 2;
then IC t =
f . (IC S)
by FUNCT_4:14
.=
l
by A1, AMI_1:48, FUNCT_4:66
;
hence
IC (Following (ProgramPart (s +* f)),(s +* f)) in NIC i,
l
by A3;
verum
end;
:: deftheorem defines JUMP AMISTD_1:def 6 :
:: deftheorem defines SUCC AMISTD_1:def 7 :
theorem
canceled;
theorem Th14:
theorem Th15:
begin
:: deftheorem Def8 defines <= AMISTD_1:def 8 :
theorem
:: deftheorem defines InsLoc-antisymmetric AMISTD_1:def 9 :
:: deftheorem Def10 defines standard AMISTD_1:def 10 :
theorem Th17:
LemRefle:
for k being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds k <= k,S
theorem Th18:
theorem Th19:
Lm3:
for a, b being set holds dom ((NAT --> a) +* (NAT .--> b)) = NAT \/ {NAT }
set III = {[1,0 ],[0 ,0 ]};
begin
definition
let N be
with_non-empty_elements set ;
func STC N -> strict AMI-Struct of
N means :
Def11:
( the
carrier of
it = NAT \/ {NAT } & the
Instruction-Counter of
it = NAT & the
Instructions of
it = {[0 ,0 ],[1,0 ]} & the
Object-Kind of
it = (NAT --> {[1,0 ],[0 ,0 ]}) +* (NAT .--> NAT ) & ex
f being
Function of
(product the Object-Kind of it),
(product the Object-Kind of it) st
( ( for
s being
Element of
product the
Object-Kind of
it holds
f . s = s +* (NAT .--> (succ (s . NAT ))) ) & the
Execution of
it = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of it))) ) );
existence
ex b1 being strict AMI-Struct of N st
( the carrier of b1 = NAT \/ {NAT } & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0 ,0 ],[1,0 ]} & the Object-Kind of b1 = (NAT --> {[1,0 ],[0 ,0 ]}) +* (NAT .--> NAT ) & ex f being Function of (product the Object-Kind of b1),(product the Object-Kind of b1) st
( ( for s being Element of product the Object-Kind of b1 holds f . s = s +* (NAT .--> (succ (s . NAT ))) ) & the Execution of b1 = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of b1))) ) )
uniqueness
for b1, b2 being strict AMI-Struct of N st the carrier of b1 = NAT \/ {NAT } & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0 ,0 ],[1,0 ]} & the Object-Kind of b1 = (NAT --> {[1,0 ],[0 ,0 ]}) +* (NAT .--> NAT ) & ex f being Function of (product the Object-Kind of b1),(product the Object-Kind of b1) st
( ( for s being Element of product the Object-Kind of b1 holds f . s = s +* (NAT .--> (succ (s . NAT ))) ) & the Execution of b1 = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of b1))) ) & the carrier of b2 = NAT \/ {NAT } & the Instruction-Counter of b2 = NAT & the Instructions of b2 = {[0 ,0 ],[1,0 ]} & the Object-Kind of b2 = (NAT --> {[1,0 ],[0 ,0 ]}) +* (NAT .--> NAT ) & ex f being Function of (product the Object-Kind of b2),(product the Object-Kind of b2) st
( ( for s being Element of product the Object-Kind of b2 holds f . s = s +* (NAT .--> (succ (s . NAT ))) ) & the Execution of b2 = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of b2))) ) holds
b1 = b2
end;
:: deftheorem Def11 defines STC AMISTD_1:def 11 :
Lm4:
for N being non empty with_non-empty_elements set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec i,s) . (IC (STC N)) = succ (IC s)
theorem Th20:
theorem
theorem Th22:
theorem
Lm5:
for z being natural number
for N being non empty with_non-empty_elements set
for l being Element of NAT
for i being Element of the Instructions of (STC N) st l = z & InsCode i = 1 holds
NIC i,l = {(z + 1)}
Lm6:
for N being non empty with_non-empty_elements set
for i being Element of the Instructions of (STC N) holds JUMP i is empty
theorem Th24:
definition
let N be non
empty with_non-empty_elements set ;
let S be non
empty stored-program IC-Ins-separated definite standard AMI-Struct of
N;
let k be
natural number ;
func il. S,
k -> Element of
NAT means :
Def12:
ex
f being
Function of
NAT ,
NAT st
(
f is
bijective & ( for
m,
n being
Element of
NAT holds
(
m <= n iff
f . m <= f . n,
S ) ) &
it = f . k );
existence
ex b1 being Element of NAT ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b1 = f . k )
uniqueness
for b1, b2 being Element of NAT st ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b1 = f . k ) & ex f being Function of NAT ,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b2 = f . k ) holds
b1 = b2
by Th17;
end;
:: deftheorem Def12 defines il. AMISTD_1:def 12 :
theorem Th25:
theorem Th26:
:: deftheorem Def13 defines locnum AMISTD_1:def 13 :
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
:: deftheorem defines + AMISTD_1:def 14 :
theorem
theorem
theorem
:: deftheorem defines NextLoc AMISTD_1:def 15 :
theorem
theorem Th35:
theorem
theorem Th37:
theorem
theorem
theorem
:: deftheorem defines sequential AMISTD_1:def 16 :
theorem Th41:
theorem Th42:
theorem
begin
:: deftheorem Def17 defines closed AMISTD_1:def 17 :
:: deftheorem defines really-closed AMISTD_1:def 18 :
:: deftheorem defines para-closed AMISTD_1:def 19 :
theorem Th44:
theorem Th45:
theorem Th46:
:: deftheorem Def20 defines lower AMISTD_1:def 20 :
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
:: deftheorem Def21 defines LastLoc AMISTD_1:def 21 :
theorem Th51:
theorem
theorem Th53:
theorem
theorem Th55:
Lm7:
now
let N be non
empty with_non-empty_elements set ;
for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of N holds
( ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) holds
l = LastLoc ((il. S,0 ) .--> (halt S)) ) )let S be non
empty stored-program halting IC-Ins-separated definite standard AMI-Struct of
N;
( ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) holds
l = LastLoc ((il. S,0 ) .--> (halt S)) ) )set F =
(il. S,0 ) .--> (halt S);
A1:
dom ((il. S,0 ) .--> (halt S)) = {(il. S,0 )}
by FUNCOP_1:19;
then A2:
card (dom ((il. S,0 ) .--> (halt S))) = 1
by CARD_1:50;
(il. S,0 ) .--> (halt S) is
lower FinPartState of
S
by Th48;
then A3:
LastLoc ((il. S,0 ) .--> (halt S)) =
il. S,
((card ((il. S,0 ) .--> (halt S))) -' 1)
by Th55
.=
il. S,
((card (dom ((il. S,0 ) .--> (halt S)))) -' 1)
by CARD_1:104
.=
il. S,
0
by A2, XREAL_1:234
;
hence
((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S
by FUNCOP_1:87;
for l being Element of NAT st ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) holds
l = LastLoc ((il. S,0 ) .--> (halt S))let l be
Element of
NAT ;
( ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) implies l = LastLoc ((il. S,0 ) .--> (halt S)) )assume
((il. S,0 ) .--> (halt S)) . l = halt S
;
( l in dom ((il. S,0 ) .--> (halt S)) implies l = LastLoc ((il. S,0 ) .--> (halt S)) )assume
l in dom ((il. S,0 ) .--> (halt S))
;
l = LastLoc ((il. S,0 ) .--> (halt S))hence
l = LastLoc ((il. S,0 ) .--> (halt S))
by A1, A3, TARSKI:def 1;
verum
end;
:: deftheorem Def22 defines halt-ending AMISTD_1:def 22 :
:: deftheorem Def23 defines unique-halt AMISTD_1:def 23 :
theorem
theorem
begin
theorem
theorem
:: deftheorem defines -' AMISTD_1:def 24 :
theorem
theorem Th61:
theorem
canceled;
theorem
theorem