Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users

### Input and Output of Instructions

by
Artur Kornilowicz

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
(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;
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

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 };
```