:: Standard Ordering of Instruction Locations
:: by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem :: AMISTD_1:1
canceled;
theorem :: AMISTD_1:2
canceled;
theorem :: AMISTD_1:3
canceled;
theorem :: AMISTD_1:4
canceled;
theorem :: AMISTD_1:5
canceled;
theorem :: AMISTD_1:6
canceled;
theorem :: AMISTD_1:7
canceled;
theorem :: AMISTD_1:8
canceled;
theorem :: AMISTD_1:9
canceled;
theorem :: AMISTD_1:10
canceled;
theorem Th11: :: AMISTD_1:11
Lm1:
for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for il being Instruction-Location of S
for I being Element of the Instructions of S
for f being FinPartState of S st f = il .--> I holds
f is autonomic
theorem :: AMISTD_1:12
theorem Th13: :: AMISTD_1:13
:: deftheorem Def1 defines IL-Subset AMISTD_1:def 1 :
:: 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 IL be non
empty set ;
:: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for i being Element of the Instructions of S
for l being Instruction-Location of S
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,llet N be
with_non-empty_elements set ;
:: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for i being Element of the Instructions of S
for l being Instruction-Location of S
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,llet S be non
empty stored-program IC-Ins-separated definite realistic AMI-Struct of
IL,
N;
:: thesis: for i being Element of the Instructions of S
for l being Instruction-Location of S
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,llet i be
Element of the
Instructions of
S;
:: thesis: for l being Instruction-Location of S
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,llet l be
Instruction-Location of
S;
:: thesis: for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,llet s be
State of
S;
:: thesis: for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,llet f be
FinPartState of
S;
:: thesis: ( f = (IC S),l --> l,i implies IC (Following (s +* f)) in NIC i,l )assume A1:
f = (IC S),
l --> l,
i
;
:: thesis: IC (Following (s +* f)) in NIC i,lset t =
s +* f;
A3:
dom f = {(IC S),l}
by A1, FUNCT_4:65;
then
IC S in dom f
by TARSKI:def 2;
then A4:
IC (s +* f) =
f . (IC S)
by FUNCT_4:14
.=
l
by A1, AMI_1:48, FUNCT_4:66
;
l in dom f
by A3, TARSKI:def 2;
then (s +* f) . l =
f . l
by FUNCT_4:14
.=
i
by A1, FUNCT_4:66
;
hence
IC (Following (s +* f)) in NIC i,
l
by A4;
:: thesis: verum
end;
:: deftheorem defines JUMP AMISTD_1:def 6 :
:: deftheorem defines SUCC AMISTD_1:def 7 :
theorem Th14: :: AMISTD_1:14
theorem Th15: :: AMISTD_1:15
:: deftheorem Def8 defines <= AMISTD_1:def 8 :
theorem :: AMISTD_1:16
:: deftheorem defines InsLoc-antisymmetric AMISTD_1:def 9 :
:: deftheorem Def10 defines standard AMISTD_1:def 10 :
theorem Th17: :: AMISTD_1:17
theorem Th18: :: AMISTD_1:18
theorem Th19: :: AMISTD_1:19
Lm3:
for a, b being set holds dom ((NAT --> a) +* (NAT .--> b)) = NAT \/ {NAT }
set III = {[1,0 ],[0 ,0 ]};
definition
let N be
with_non-empty_elements set ;
func STC N -> strict AMI-Struct of
NAT ,
N means :
Def11:
:: AMISTD_1:def 11
( 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 NAT ,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 NAT ,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 :
for
N being
with_non-empty_elements set for
b2 being
strict AMI-Struct of
NAT ,
N holds
(
b2 = STC N iff ( 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))) ) ) );
Lm4:
for N being 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: :: AMISTD_1:20
theorem :: AMISTD_1:21
theorem Th22: :: AMISTD_1:22
theorem :: AMISTD_1:23
Lm5:
for z being natural number
for N being with_non-empty_elements set
for l being Instruction-Location of STC N
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 with_non-empty_elements set
for i being Element of the Instructions of (STC N) holds JUMP i is empty
theorem Th24: :: AMISTD_1:24
definition
let N be
with_non-empty_elements set ;
let S be non
empty stored-program IC-Ins-separated definite standard AMI-Struct of
NAT ,
N;
let k be
natural number ;
func il. S,
k -> Instruction-Location of
S means :
Def12:
:: AMISTD_1:def 12
ex
f being
IL-Function of
NAT ,
S st
(
f is
bijective & ( for
m,
n being
Element of
NAT holds
(
m <= n iff
f . m <= f . n ) ) &
it = f . k );
existence
ex b1 being Instruction-Location of S ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & b1 = f . k )
uniqueness
for b1, b2 being Instruction-Location of S st ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & b1 = f . k ) & ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & b2 = f . k ) holds
b1 = b2
by Th17;
end;
:: deftheorem Def12 defines il. AMISTD_1:def 12 :
theorem Th25: :: AMISTD_1:25
theorem Th26: :: AMISTD_1:26
:: deftheorem Def13 defines locnum AMISTD_1:def 13 :
theorem Th27: :: AMISTD_1:27
theorem Th28: :: AMISTD_1:28
theorem Th29: :: AMISTD_1:29
theorem Th30: :: AMISTD_1:30
:: deftheorem defines + AMISTD_1:def 14 :
theorem :: AMISTD_1:31
theorem :: AMISTD_1:32
theorem :: AMISTD_1:33
:: deftheorem defines NextLoc AMISTD_1:def 15 :
theorem :: AMISTD_1:34
theorem Th35: :: AMISTD_1:35
theorem :: AMISTD_1:36
theorem Th37: :: AMISTD_1:37
theorem :: AMISTD_1:38
theorem :: AMISTD_1:39
theorem :: AMISTD_1:40
:: deftheorem defines sequential AMISTD_1:def 16 :
theorem Th41: :: AMISTD_1:41
theorem Th42: :: AMISTD_1:42
theorem :: AMISTD_1:43
:: 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: :: AMISTD_1:44
theorem Th45: :: AMISTD_1:45
theorem Th46: :: AMISTD_1:46
:: deftheorem Def20 defines lower AMISTD_1:def 20 :
theorem Th47: :: AMISTD_1:47
theorem Th48: :: AMISTD_1:48
theorem Th49: :: AMISTD_1:49
theorem Th50: :: AMISTD_1:50
:: deftheorem Def21 defines LastLoc AMISTD_1:def 21 :
theorem Th51: :: AMISTD_1:51
theorem :: AMISTD_1:52
theorem Th53: :: AMISTD_1:53
theorem :: AMISTD_1:54
theorem Th55: :: AMISTD_1:55
Lm7:
now
let IL be non
empty set ;
:: thesis: for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N holds
( ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S & ( for l being Instruction-Location of S 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 N be
with_non-empty_elements set ;
:: thesis: for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N holds
( ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S & ( for l being Instruction-Location of S 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
NAT ,
N;
:: thesis: ( ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S & ( for l being Instruction-Location of S 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 PRE_CIRC:21
.=
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;
:: thesis: for l being Instruction-Location of S 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
Instruction-Location of
S;
:: thesis: ( ((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
;
:: thesis: ( 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))
;
:: thesis: l = LastLoc ((il. S,0 ) .--> (halt S))hence
l = LastLoc ((il. S,0 ) .--> (halt S))
by A1, A3, TARSKI:def 1;
:: thesis: verum
end;
:: deftheorem defines halt-ending AMISTD_1:def 22 :
:: deftheorem defines unique-halt AMISTD_1:def 23 :
theorem :: AMISTD_1:56
theorem :: AMISTD_1:57
theorem :: AMISTD_1:58
theorem :: AMISTD_1:59
:: deftheorem defines -' AMISTD_1:def 24 :
theorem :: AMISTD_1:60
theorem Th5: :: AMISTD_1:61
theorem :: AMISTD_1:62
canceled;
theorem :: AMISTD_1:63
theorem :: AMISTD_1:64