Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### The abstract of the Mizar article:

### Input and Output of Instructions

**by****Artur Kornilowicz**- Received May 8, 2001
- MML identifier: AMI_7

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_3, AMI_1, BOOLE, CAT_1, FUNCT_1, RELAT_1, FUNCT_4, GOBOARD5, FRECHET, AMISTD_1, REALSET1, FUNCOP_1, AMISTD_2, CARD_5, NET_1, AMI_5, AMI_2, INT_1, FINSEQ_1, ARYTM_1, SQUARE_1, ARYTM_3, NAT_1, AMI_7; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, REALSET1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, FINSEQ_1, FUNCOP_1, CQC_LANG, INT_1, NAT_1, FUNCT_4, STRUCT_0, AMI_1, AMI_2, AMI_3, AMI_5, FUNCT_7, AMISTD_1, AMISTD_2; constructors DOMAIN_1, FUNCT_7, NAT_1, AMI_5, SQUARE_1, AMISTD_2, REALSET1, PRE_CIRC; clusters AMI_1, XREAL_0, INT_1, AMISTD_1, SCMRING1, AMI_6, AMISTD_2, RELSET_1, FUNCOP_1, WAYBEL12, SCMRING3, SQUARE_1, XBOOLE_0, FRAENKEL; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin :: Preliminaries reserve N for with_non-empty_elements set; theorem :: AMI_7:1 for x, y, z being set st x <> y & x <> z holds {x, y, z} \ {x} = {y, z}; theorem :: AMI_7:2 for A being non empty non void AMI-Struct over N, s being State of A, o being Object of A holds s.o in ObjectKind o; theorem :: AMI_7:3 for A being realistic IC-Ins-separated definite (non empty non void AMI-Struct over N), s being State of A, f being Instruction-Location of A, w being Element of ObjectKind IC A holds (s+*(IC A,w)).f = s.f; definition let N be with_non-empty_elements set, A be IC-Ins-separated definite (non empty non void AMI-Struct over N), s be State of A, o be Object of A, a be Element of ObjectKind o; redefine func s+*(o,a) -> State of A; end; theorem :: AMI_7:4 for A being steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N), s being State of A, o being Object of A, f being Instruction-Location of A, I being Instruction of A, w being Element of ObjectKind o st f <> o holds Exec(I,s).f = Exec(I,s+*(o,w)).f; theorem :: AMI_7:5 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), s being State of A, o being Object of A, w being Element of ObjectKind o st o <> IC A holds IC s = IC (s+*(o,w)); theorem :: AMI_7:6 for A being standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), I being Instruction of A, s being State of A, o being Object of A, w being Element of ObjectKind o st I is sequential & o <> IC A holds IC Exec(I,s) = IC Exec(I,s+*(o,w)); theorem :: AMI_7:7 for A being standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), I being Instruction of A, s being State of A, o being Object of A, w being Element of ObjectKind o st I is sequential & o <> IC A holds IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w)); theorem :: AMI_7:8 for A being standard steady-programmed (IC-Ins-separated definite (non empty non void AMI-Struct over N)), I being Instruction of A, s being State of A, o being Object of A, w being Element of ObjectKind o, i being Instruction-Location of A holds Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i; begin :: Input and Output of Instructions definition let N be set, A be AMI-Struct over N; attr A is with_non_trivial_Instructions means :: AMI_7:def 1 the Instructions of A is non trivial; end; definition let N be set, A be non empty AMI-Struct over N; attr A is with_non_trivial_ObjectKinds means :: AMI_7:def 2 for o being Object of A holds ObjectKind o is non trivial; end; definition let N be with_non-empty_elements set; cluster STC N -> with_non_trivial_ObjectKinds; end; definition let N be with_non-empty_elements set; cluster halting realistic steady-programmed programmable with_explicit_jumps without_implicit_jumps IC-good Exec-preserving with_non_trivial_ObjectKinds with_non_trivial_Instructions (regular standard (IC-Ins-separated definite (non empty non void AMI-Struct over N))); end; definition let N be with_non-empty_elements set; cluster with_non_trivial_ObjectKinds -> with_non_trivial_Instructions (definite (non empty non void AMI-Struct over N)); end; definition let N be with_non-empty_elements set; cluster with_non_trivial_ObjectKinds -> with-non-trivial-Instruction-Locations (IC-Ins-separated (non empty AMI-Struct over N)); end; definition let N be with_non-empty_elements set, A be with_non_trivial_ObjectKinds (non empty AMI-Struct over N), o be Object of A; cluster ObjectKind o -> non trivial; end; definition let N be with_non-empty_elements set, A be with_non_trivial_Instructions AMI-Struct over N; cluster the Instructions of A -> non trivial; end; definition let N be with_non-empty_elements set, A be with-non-trivial-Instruction-Locations IC-Ins-separated (non empty AMI-Struct over N); cluster ObjectKind IC A -> non trivial; end; definition let N be with_non-empty_elements set, A be non empty non void AMI-Struct over N, I be Instruction of A; func Output I -> Subset of A means :: AMI_7:def 3 for o being Object of A holds o in it iff ex s being State of A st s.o <> Exec(I,s).o; end; definition let N be with_non-empty_elements set, A be IC-Ins-separated definite (non empty non void AMI-Struct over N), I be Instruction of A; func Out_\_Inp I -> Subset of A means :: AMI_7:def 4 for o being Object of A holds o in it iff for s being State of A, a being Element of ObjectKind o holds Exec(I,s) = Exec(I,s+*(o,a)); func Out_U_Inp I -> Subset of A means :: AMI_7:def 5 for o being Object of A holds o in it iff ex s being State of A, a being Element of ObjectKind o st Exec(I,s+*(o,a)) <> Exec(I,s) +* (o,a); end; definition let N be with_non-empty_elements set, A be IC-Ins-separated definite (non empty non void AMI-Struct over N), I be Instruction of A; func Input I -> Subset of A equals :: AMI_7:def 6 Out_U_Inp I \ Out_\_Inp I; end; theorem :: AMI_7:9 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A holds Out_\_Inp I misses Input I; theorem :: AMI_7:10 for A being with_non_trivial_ObjectKinds IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A holds Out_\_Inp I c= Output I; theorem :: AMI_7:11 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A holds Output I c= Out_U_Inp I; theorem :: AMI_7:12 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A holds Input I c= Out_U_Inp I; theorem :: AMI_7:13 for A being with_non_trivial_ObjectKinds IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A holds Out_\_Inp I = Output I \ Input I; theorem :: AMI_7:14 for A being with_non_trivial_ObjectKinds IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A holds Out_U_Inp I = Output I \/ Input I; theorem :: AMI_7:15 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A, o being Object of A st ObjectKind o is trivial holds not o in Out_U_Inp I; theorem :: AMI_7:16 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N) , I being Instruction of A, o being Object of A st ObjectKind o is trivial holds not o in Input I; theorem :: AMI_7:17 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N) , I being Instruction of A, o being Object of A st ObjectKind o is trivial holds not o in Output I; theorem :: AMI_7:18 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A holds I is halting iff Output I is empty; theorem :: AMI_7:19 for A being with_non_trivial_ObjectKinds IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A st I is halting holds Out_\_Inp I is empty; theorem :: AMI_7:20 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A st I is halting holds Out_U_Inp I is empty; theorem :: AMI_7:21 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A st I is halting holds Input I is empty; definition let N be with_non-empty_elements set, A be halting IC-Ins-separated definite (non empty non void AMI-Struct over N), I be halting Instruction of A; cluster Input I -> empty; cluster Output I -> empty; cluster Out_U_Inp I -> empty; end; definition let N be with_non-empty_elements set, A be halting with_non_trivial_ObjectKinds IC-Ins-separated definite (non empty non void AMI-Struct over N), I be halting Instruction of A; cluster Out_\_Inp I -> empty; end; theorem :: AMI_7:22 for A being with_non_trivial_Instructions steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N), f being Instruction-Location of A, I being Instruction of A holds not f in Out_\_Inp I; theorem :: AMI_7:23 for A being standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), I being Instruction of A st I is sequential holds not IC A in Out_\_Inp I; theorem :: AMI_7:24 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A st ex s being State of A st Exec(I,s).IC A <> IC s holds IC A in Output I; theorem :: AMI_7:25 for A being standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), I being Instruction of A st I is sequential holds IC A in Output I; theorem :: AMI_7:26 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), I being Instruction of A st ex s being State of A st Exec(I,s).IC A <> IC s holds IC A in Out_U_Inp I; theorem :: AMI_7:27 for A being standard (IC-Ins-separated definite (non empty non void AMI-Struct over N)), I being Instruction of A st I is sequential holds IC A in Out_U_Inp I; theorem :: AMI_7:28 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N), f being Instruction-Location of A, I being Instruction of A st for s being State of A, p being programmed FinPartState of A holds Exec (I, s +* p) = Exec (I,s) +* p holds not f in Out_U_Inp I; theorem :: AMI_7:29 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N) , I being Instruction of A, o being Object of A st I is jump-only holds o in Output I implies o = IC A; begin :: SCM reserve a, b for Data-Location, f for Instruction-Location of SCM, I for Instruction of SCM; theorem :: AMI_7:30 for s being State of SCM, w being Element of ObjectKind IC SCM holds (s+*(IC SCM,w)).a = s.a; theorem :: AMI_7:31 f <> Next f; definition let s be State of SCM, dl be Data-Location, k be Integer; redefine func s+*(dl,k) -> State of SCM; end; definition cluster SCM -> with_non_trivial_ObjectKinds; end; theorem :: AMI_7:32 Out_\_Inp (a:=a) = {}; theorem :: AMI_7:33 a <> b implies Out_\_Inp (a:=b) = { a }; theorem :: AMI_7:34 Out_\_Inp AddTo(a,b) = {}; theorem :: AMI_7:35 Out_\_Inp SubFrom(a,a) = { a }; theorem :: AMI_7:36 a <> b implies Out_\_Inp SubFrom(a,b) = {}; theorem :: AMI_7:37 Out_\_Inp MultBy(a,b) = {}; theorem :: AMI_7:38 Out_\_Inp Divide(a,a) = { a }; theorem :: AMI_7:39 a <> b implies Out_\_Inp Divide(a,b) = {}; theorem :: AMI_7:40 Out_\_Inp goto f = { IC SCM }; theorem :: AMI_7:41 Out_\_Inp (a =0_goto f) = {}; theorem :: AMI_7:42 Out_\_Inp (a >0_goto f) = {}; theorem :: AMI_7:43 Output (a:=a) = { IC SCM }; theorem :: AMI_7:44 a <> b implies Output (a:=b) = { a, IC SCM }; theorem :: AMI_7:45 Output AddTo(a,b) = { a, IC SCM }; theorem :: AMI_7:46 Output SubFrom(a,b) = { a, IC SCM }; theorem :: AMI_7:47 Output MultBy(a,b) = { a, IC SCM }; theorem :: AMI_7:48 Output Divide(a,b) = { a, b, IC SCM }; theorem :: AMI_7:49 Output goto f = { IC SCM }; theorem :: AMI_7:50 Output (a =0_goto f) = { IC SCM }; theorem :: AMI_7:51 Output (a >0_goto f) = { IC SCM }; theorem :: AMI_7:52 not f in Out_U_Inp I; theorem :: AMI_7:53 Out_U_Inp (a:=a) = { IC SCM }; theorem :: AMI_7:54 a <> b implies Out_U_Inp (a:=b) = { a, b, IC SCM }; theorem :: AMI_7:55 Out_U_Inp AddTo(a,b) = { a, b, IC SCM }; theorem :: AMI_7:56 Out_U_Inp SubFrom(a,b) = { a, b, IC SCM }; theorem :: AMI_7:57 Out_U_Inp MultBy(a,b) = { a, b, IC SCM }; theorem :: AMI_7:58 Out_U_Inp Divide(a,b) = { a, b, IC SCM }; theorem :: AMI_7:59 Out_U_Inp (goto f) = { IC SCM }; theorem :: AMI_7:60 Out_U_Inp (a =0_goto f) = { a, IC SCM }; theorem :: AMI_7:61 Out_U_Inp (a >0_goto f) = { a, IC SCM }; theorem :: AMI_7:62 Input (a:=a) = { IC SCM }; theorem :: AMI_7:63 a <> b implies Input (a:=b) = { b, IC SCM }; theorem :: AMI_7:64 Input AddTo(a,b) = { a, b, IC SCM }; theorem :: AMI_7:65 Input SubFrom(a,a) = { IC SCM }; theorem :: AMI_7:66 a <> b implies Input SubFrom(a,b) = { a, b, IC SCM }; theorem :: AMI_7:67 Input MultBy(a,b) = { a, b, IC SCM }; theorem :: AMI_7:68 Input Divide(a,a) = { IC SCM }; theorem :: AMI_7:69 a <> b implies Input Divide(a,b) = { a, b, IC SCM }; theorem :: AMI_7:70 Input goto f = {}; theorem :: AMI_7:71 Input (a =0_goto f) = { a, IC SCM }; theorem :: AMI_7:72 Input (a >0_goto f) = { a, IC SCM };

Back to top