Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### A Mathematical Model of CPU

**by****Yatsuka Nakamura, and****Andrzej Trybulec**- Received October 14, 1992
- MML identifier: AMI_1

- [ Mizar article, MML identifier index ]

environ vocabulary INT_1, BOOLE, FUNCT_2, FUNCT_1, RELAT_1, FUNCOP_1, CAT_1, FUNCT_4, CARD_3, TARSKI, FRAENKEL, FUNCT_3, PARTFUN1, FINSET_1, AMI_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, CARD_3, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, NAT_1, CQC_LANG, FRAENKEL, FUNCOP_1, FUNCT_4, FINSEQ_1, FUNCT_3, PARTFUN1, STRUCT_0; constructors CARD_3, NAT_1, CQC_LANG, CAT_2, INT_2, PARTFUN1, STRUCT_0, MEMBERED, XBOOLE_0; clusters SUBSET_1, FUNCT_1, INT_1, FRAENKEL, RELAT_1, FINSET_1, RELSET_1, FINSEQ_1, FUNCOP_1, FUNCT_4, CQC_LANG, STRUCT_0, XBOOLE_0, FUNCT_2, MEMBERED, ZFMISC_1, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve x for set; theorem :: AMI_1:1 NAT <> INT; theorem :: AMI_1:2 for a,b being set holds 1 <> [a,b]; theorem :: AMI_1:3 for a,b being set holds 2 <> [a,b]; canceled; theorem :: AMI_1:5 for a,b,c,d being set st a <> b holds product (a,b) --> ({c},{d}) = { (a,b) --> (c,d) }; definition let IT be set; attr IT is with_non-empty_elements means :: AMI_1:def 1 not {} in IT; end; definition cluster non empty with_non-empty_elements set; end; definition let A be non empty set; cluster { A } -> with_non-empty_elements; let B be non empty set; cluster { A, B } -> with_non-empty_elements; end; definition let A,B be with_non-empty_elements set; cluster A \/ B -> with_non-empty_elements; end; begin :: General concepts reserve N for with_non-empty_elements set; definition let N be set; struct (1-sorted) AMI-Struct over N (# carrier -> set, Instruction-Counter -> Element of the carrier, Instruction-Locations -> Subset of the carrier, Instruction-Codes -> non empty set, Instructions -> non empty Subset of [: the Instruction-Codes, ((union N) \/ the carrier)* :], Object-Kind -> Function of the carrier, N \/ { the Instructions, the Instruction-Locations }, Execution -> Function of the Instructions, Funcs(product the Object-Kind, product the Object-Kind) #); end; definition let N be set; func Trivial-AMI N -> strict AMI-Struct over N means :: AMI_1:def 2 the carrier of it = {0,1} & the Instruction-Counter of it = 0 & the Instruction-Locations of it = {1} & the Instruction-Codes of it = {0} & the Instructions of it = {[0,{}]} & the Object-Kind of it = (0,1) --> ({1},{[0,{}]}) & the Execution of it = {[0,{}]} --> id product (0,1) --> ({1},{[0,{}]}); end; definition let N be set; let S be AMI-Struct over N; attr S is void means :: AMI_1:def 3 the Instruction-Locations of S is empty; end; definition let N be set; cluster Trivial-AMI N -> non empty non void; end; definition let N be set; cluster non empty non void AMI-Struct over N; end; definition let N be set; let S be non empty AMI-Struct over N; cluster the carrier of S -> non empty; end; definition let N be set; let S be non void AMI-Struct over N; cluster the Instruction-Locations of S -> non empty; end; definition let N be set; let S be non empty AMI-Struct over N; mode Object of S is Element of S; end; definition let N be set; let S be non empty non void AMI-Struct over N; mode Instruction-Location of S is Element of the Instruction-Locations of S; end; definition let N be set; let S be AMI-Struct over N; mode Instruction of S is Element of the Instructions of S; canceled; end; definition let N be set; let S be non empty AMI-Struct over N; func IC S -> Object of S equals :: AMI_1:def 5 the Instruction-Counter of S; end; definition let N be set; let S be non empty AMI-Struct over N; let o be Object of S; func ObjectKind o -> Element of N \/ { the Instructions of S, the Instruction-Locations of S } equals :: AMI_1:def 6 (the Object-Kind of S).o; end; definition let f be Function; cluster product f -> functional; end; definition let A be set; let B be with_non-empty_elements set; let f be Function of A,B; cluster product f -> non empty; end; definition let N be set; let S be AMI-Struct over N; mode State of S is Element of product the Object-Kind of S; end; definition let N be with_non-empty_elements set; let S be non void AMI-Struct over N; let I be Instruction of S, s be State of S; func Exec(I,s) -> State of S equals :: AMI_1:def 7 ((the Execution of S).I).s; end; definition let N; let S be non void AMI-Struct over N; let I be Instruction of S; attr I is halting means :: AMI_1:def 8 for s being State of S holds Exec(I,s) = s; end; definition let N; let S be non void AMI-Struct over N; attr S is halting means :: AMI_1:def 9 ex I being Instruction of S st I is halting & for J being Instruction of S st J is halting holds I = J; end; reserve E for set; theorem :: AMI_1:6 Trivial-AMI N is halting; definition let N; cluster Trivial-AMI N -> halting; end; definition let N; cluster halting (non void AMI-Struct over N); end; definition let N; let S be halting (non void AMI-Struct over N); func halt S -> Instruction of S means :: AMI_1:def 10 ex I being Instruction of S st I is halting & it = I; end; definition let N; let S be halting (non void AMI-Struct over N); cluster halt S -> halting; end; definition let N be set; let IT be non empty AMI-Struct over N; attr IT is IC-Ins-separated means :: AMI_1:def 11 ObjectKind IC IT = the Instruction-Locations of IT; end; definition let N be set; let IT be AMI-Struct over N; attr IT is data-oriented means :: AMI_1:def 12 (the Object-Kind of IT)"{ the Instructions of IT } c= the Instruction-Locations of IT; end; definition let N be with_non-empty_elements set; let IT be non empty non void AMI-Struct over N; attr IT is steady-programmed means :: AMI_1:def 13 for s being State of IT, i being Instruction of IT, l being Instruction-Location of IT holds Exec(i,s).l = s.l; end; definition let N be set; let IT be non empty non void AMI-Struct over N; attr IT is definite means :: AMI_1:def 14 for l being Instruction-Location of IT holds ObjectKind l = the Instructions of IT; end; theorem :: AMI_1:7 Trivial-AMI E is IC-Ins-separated; theorem :: AMI_1:8 Trivial-AMI E is data-oriented; theorem :: AMI_1:9 for s1, s2 being State of Trivial-AMI E holds s1=s2; theorem :: AMI_1:10 Trivial-AMI N is steady-programmed; theorem :: AMI_1:11 Trivial-AMI E is definite; definition let E be set; cluster Trivial-AMI E -> data-oriented; end; definition let E be set; cluster Trivial-AMI E -> IC-Ins-separated definite; end; definition let N be with_non-empty_elements set; cluster Trivial-AMI N -> steady-programmed; end; definition let E be set; cluster data-oriented strict AMI-Struct over E; end; definition let M be set; cluster IC-Ins-separated data-oriented definite strict (non empty non void AMI-Struct over M); end; definition let N; cluster IC-Ins-separated data-oriented halting steady-programmed definite strict (non empty non void AMI-Struct over N); end; definition let N be with_non-empty_elements set; let S be IC-Ins-separated (non empty non void AMI-Struct over N); let s be State of S; func IC s -> Instruction-Location of S equals :: AMI_1:def 15 s.IC S; end; begin :: Preliminaries reserve x,y,z,A,B for set, f,g,h for Function, i,j,k for Nat; canceled; theorem :: AMI_1:13 for f being Function holds pr1(dom f,rng f).:f = dom f; theorem :: AMI_1:14 f tolerates g & [x,y] in f & [x,z] in g implies y = z; theorem :: AMI_1:15 (for x st x in A holds x is Function) & (for f,g being Function st f in A & g in A holds f tolerates g) implies union A is Function; theorem :: AMI_1:16 dom f c= A \/ B implies f|A +* f|B = f; canceled; theorem :: AMI_1:18 for x1,x2,y1,y2 being set holds (x1,x2)-->(y1,y2) = (x1 .--> y1) +* (x2 .--> y2); theorem :: AMI_1:19 for x,y holds x .--> y = {[x,y]}; theorem :: AMI_1:20 for a,b,c being set holds (a,a) --> (b,c) = a .--> c; theorem :: AMI_1:21 for f being Function holds dom f is finite iff f is finite; theorem :: AMI_1:22 x in product f implies x is Function; begin :: Superproducts definition let f be Function; func sproduct f -> set means :: AMI_1:def 16 x in it iff ex g st x = g & dom g c= dom f & for x st x in dom g holds g.x in f.x; end; definition let f be Function; cluster sproduct f -> functional non empty; end; canceled 2; theorem :: AMI_1:25 g in sproduct f implies dom g c= dom f & for x st x in dom g holds g.x in f.x; theorem :: AMI_1:26 {} in sproduct f; theorem :: AMI_1:27 product f c= sproduct f; theorem :: AMI_1:28 x in sproduct f implies x is PartFunc of dom f, union rng f; theorem :: AMI_1:29 g in product f & h in sproduct f implies g +* h in product f; theorem :: AMI_1:30 product f <> {} implies (g in sproduct f iff ex h st h in product f & g <= h); theorem :: AMI_1:31 sproduct f c= PFuncs(dom f,union rng f); theorem :: AMI_1:32 f c= g implies sproduct f c= sproduct g; theorem :: AMI_1:33 sproduct {} = {{}}; theorem :: AMI_1:34 PFuncs(A,B) = sproduct (A --> B); theorem :: AMI_1:35 for A, B being non empty set for f being Function of A,B holds sproduct f = sproduct(f|{x where x is Element of A: f.x <> {} }); theorem :: AMI_1:36 x in dom f & y in f.x implies x .--> y in sproduct f; theorem :: AMI_1:37 sproduct f = {{}} iff for x st x in dom f holds f.x = {}; theorem :: AMI_1:38 A c= sproduct f & (for h1,h2 being Function st h1 in A & h2 in A holds h1 tolerates h2) implies union A in sproduct f; theorem :: AMI_1:39 g tolerates h & g in sproduct f & h in sproduct f implies g \/ h in sproduct f; theorem :: AMI_1:40 g c= h & h in sproduct f implies g in sproduct f; theorem :: AMI_1:41 g in sproduct f implies g|A in sproduct f; theorem :: AMI_1:42 g in sproduct f implies g|A in sproduct f|A; theorem :: AMI_1:43 h in sproduct(f+*g) implies ex f',g' being Function st f' in sproduct f & g' in sproduct g & h = f'+*g'; theorem :: AMI_1:44 for f',g' being Function st dom g misses dom f' \ dom g' & f' in sproduct f & g' in sproduct g holds f'+*g' in sproduct(f+*g); theorem :: AMI_1:45 for f',g' being Function st dom f' misses dom g \ dom g' & f' in sproduct f & g' in sproduct g holds f'+*g' in sproduct(f+*g); theorem :: AMI_1:46 g in sproduct f & h in sproduct f implies g +* h in sproduct f; theorem :: AMI_1:47 for x1,x2,y1,y2 being set holds x1 in dom f & y1 in f.x1 & x2 in dom f & y2 in f.x2 implies (x1,x2)-->(y1,y2) in sproduct f; begin :: General theory definition let N; let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let s be State of S; func CurInstr s -> Instruction of S equals :: AMI_1:def 17 s.IC s; end; definition let N; let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let s be State of S; func Following s -> State of S equals :: AMI_1:def 18 Exec(CurInstr s,s); end; definition let N; let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let s be State of S; func Computation s -> Function of NAT, product the Object-Kind of S means :: AMI_1:def 19 it.0 = s & for i holds it.(i+1) = Following(it.i); end; definition let N; let S be non void AMI-Struct over N; let f be Function of NAT, product the Object-Kind of S; let k; redefine func f.k -> State of S; end; definition let N; let S be halting IC-Ins-separated definite (non empty non void AMI-Struct over N); let IT be State of S; attr IT is halting means :: AMI_1:def 20 ex k st CurInstr((Computation IT).k) = halt S; end; definition let N be set; let IT be AMI-Struct over N; attr IT is realistic means :: AMI_1:def 21 the Instructions of IT <> the Instruction-Locations of IT; end; theorem :: AMI_1:48 for S being IC-Ins-separated definite (non empty non void AMI-Struct over E) st S is realistic holds not ex l being Instruction-Location of S st IC S = l; reserve S for IC-Ins-separated definite (non empty non void AMI-Struct over N), s for State of S; canceled 2; theorem :: AMI_1:51 for k holds (Computation s).(i+k) = (Computation (Computation s).i).k; theorem :: AMI_1:52 i <= j implies for N for S being halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for s being State of S st CurInstr((Computation s).i) = halt S holds (Computation s).j = (Computation s).i; definition let N; let S be halting IC-Ins-separated definite (non empty non void AMI-Struct over N); let s be State of S such that s is halting; func Result s -> State of S means :: AMI_1:def 22 ex k st it = (Computation s).k & CurInstr(it) = halt S; end; theorem :: AMI_1:53 for S being steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N) for s being State of S, i be Instruction-Location of S holds s.i = (Following s).i; definition let N; let S be definite (non empty non void AMI-Struct over N); let s be State of S, l be Instruction-Location of S; redefine func s.l -> Instruction of S; end; theorem :: AMI_1:54 for S being steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N) for s being State of S, i be Instruction-Location of S, k holds s.i = (Computation s).k.i; theorem :: AMI_1:55 for S being steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N) for s being State of S holds (Computation s).(k+1) = Exec(s.(IC (Computation s).k),(Computation s).k); theorem :: AMI_1:56 for S being steady-programmed IC-Ins-separated halting definite (non empty non void AMI-Struct over N) for s being State of S, k st s.IC (Computation s).k = halt S holds Result s = (Computation s).k; theorem :: AMI_1:57 for S being steady-programmed IC-Ins-separated halting definite (non empty non void AMI-Struct over N) for s being State of S st ex k st s.IC (Computation s).k = halt S for i holds Result s = Result (Computation s).i; definition let N; let S be non empty non void AMI-Struct over N, o be Object of S; cluster ObjectKind o -> non empty; end; begin :: Finite substates definition let N be set; let S be AMI-Struct over N; func FinPartSt S -> Subset of sproduct the Object-Kind of S equals :: AMI_1:def 23 { p where p is Element of sproduct the Object-Kind of S: p is finite }; end; definition let N be set; let S be AMI-Struct over N; mode FinPartState of S -> Element of sproduct the Object-Kind of S means :: AMI_1:def 24 it is finite; end; definition let N; let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let IT be FinPartState of S; attr IT is autonomic means :: AMI_1:def 25 for s1,s2 being State of S st IT c= s1 & IT c= s2 for i holds (Computation s1).i|dom IT = (Computation s2).i|dom IT; end; definition let N; let S be halting IC-Ins-separated definite (non empty non void AMI-Struct over N); let IT be FinPartState of S; attr IT is halting means :: AMI_1:def 26 for s being State of S st IT c= s holds s is halting; end; definition let N; let IT be IC-Ins-separated definite (non empty non void AMI-Struct over N); attr IT is programmable means :: AMI_1:def 27 ex s being FinPartState of IT st s is non empty autonomic; end; theorem :: AMI_1:58 for S being IC-Ins-separated definite (non empty non void AMI-Struct over N) for A,B being set, la,lb being Object of S st ObjectKind la = A & ObjectKind lb = B for a being Element of A, b being Element of B holds (la,lb) --> (a,b) is FinPartState of S; theorem :: AMI_1:59 for S being IC-Ins-separated definite (non empty non void AMI-Struct over N) for A being set, la being Object of S st ObjectKind la = A for a being Element of A holds la .--> a is FinPartState of S; definition let N; let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let la be Object of S; let a be Element of ObjectKind la; redefine func la .--> a -> FinPartState of S; end; definition let N; let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let la,lb be Object of S; let a be Element of ObjectKind la, b be Element of ObjectKind lb; redefine func (la,lb) --> (a,b) -> FinPartState of S; end; theorem :: AMI_1:60 Trivial-AMI E is realistic; theorem :: AMI_1:61 Trivial-AMI N is programmable; definition let E; cluster Trivial-AMI E -> realistic; end; definition let N; cluster Trivial-AMI N -> programmable; end; definition let E; cluster data-oriented realistic strict AMI-Struct over E; end; definition let M be set; cluster data-oriented realistic strict IC-Ins-separated definite (non empty non void AMI-Struct over M); end; definition let N; cluster data-oriented halting steady-programmed realistic programmable strict (IC-Ins-separated definite (non empty non void AMI-Struct over N)); end; theorem :: AMI_1:62 for S being non void AMI-Struct over N, s being State of S, p being FinPartState of S holds s|dom p is FinPartState of S; theorem :: AMI_1:63 for N being set for S being AMI-Struct over N holds {} is FinPartState of S; definition let N; let S be programmable (IC-Ins-separated definite (non empty non void AMI-Struct over N)); cluster non empty autonomic FinPartState of S; end; definition let N be set; let S be AMI-Struct over N; let f,g be FinPartState of S; redefine func f +* g -> FinPartState of S; end; begin :: Preprograms theorem :: AMI_1:64 for S being halting realistic IC-Ins-separated definite (non empty non void AMI-Struct over N) for loc being Instruction-Location of S for l being Element of ObjectKind IC S st l = loc for h being Element of ObjectKind loc st h = halt S for s being State of S st (IC S,loc) --> (l, h) c= s holds CurInstr s = halt S; theorem :: AMI_1:65 for S being halting realistic IC-Ins-separated definite (non empty non void AMI-Struct over N) for loc being Instruction-Location of S for l being Element of ObjectKind IC S st l = loc for h being Element of ObjectKind loc st h = halt S holds (IC S,loc) --> (l, h) is halting; theorem :: AMI_1:66 for S being realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for loc being Instruction-Location of S for l being Element of ObjectKind IC S st l = loc for h being Element of ObjectKind loc st h = halt S for s being State of S st (IC S,loc) --> (l, h) c= s for i holds (Computation s).i = s; theorem :: AMI_1:67 for S be realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for loc being Instruction-Location of S for l being Element of ObjectKind IC S st l = loc for h being Element of ObjectKind loc st h = halt S holds (IC S,loc) --> (l, h) is autonomic; definition let N; let S be realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N); cluster autonomic halting FinPartState of S; end; definition let N; let S be realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N); mode pre-program of S is autonomic halting FinPartState of S; end; definition let N; let S be realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N); let s be FinPartState of S; assume s is pre-program of S; func Result(s) -> FinPartState of S means :: AMI_1:def 28 for s' being State of S st s c= s' holds it = (Result s')|dom s; end; begin :: Computability definition let N; let S be realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N); let p be FinPartState of S, F be Function; pred p computes F means :: AMI_1:def 29 for x being set st x in dom F ex s being FinPartState of S st x = s & p +* s is pre-program of S & F.s c= Result(p +* s); antonym p does_not_compute F; end; theorem :: AMI_1:68 for S being realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for p being FinPartState of S holds p computes {}; theorem :: AMI_1:69 for S being realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for p being FinPartState of S holds p is pre-program of S iff p computes {} .--> Result(p); theorem :: AMI_1:70 for S being realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for p being FinPartState of S holds p is pre-program of S iff p computes {} .--> {}; definition let N; let S be realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N); let IT be PartFunc of FinPartSt S, FinPartSt S; attr IT is computable means :: AMI_1:def 30 ex p being FinPartState of S st p computes IT; end; theorem :: AMI_1:71 for S being realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for F being PartFunc of FinPartSt S, FinPartSt S st F = {} holds F is computable; theorem :: AMI_1:72 for S being realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> {} holds F is computable; theorem :: AMI_1:73 for S being realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for p being pre-program of S for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> Result(p) holds F is computable; definition let N; let S be realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N); let F be PartFunc of FinPartSt S, FinPartSt S such that F is computable; mode Program of F -> FinPartState of S means :: AMI_1:def 31 it computes F; end; definition let N be set, S be AMI-Struct over N; mode InsType of S is Element of the Instruction-Codes of S; canceled; end; theorem :: AMI_1:74 for S being realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for F being PartFunc of FinPartSt S, FinPartSt S st F = {} for p being FinPartState of S holds p is Program of F; theorem :: AMI_1:75 for S being realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> {} for p being pre-program of S holds p is Program of F; theorem :: AMI_1:76 for S being realistic halting IC-Ins-separated definite (non empty non void AMI-Struct over N) for p being pre-program of S for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> Result p holds p is Program of F;

Back to top