begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem AMISTD_1:def 1 :
canceled;
:: deftheorem AMISTD_1:def 2 :
canceled;
:: deftheorem defines jump-only AMISTD_1:def 3 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program standard-ins AMI-Struct of N
for T being InsType of S holds
( T is jump-only iff for s being State of S
for o being Object of S
for I being Instruction of S st InsCode I = T & o in Data-Locations S holds
(Exec (I,s)) . o = s . o );
:: deftheorem defines jump-only AMISTD_1:def 4 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program standard-ins AMI-Struct of N
for I being Instruction of S holds
( I is jump-only iff InsCode I is jump-only );
:: deftheorem defines NIC AMISTD_1:def 5 :
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
for l being Nat
for i being Element of the Instructions of S holds NIC (i,l) = { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = l } ;
Lm2:
now
let N be non
empty with_non-empty_elements set ;
for S being non empty stored-program IC-Ins-separated 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,l)let S be non
empty stored-program IC-Ins-separated 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,l)let 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,l)let 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,l)let 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,l)let 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,l)reconsider 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 COMPOS_1:38
.=
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, COMPOS_1:3, 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 :
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
for i being Element of the Instructions of S holds JUMP i = meet { (NIC (i,l)) where l is Element of NAT : verum } ;
:: deftheorem defines SUCC AMISTD_1:def 7 :
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
for l being Nat holds SUCC (l,S) = union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the Instructions of S : verum } ;
theorem
canceled;
theorem Th14:
theorem Th15:
begin
:: deftheorem AMISTD_1:def 8 :
canceled;
:: deftheorem AMISTD_1:def 9 :
canceled;
:: deftheorem Def10 defines standard AMISTD_1:def 10 :
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
( S is standard iff for m, n being Element of NAT holds
( m <= n iff ex f being non empty FinSequence of NAT st
( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) ) );
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 ex f being non empty FinSequence of NAT st
( f /. 1 = k & f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th19:
Lm3:
for a, b being set holds dom ((NAT --> a) +* (NAT .--> b)) = NAT \/ {NAT}
set III = {[1,0,0],[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,0],[1,0,0]} & the
haltF of
it = [0,0,0] & the
Object-Kind of
it = (NAT --> {[1,0,0],[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,0] .--> f) +* ([0,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,0],[1,0,0]} & the haltF of b1 = [0,0,0] & the Object-Kind of b1 = (NAT --> {[1,0,0],[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,0] .--> f) +* ([0,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,0],[1,0,0]} & the haltF of b1 = [0,0,0] & the Object-Kind of b1 = (NAT --> {[1,0,0],[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,0] .--> f) +* ([0,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,0],[1,0,0]} & the haltF of b2 = [0,0,0] & the Object-Kind of b2 = (NAT --> {[1,0,0],[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,0] .--> f) +* ([0,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 N holds
( b2 = STC N iff ( the carrier of b2 = NAT \/ {NAT} & the Instruction-Counter of b2 = NAT & the Instructions of b2 = {[0,0,0],[1,0,0]} & the haltF of b2 = [0,0,0] & the Object-Kind of b2 = (NAT --> {[1,0,0],[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,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of b2))) ) ) );
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:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
:: deftheorem AMISTD_1:def 12 :
canceled;
:: deftheorem AMISTD_1:def 13 :
canceled;
:: deftheorem AMISTD_1:def 14 :
canceled;
:: deftheorem AMISTD_1:def 15 :
canceled;
:: deftheorem defines sequential AMISTD_1:def 16 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for i being Instruction of S holds
( i is sequential iff for s being State of S holds (Exec (i,s)) . (IC S) = succ (IC s) );
theorem Th41:
theorem
canceled;
theorem
begin
:: deftheorem Def17 defines closed AMISTD_1:def 17 :
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
for F being NAT -defined the Instructions of b2 -valued FinPartState of holds
( F is closed iff for l being Element of NAT st l in dom F holds
NIC ((F /. l),l) c= dom F );
:: deftheorem defines really-closed AMISTD_1:def 18 :
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
for F being NAT -defined the Instructions of b2 -valued FinPartState of holds
( F is really-closed iff for s being State of S st IC s in dom F holds
for k being Element of NAT holds IC (Comput (F,s,k)) in dom F );
:: deftheorem defines para-closed AMISTD_1:def 19 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued Function holds
( F is para-closed iff for s being State of S st IC s = 0 holds
for k being Element of NAT holds IC (Comput (F,s,k)) in dom F );
theorem Th44:
theorem Th45:
theorem Th46:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
begin
theorem