:: Input and Output of Instructions :: by Artur Korni{\l}owicz :: :: Received May 8, 2001 :: Copyright (c) 2001-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, AMI_1, FSM_1, CAT_1, FUNCT_1, RELAT_1, STRUCT_0, SUBSET_1, FUNCT_4, FUNCOP_1, GOBOARD5, FRECHET, AMISTD_1, ZFMISC_1, NUMBERS, CARD_1, GLIB_000, AMISTD_2, NET_1, TARSKI, AMISTD_4, QUANTAL1, GOBRD13, MEMSTR_0, COMPOS_1, ARYTM_3; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ZFMISC_1, XTUPLE_0, MCART_1, ORDINAL1, NUMBERS, FUNCOP_1, FUNCT_4, XCMPLX_0, NAT_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, MEASURE6, AMISTD_1, AMISTD_2; constructors ZFMISC_1, AMISTD_2, NAT_1, PRE_POLY, EXTPRO_1, AMISTD_1, DOMAIN_1, FUNCT_7, FUNCT_4, MEMSTR_0, RELSET_1, MEASURE6, PBOOLE, XTUPLE_0; registrations FUNCOP_1, STRUCT_0, AMISTD_1, AMISTD_2, ORDINAL1, EXTPRO_1, ORDINAL6, FUNCT_4, MEMSTR_0, MEASURE6; requirements SUBSET, BOOLE, NUMERALS; begin :: Preliminaries reserve N for with_zero set; definition let N be with_zero set, A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, s be State of A, o be Object of A, a be Element of Values o; redefine func s+*(o,a) -> State of A; end; theorem :: AMISTD_4:1 for A being standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A, s being State of A, o being Object of A, w being Element of Values o st I is sequential & o <> IC A holds IC Exec(I,s) = IC Exec(I,s+*(o,w)); theorem :: AMISTD_4:2 for A being standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A, s being State of A, o being Object of A, w being Element of Values o st I is sequential & o <> IC A holds IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w)); begin :: Input and Output of Instructions definition let A be COM-Struct; attr A is with_non_trivial_Instructions means :: AMISTD_4:def 1 the InstructionsF of A is non trivial; end; definition let N be with_zero set, A be non empty with_non-empty_values AMI-Struct over N; attr A is with_non_trivial_ObjectKinds means :: AMISTD_4:def 2 for o being Object of A holds Values o is non trivial; end; registration let N be with_zero set; cluster STC N -> with_non_trivial_ObjectKinds; end; registration let N be with_zero set; cluster with_explicit_jumps IC-relocable with_non_trivial_ObjectKinds with_non_trivial_Instructions for standard halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; end; registration let N be with_zero set; cluster STC N -> with_non_trivial_Instructions; end; registration let N be with_zero set; cluster with_non_trivial_ObjectKinds with_non_trivial_Instructions IC-Ins-separated for non empty with_non-empty_values AMI-Struct over N; end; registration let N be with_zero set, A be with_non_trivial_ObjectKinds non empty with_non-empty_values AMI-Struct over N, o be Object of A; cluster Values o -> non trivial; end; registration let N be with_zero set, A be with_non_trivial_Instructions with_non-empty_values AMI-Struct over N; cluster the InstructionsF of A -> non trivial; end; registration let N be with_zero set, A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; cluster Values IC A -> non trivial; end; definition let N be with_zero set, A be non empty with_non-empty_values AMI-Struct over N, I be Instruction of A; func Output I -> Subset of A means :: AMISTD_4: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_zero set, A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A; func Out_\_Inp I -> Subset of A means :: AMISTD_4:def 4 for o being Object of A holds o in it iff for s being State of A, a being Element of Values o holds Exec(I, s) = Exec(I,s+*(o,a)); func Out_U_Inp I -> Subset of A means :: AMISTD_4:def 5 for o being Object of A holds o in it iff ex s being State of A, a being Element of Values o st Exec(I,s+*( o,a)) <> Exec(I,s) +* (o,a); end; definition let N be with_zero set, A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A; func Input I -> Subset of A equals :: AMISTD_4:def 6 Out_U_Inp I \ Out_\_Inp I; end; theorem :: AMISTD_4:3 for A being with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A holds Out_\_Inp I c= Output I; theorem :: AMISTD_4:4 for A being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A holds Output I c= Out_U_Inp I; theorem :: AMISTD_4:5 for A being with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A holds Out_\_Inp I = Output I \ Input I; theorem :: AMISTD_4:6 for A being with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A holds Out_U_Inp I = Output I \/ Input I; theorem :: AMISTD_4:7 for A being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A, o being Object of A st Values o is trivial holds not o in Out_U_Inp I; theorem :: AMISTD_4:8 for A being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N , I being Instruction of A, o being Object of A st Values o is trivial holds not o in Input I; theorem :: AMISTD_4:9 for A being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N , I being Instruction of A, o being Object of A st Values o is trivial holds not o in Output I; theorem :: AMISTD_4:10 for A being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A holds I is halting iff Output I is empty; theorem :: AMISTD_4:11 for A being with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A st I is halting holds Out_\_Inp I is empty; theorem :: AMISTD_4:12 for A being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A st I is halting holds Out_U_Inp I is empty; theorem :: AMISTD_4:13 for A being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A st I is halting holds Input I is empty; registration let N be with_zero set, A be halting IC-Ins-separated non empty with_non-empty_values 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; registration let N be with_zero set; cluster halting with_non_trivial_ObjectKinds IC-Ins-separated for non empty with_non-empty_values AMI-Struct over N; end; registration let N be with_zero set, A be halting with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be halting Instruction of A; cluster Out_\_Inp I -> empty; end; registration let N; cluster with_non_trivial_Instructions IC-Ins-separated for non empty with_non-empty_values AMI-Struct over N; end; theorem :: AMISTD_4:14 for A being standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A st I is sequential holds not IC A in Out_\_Inp I; theorem :: AMISTD_4:15 for A being IC-Ins-separated non empty with_non-empty_values 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; registration let N; cluster standard for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; end; theorem :: AMISTD_4:16 for A being standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A st I is sequential holds IC A in Output I; theorem :: AMISTD_4:17 for A being IC-Ins-separated non empty with_non-empty_values 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 :: AMISTD_4:18 for A being standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I being Instruction of A st I is sequential holds IC A in Out_U_Inp I; theorem :: AMISTD_4:19 for A being IC-Ins-separated non empty with_non-empty_values 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;