Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### Standard Ordering of Instruction Locations

**by****Andrzej Trybulec,****Piotr Rudnicki, and****Artur Kornilowicz**- Received April 14, 2000
- MML identifier: AMISTD_1

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_3, ORDINAL2, ARYTM, SQUARE_1, FINSET_1, REALSET1, FINSEQ_1, RELAT_1, AMI_1, BOOLE, FUNCT_1, SGRAPH1, FUNCOP_1, CAT_1, GRAPH_2, FINSEQ_4, FUNCT_4, CARD_3, AMI_5, SETFAM_1, TARSKI, GOBOARD5, ARYTM_1, ORDINAL1, FUNCT_2, MCART_1, FRECHET, PRE_TOPC, WAYBEL_0, CARD_1, AMISTD_1, MEMBERED; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, ORDINAL2, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, MEMBERED, REALSET1, FUNCT_1, PARTFUN1, FUNCT_2, DOMAIN_1, CARD_1, CARD_3, FINSEQ_1, FINSEQ_4, CQC_LANG, GRAPH_2, FINSET_1, FUNCT_4, STRUCT_0, AMI_1, AMI_3, AMI_5, ORDINAL1, BINARITH, PRE_CIRC; constructors FINSEQ_4, GRAPH_2, REALSET1, DOMAIN_1, FINSEQ_6, AMI_5, BINARITH, PRE_CIRC, WELLORD2, SEQ_2, PARTFUN1, RELAT_2; clusters AMI_1, RELSET_1, INT_1, FINSEQ_5, FUNCT_7, SUBSET_1, RELAT_1, FINSEQ_6, FINSEQ_1, NAT_1, TEX_2, SCMFSA_4, PRELAMB, GROUP_2, YELLOW13, FUNCT_1, SCMRING1, REALSET1, XBOOLE_0, FUNCT_2, FRAENKEL, MEMBERED, PRE_CIRC, ZFMISC_1, PARTFUN1, ORDINAL2; requirements NUMERALS, BOOLE, REAL, SUBSET, ARITHM; begin :: Preliminaries reserve x, X for set, D for non empty set, k, n for Nat, z for natural number; theorem :: AMISTD_1:1 for r being real number holds max {r} = r; theorem :: AMISTD_1:2 max {n} = n; definition cluster non trivial FinSequence; end; theorem :: AMISTD_1:3 for f being trivial FinSequence of D holds f is empty or ex x being Element of D st f = <*x*>; definition cluster -> with_non-empty_elements Relation; end; theorem :: AMISTD_1:4 id X is bijective; definition let A be finite set, B be set; cluster A --> B -> finite; end; definition let x, y be set; cluster x .--> y -> trivial; end; begin :: Restricted concatenation definition let f1 be non empty FinSequence, f2 be FinSequence; cluster f1^'f2 -> non empty; end; theorem :: AMISTD_1:5 for f1 being non empty FinSequence of D, f2 being FinSequence of D holds (f1^'f2)/.1 = f1/.1; theorem :: AMISTD_1:6 for f1 being FinSequence of D, f2 being non trivial FinSequence of D holds (f1^'f2)/.len(f1^'f2) = f2/.len f2; theorem :: AMISTD_1:7 for f being FinSequence holds f^'{} = f; theorem :: AMISTD_1:8 for f being FinSequence holds f^'<*x*> = f; theorem :: AMISTD_1:9 :: GRAPH_2:14 for f1, f2 being FinSequence of D holds 1<=n & n<=len f1 implies (f1^'f2)/.n = f1/.n; theorem :: AMISTD_1:10 :: GRAPH_2:15 for f1, f2 being FinSequence of D holds 1<=n & n<len f2 implies (f1^'f2)/.(len f1 + n) = f2/.(n+1); begin :: Ami-Struct reserve N for with_non-empty_elements set, S for IC-Ins-separated definite (non empty non void AMI-Struct over N), i for Element of the Instructions of S, l, l1, l2, l3 for Instruction-Location of S, s for State of S; theorem :: AMISTD_1:11 for S being definite (non empty non void AMI-Struct over N), I being Element of the Instructions of S, s being State of S holds s +* ((the Instruction-Locations of S) --> I) is State of S; definition let N be set, S be AMI-Struct over N; cluster empty -> programmed FinPartState of S; end; definition let N be set, S be AMI-Struct over N; cluster empty FinPartState of S; end; definition let N be with_non-empty_elements set, S be IC-Ins-separated definite (non empty non void AMI-Struct over N); cluster non empty trivial programmed FinPartState of S; end; definition let N be with_non-empty_elements set, S be non void AMI-Struct over N, i be Element of the Instructions of S, s be State of S; cluster ((the Execution of S).i).s -> Function-like Relation-like; end; definition let N be with_non-empty_elements set; let S be steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N); cluster non empty trivial autonomic programmed FinPartState of S; end; theorem :: AMISTD_1:12 for S being steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N), il being Instruction-Location of S, I being Element of the Instructions of S holds il .--> I is autonomic; theorem :: AMISTD_1:13 for S being steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N) holds S is programmable; definition let N be with_non-empty_elements set; cluster steady-programmed -> programmable (IC-Ins-separated definite (non empty non void AMI-Struct over N)); end; definition let N be with_non-empty_elements set; let S be non empty non void AMI-Struct over N; let T be InsType of S; canceled 2; attr T is jump-only means :: AMISTD_1:def 3 for s being State of S, o being Object of S, I being Instruction of S st InsCode I = T & o <> IC S holds Exec(I, s).o = s.o; end; definition let N be with_non-empty_elements set; let S be non empty non void AMI-Struct over N; let I be Instruction of S; attr I is jump-only means :: AMISTD_1:def 4 InsCode I is jump-only; end; definition let N,S,l; let i be Element of the Instructions of S; func NIC(i,l) -> Subset of the Instruction-Locations of S equals :: AMISTD_1:def 5 { IC Following s : IC s = l & s.l = i }; end; definition let N be with_non-empty_elements set, S be realistic IC-Ins-separated definite (non empty non void AMI-Struct over N), i be Element of the Instructions of S, l be Instruction-Location of S; cluster NIC(i,l) -> non empty; end; definition let N,S,i; func JUMP i -> Subset of the Instruction-Locations of S equals :: AMISTD_1:def 6 meet { NIC(i,l) : not contradiction }; end; definition let N,S,l; func SUCC l -> Subset of the Instruction-Locations of S equals :: AMISTD_1:def 7 union { NIC(i,l) \ JUMP i : not contradiction }; end; theorem :: AMISTD_1:14 for i being Element of the Instructions of S st the Instruction-Locations of S is non trivial & (for l being Instruction-Location of S holds NIC(i,l)={l}) holds JUMP i is empty; theorem :: AMISTD_1:15 for S being realistic IC-Ins-separated definite (non empty non void AMI-Struct over N), il being Instruction-Location of S, i being Instruction of S st i is halting holds NIC(i,il) = {il}; begin :: Ordering of Instruction Locations definition let N,S,l1,l2; pred l1 <= l2 means :: AMISTD_1:def 8 ex f being non empty FinSequence of the Instruction-Locations of S st f/.1 = l1 & f/.len f = l2 & for n st 1 <= n & n < len f holds f/.(n+1) in SUCC f/.n; reflexivity; end; theorem :: AMISTD_1:16 l1 <= l2 & l2 <= l3 implies l1 <= l3; definition let N, S; attr S is InsLoc-antisymmetric means :: AMISTD_1:def 9 for l1, l2 st l1 <= l2 & l2 <= l1 holds l1 = l2; end; definition let N, S; attr S is standard means :: AMISTD_1:def 10 ex f being Function of NAT, the Instruction-Locations of S st f is bijective & for m, n being Nat holds m <= n iff f.m <= f.n; end; theorem :: AMISTD_1:17 for f1, f2 being Function of NAT, the Instruction-Locations of S st f1 is bijective & (for m, n being Nat holds m <= n iff f1.m <= f1.n) & f2 is bijective & (for m, n being Nat holds m <= n iff f2.m <= f2.n) holds f1 = f2; theorem :: AMISTD_1:18 for f being Function of NAT, the Instruction-Locations of S st f is bijective holds (for m, n being Nat holds m <= n iff f.m <= f.n) iff (for k being Nat holds f.(k+1) in SUCC (f.k) & for j being Nat st f.j in SUCC (f.k) holds k <= j); theorem :: AMISTD_1:19 S is standard iff ex f being Function of NAT, the Instruction-Locations of S st f is bijective & for k being Nat holds f.(k+1) in SUCC (f.k) & for j being Nat st f.j in SUCC (f.k) holds k <= j; begin :: Standard trivial computer definition let N be with_non-empty_elements set; func STC N -> strict AMI-Struct over N means :: AMISTD_1:def 11 the carrier of it = NAT \/ {NAT} & the Instruction-Counter of it = NAT & the Instruction-Locations of it = NAT & the Instruction-Codes of it = {0,1} & 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); end; definition let N be with_non-empty_elements set; cluster the Instruction-Locations of STC N -> infinite; end; definition let N be with_non-empty_elements set; cluster STC N -> non empty non void; end; definition let N be with_non-empty_elements set; cluster STC N -> IC-Ins-separated definite realistic steady-programmed data-oriented; end; theorem :: AMISTD_1:20 for i being Instruction of STC N st InsCode i = 0 holds i is halting; theorem :: AMISTD_1:21 for i being Instruction of STC N st InsCode i = 1 holds i is non halting; theorem :: AMISTD_1:22 for i being Element of the Instructions of STC N holds InsCode i = 1 or InsCode i = 0; theorem :: AMISTD_1:23 for i being Instruction of STC N holds i is jump-only; theorem :: AMISTD_1:24 for l being Instruction-Location of STC N st l = z holds SUCC l = {z, z+1}; definition let N be with_non-empty_elements set; cluster STC N -> standard; end; definition let N be with_non-empty_elements set; cluster STC N -> halting; end; definition let N be with_non-empty_elements set; cluster standard halting realistic steady-programmed programmable (IC-Ins-separated definite (non empty non void AMI-Struct over N)); end; reserve T for standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)); definition let N be with_non-empty_elements set, S be standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), k be natural number; func il.(S,k) -> Instruction-Location of S means :: AMISTD_1:def 12 ex f being Function of NAT, the Instruction-Locations of S st f is bijective & (for m, n being Nat holds m <= n iff f.m <= f.n) & it = f.k; end; theorem :: AMISTD_1:25 for k1, k2 being natural number st il.(T,k1) = il.(T,k2) holds k1 = k2; theorem :: AMISTD_1:26 for l being Instruction-Location of T ex k being natural number st l = il.(T,k); definition let N be with_non-empty_elements set, S be standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), l be Instruction-Location of S; func locnum l -> natural number means :: AMISTD_1:def 13 il.(S,it) = l; end; definition let N be with_non-empty_elements set, S be standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), l be Instruction-Location of S; redefine func locnum l -> Nat; end; theorem :: AMISTD_1:27 for l1, l2 being Instruction-Location of T holds locnum l1 = locnum l2 implies l1 = l2; theorem :: AMISTD_1:28 for k1, k2 being natural number holds il.(T,k1) <= il.(T,k2) iff k1 <= k2; theorem :: AMISTD_1:29 for l1, l2 being Instruction-Location of T holds locnum l1 <= locnum l2 iff l1 <= l2; theorem :: AMISTD_1:30 S is standard implies S is InsLoc-antisymmetric; definition let N; cluster standard -> InsLoc-antisymmetric (IC-Ins-separated definite (non empty non void AMI-Struct over N)); end; definition let N be with_non-empty_elements set, S be standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), f be Instruction-Location of S, k be natural number; func f + k -> Instruction-Location of S equals :: AMISTD_1:def 14 il.(S,locnum f + k); end; theorem :: AMISTD_1:31 for f being Instruction-Location of T holds f + 0 = f; theorem :: AMISTD_1:32 for f, g being Instruction-Location of T st f + z = g + z holds f = g; theorem :: AMISTD_1:33 for f being Instruction-Location of T holds locnum f + z = locnum (f + z); definition let N be with_non-empty_elements set, S be standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), f be Instruction-Location of S; func NextLoc f -> Instruction-Location of S equals :: AMISTD_1:def 15 f + 1; end; theorem :: AMISTD_1:34 for f being Instruction-Location of T holds NextLoc f = il.(T,locnum f + 1); theorem :: AMISTD_1:35 for f being Instruction-Location of T holds f <> NextLoc f; theorem :: AMISTD_1:36 for f, g being Instruction-Location of T st NextLoc f = NextLoc g holds f = g; theorem :: AMISTD_1:37 il.(STC N, z) = z; theorem :: AMISTD_1:38 for i being Instruction of STC N, s being State of STC N st InsCode i = 1 holds Exec(i,s).IC STC N = NextLoc IC s; theorem :: AMISTD_1:39 for l being Instruction-Location of STC N, i being Element of the Instructions of STC N st InsCode i = 1 holds NIC(i, l) = {NextLoc l}; theorem :: AMISTD_1:40 for l being Instruction-Location of STC N holds SUCC l = {l, NextLoc l}; definition let N be with_non-empty_elements set, S be standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), i be Instruction of S; attr i is sequential means :: AMISTD_1:def 16 for s being State of S holds Exec(i, s).IC S = NextLoc IC s; end; theorem :: AMISTD_1:41 for S being standard realistic (IC-Ins-separated definite (non empty non void AMI-Struct over N)), il being Instruction-Location of S, i being Instruction of S st i is sequential holds NIC(i,il) = {NextLoc il}; theorem :: AMISTD_1:42 for S being realistic standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), i being Instruction of S st i is sequential holds i is non halting; definition let N; let S be realistic standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)); cluster sequential -> non halting Instruction of S; cluster halting -> non sequential Instruction of S; end; theorem :: AMISTD_1:43 for i being Instruction of T st JUMP i is non empty holds i is non sequential ; begin :: Closedness of finite partial states definition let N be with_non-empty_elements set; let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let F be FinPartState of S; attr F is closed means :: AMISTD_1:def 17 for l being Instruction-Location of S st l in dom F holds NIC (pi(F,l), l) c= dom F; attr F is really-closed means :: AMISTD_1:def 18 for s being State of S st F c= s & IC s in dom F for k being Nat holds IC (Computation s).k in dom F; end; definition let N be with_non-empty_elements set; let S be standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)); let F be FinPartState of S; attr F is para-closed means :: AMISTD_1:def 19 for s being State of S st F c= s & IC s = il.(S,0) for k being Nat holds IC (Computation s).k in dom F; end; theorem :: AMISTD_1:44 for S being standard steady-programmed (IC-Ins-separated definite (non empty non void AMI-Struct over N)), F being FinPartState of S st F is really-closed & il.(S,0) in dom F holds F is para-closed; theorem :: AMISTD_1:45 for S being IC-Ins-separated definite steady-programmed (non empty non void AMI-Struct over N), F being FinPartState of S st F is closed holds F is really-closed; definition let N be with_non-empty_elements set, S be IC-Ins-separated definite steady-programmed (non empty non void AMI-Struct over N); cluster closed -> really-closed FinPartState of S; end; theorem :: AMISTD_1:46 for S being standard realistic halting (IC-Ins-separated definite (non empty non void AMI-Struct over N)) holds il.(S,0) .--> halt S is closed; definition let N be with_non-empty_elements set; let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let F be FinPartState of S; attr F is lower means :: AMISTD_1:def 20 for l being Instruction-Location of S st l in dom F holds for m being Instruction-Location of S st m <= l holds m in dom F; end; theorem :: AMISTD_1:47 for F being empty FinPartState of S holds F is lower; definition let N be with_non-empty_elements set, S be IC-Ins-separated definite (non empty non void AMI-Struct over N); cluster empty -> lower FinPartState of S; end; theorem :: AMISTD_1:48 for i being Element of the Instructions of T holds il.(T,0) .--> i is lower; definition let N be with_non-empty_elements set; let S be standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)); cluster lower non empty trivial programmed FinPartState of S; end; theorem :: AMISTD_1:49 for F being lower non empty programmed FinPartState of T holds il.(T,0) in dom F; theorem :: AMISTD_1:50 for P being lower programmed FinPartState of T holds z < card P iff il.(T,z) in dom P; definition let N be with_non-empty_elements set; let S be standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)); let F be non empty programmed FinPartState of S; func LastLoc F -> Instruction-Location of S means :: AMISTD_1:def 21 ex M being finite non empty natural-membered set st M = { locnum l where l is Element of the Instruction-Locations of S : l in dom F } & it = il.(S, max M); end; theorem :: AMISTD_1:51 for F being non empty programmed FinPartState of T holds LastLoc F in dom F; theorem :: AMISTD_1:52 for F, G being non empty programmed FinPartState of T st F c= G holds LastLoc F <= LastLoc G; theorem :: AMISTD_1:53 for F being non empty programmed FinPartState of T, l being Instruction-Location of T st l in dom F holds l <= LastLoc F; theorem :: AMISTD_1:54 for F being lower non empty programmed FinPartState of T, G being non empty programmed FinPartState of T holds F c= G & LastLoc F = LastLoc G implies F = G; theorem :: AMISTD_1:55 for F being lower non empty programmed FinPartState of T holds LastLoc F = il.(T, card F -' 1); definition let N be with_non-empty_elements set, S be standard steady-programmed (IC-Ins-separated definite (non empty non void AMI-Struct over N)); cluster really-closed lower non empty programmed -> para-closed FinPartState of S; end; definition let N be with_non-empty_elements set, S be standard halting (IC-Ins-separated definite (non empty non void AMI-Struct over N)), F be non empty programmed FinPartState of S; attr F is halt-ending means :: AMISTD_1:def 22 F.(LastLoc F) = halt S; attr F is unique-halt means :: AMISTD_1:def 23 for f being Instruction-Location of S st F.f = halt S & f in dom F holds f = LastLoc F; end; definition let N be with_non-empty_elements set; let S be standard halting (IC-Ins-separated definite (non empty non void AMI-Struct over N)); cluster halt-ending unique-halt trivial (lower non empty programmed FinPartState of S); end; definition let N be with_non-empty_elements set; let S be standard halting realistic (IC-Ins-separated definite (non empty non void AMI-Struct over N)); cluster trivial closed lower non empty programmed FinPartState of S; end; definition let N be with_non-empty_elements set; let S be standard halting realistic (IC-Ins-separated definite (non empty non void AMI-Struct over N)); cluster halt-ending unique-halt trivial closed (lower non empty programmed FinPartState of S); end; definition let N be with_non-empty_elements set; let S be standard halting realistic steady-programmed (IC-Ins-separated definite (non empty non void AMI-Struct over N)); cluster halt-ending unique-halt autonomic trivial closed (lower non empty programmed FinPartState of S); end; definition let N be with_non-empty_elements set; let S be standard halting (IC-Ins-separated definite (non empty non void AMI-Struct over N)); mode pre-Macro of S is halt-ending unique-halt (lower non empty programmed FinPartState of S); canceled; end; definition let N be with_non-empty_elements set; let S be standard realistic halting (IC-Ins-separated definite (non empty non void AMI-Struct over N)); cluster closed pre-Macro of S; end;

Back to top