:: Input and Output of Instructions
:: by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001-2026 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;
definitions EXTPRO_1, AMISTD_1, XBOOLE_0;
equalities XBOOLE_0, FUNCOP_1, MEMSTR_0;
expansions XBOOLE_0;
theorems FUNCT_7, TARSKI, AMISTD_1, SUBSET_1, FUNCOP_1, ZFMISC_1, FUNCT_1,
XBOOLE_0, XBOOLE_1, PARTFUN1, STRUCT_0, MEMSTR_0, MEASURE6, XTUPLE_0,
NAT_1;
schemes SUBSET_1;
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; :: redefines +* (FUNCT_7, definition)
coherence
proof
dom s = the carrier of A by PARTFUN1:def 2;
then s+*(o,a) = s+*(o .--> a) by FUNCT_7:def 3;
hence thesis;
end;
end;
theorem Th1:
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))
proof
let A be standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N, I be Instruction of A,
s be State of A, o be Object of
A, w be Element of Values o such that
A1: for s being State of A holds Exec(I,s).IC A = IC s + 1 and
A2: o <> IC A;
thus IC Exec(I,s) = IC s + 1 by A1
.= IC (s+*(o,w)) + 1 by A2,FUNCT_7:32
.= IC Exec(I,s+*(o,w)) by A1;
end;
theorem
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))
proof
let A be standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N, I be Instruction of A,
s be State of A, o be Object of
A, w be Element of Values o such that
A1: I is sequential and
A2: o <> IC A;
thus IC Exec(I,s+*(o,w)) = IC Exec(I,s) by A1,A2,Th1
.= IC (Exec(I,s) +* (o,w)) by A2,FUNCT_7:32;
end;
begin :: Input and Output of Instructions
definition
let A be COM-Struct;
attr A is with_non_trivial_Instructions means
:Def1:
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
:Def2:
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;
coherence
proof
let o be Object of STC N;
A1: the carrier of STC N = {0} by AMISTD_1:def 7;
A2: the Object-Kind of STC N = 0 .--> 0
by AMISTD_1:def 7;
per cases by A1;
suppose
A3: o in {0};
A4: the ValuesF of STC N = N --> NAT by AMISTD_1:def 7;
0 in N by MEASURE6:def 2;
then the_Values_of STC N = 0 .--> NAT by A2,A4,FUNCOP_1:89;
then Values o = (0 .--> NAT).o
.= NAT by A3,FUNCOP_1:7;
hence thesis;
end;
end;
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;
existence
proof
take STC N;
A1: [1,0,0] in {[1,0,0],[0,0,0]} & [0,0,0] in {[1,0,0],[0,0,0]}
by TARSKI:def 2;
the InstructionsF of STC N = {[0,0,0],[1,0,0]} & [1,0,0] <> [0,0,0] by
AMISTD_1:def 7,XTUPLE_0:3;
then the InstructionsF of STC N is non trivial by A1,ZFMISC_1:def 10;
hence thesis;
end;
end;
registration
let N be with_zero set;
cluster STC N -> with_non_trivial_Instructions;
coherence
proof
A1: [0,0,0] <> [1,0,0] by XTUPLE_0:3;
the InstructionsF of STC N = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;
then [0,0,0] in the InstructionsF of STC N
& [1,0,0] in the InstructionsF of STC N by TARSKI:def 2;
hence the InstructionsF of STC N is non trivial by A1,ZFMISC_1:def 10;
end;
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;
existence
proof
take STC N;
thus thesis;
end;
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;
coherence by Def2;
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;
coherence by Def1;
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;
coherence by MEMSTR_0:def 6;
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
:Def3:
for o being Object of A holds o in
it iff ex s being State of A st s.o <> Exec(I,s).o;
existence
proof
defpred P[set] means ex s being State of A st s.$1 <> Exec(I,s).$1;
consider X being Subset of A such that
A1: for x being set holds x in X iff x in the carrier of A & P[x] from
SUBSET_1:sch 1;
take X;
thus thesis by A1;
end;
uniqueness
proof
defpred P[set] means ex s being State of A st s.$1 <> Exec(I,s).$1;
let a, b be Subset of A such that
A2: for o being Object of A holds o in a iff P[o] and
A3: for o being Object of A holds o in b iff P[o];
thus a = b from SUBSET_1:sch 2(A2,A3);
end;
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
:Def4:
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));
existence
proof
defpred P[set] means ex l being Object of A st l = $1 & for s being State
of A, a being Element of Values l holds Exec(I,s) = Exec(I,s+*(l,a));
consider X being Subset of A such that
A1: for x being set holds x in X iff x in the carrier of A & P[x] from
SUBSET_1:sch 1;
take X;
let l be Object of A;
hereby
assume l in X;
then P[l] by A1;
hence
for s being State of A, a being Element of Values l holds Exec(
I,s) = Exec(I,s+*(l,a));
end;
thus thesis by A1;
end;
uniqueness
proof
defpred P[Object of A] means for s being State of A, a being Element of
Values $1 holds Exec(I,s) = Exec(I,s+*($1,a));
let a, b be Subset of A such that
A2: for o being Object of A holds o in a iff P[o] and
A3: for o being Object of A holds o in b iff P[o];
thus a = b from SUBSET_1:sch 2(A2,A3);
end;
func Out_U_Inp I -> Subset of A means
:Def5:
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);
existence
proof
defpred P[set] means ex l being Object of A st l = $1 & ex s being State
of A, a being Element of Values l st Exec(I,s+*(l,a)) <> Exec(I,s) +* (l,a);
consider X being Subset of A such that
A4: for x being set holds x in X iff x in the carrier of A & P[x] from
SUBSET_1:sch 1;
take X;
let l be Object of A;
hereby
assume l in X;
then P[l] by A4;
hence ex s being State of A, a being Element of Values l st Exec(I,s
+*(l,a)) <> Exec(I,s) +* (l,a);
end;
thus thesis by A4;
end;
uniqueness
proof
defpred P[Object of A] means ex s being State of A, a being Element of
Values $1 st Exec(I,s+*($1,a)) <> Exec(I,s) +* ($1,a);
let a, b be Subset of A such that
A5: for o being Object of A holds o in a iff P[o] and
A6: for o being Object of A holds o in b iff P[o];
thus a = b from SUBSET_1:sch 2(A5,A6);
end;
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
Out_U_Inp I \ Out_\_Inp I;
coherence;
end;
theorem Th3:
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
proof
let A be with_non_trivial_ObjectKinds IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N, I be Instruction of A;
for o being Object of A holds o in Out_\_Inp I implies o in Output I
proof
let o be Object of A;
set s = the State of A,a = the Element of Values o;
consider w being object such that
A1: w in Values o and
A2: w <> a by SUBSET_1:48;
reconsider w as Element of Values o by A1;
set t = s +* (o,w);
A3: dom t = the carrier of A by PARTFUN1:def 2;
A4: dom s = the carrier of A by PARTFUN1:def 2;
assume
A5: not thesis;
then
A6: Exec(I,t+*(o,a)).o = (t+*(o,a)).o by Def3
.= a by A3,FUNCT_7:31;
Exec(I,t).o = t.o by A5,Def3
.= w by A4,FUNCT_7:31;
hence contradiction by A5,A2,A6,Def4;
end;
hence thesis by SUBSET_1:2;
end;
theorem Th4:
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
proof
let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
N, I be Instruction of A;
for o being Object of A holds o in Output I implies o in Out_U_Inp I
proof
let o be Object of A;
assume
A1: not thesis;
for s being State of A holds s.o = Exec(I,s).o
proof
let s be State of A;
reconsider so = s.o as Element of Values o by MEMSTR_0:77;
A2: Exec(I,s+*(o,so)) = Exec(I,s) +* (o,so) by A1,Def5;
dom Exec(I,s) = the carrier of A by PARTFUN1:def 2;
hence s.o = (Exec(I,s) +* (o,so)).o by FUNCT_7:31
.= Exec(I,s).o by A2,FUNCT_7:35;
end;
hence contradiction by A1,Def3;
end;
hence thesis by SUBSET_1:2;
end;
theorem
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
proof
let A be with_non_trivial_ObjectKinds IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N, I be Instruction of A;
for o being Object of A holds o in Out_\_Inp I iff o in Output I \ Input
I
proof
let o be Object of A;
hereby
A1: Out_\_Inp I c= Output I by Th3;
assume
A2: o in Out_\_Inp I;
Out_\_Inp I misses Input I by XBOOLE_1:85;
then not o in Input I by A2,XBOOLE_0:3;
hence o in Output I \ Input I by A2,A1,XBOOLE_0:def 5;
end;
assume
A3: o in Output I \ Input I;
then
A4: not o in Input I by XBOOLE_0:def 5;
per cases by A4,XBOOLE_0:def 5;
suppose
A5: not o in Out_U_Inp I;
Output I c= Out_U_Inp I by Th4;
then not o in Output I by A5;
hence thesis by A3,XBOOLE_0:def 5;
end;
suppose
o in Out_\_Inp I;
hence thesis;
end;
end;
hence thesis by SUBSET_1:3;
end;
theorem
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
proof
let A be with_non_trivial_ObjectKinds IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N, I be Instruction of A;
for o being Object of A st o in Out_U_Inp I holds o in Output I \/ Input
I
proof
let o be Object of A such that
A1: o in Out_U_Inp I;
o in Input I or o in Output I
proof
assume
A2: not o in Input I;
per cases by A2,XBOOLE_0:def 5;
suppose
not o in Out_U_Inp I;
hence thesis by A1;
end;
suppose
A3: o in Out_\_Inp I;
Out_\_Inp I c= Output I by Th3;
hence thesis by A3;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
hence Out_U_Inp I c= Output I \/ Input I by SUBSET_1:2;
Output I c= Out_U_Inp I & Input I c= Out_U_Inp I by Th4,XBOOLE_1:36;
hence thesis by XBOOLE_1:8;
end;
theorem Th7:
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
proof
let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
N, I be Instruction of A, o be Object of A such that
A1: Values o is trivial;
assume o in Out_U_Inp I;
then consider s being State of A, a being Element of Values o such that
A2: Exec(I,s+*(o,a)) <> Exec(I,s) +* (o,a) by Def5;
s.o is Element of Values o by MEMSTR_0:77;
then s.o = a by A1,ZFMISC_1:def 10;
then
A3: Exec(I,s+*(o,a)) = Exec(I,s) by FUNCT_7:35;
A4: dom Exec(I,s) = the carrier of A by PARTFUN1:def 2;
A5: for x being object st x in the carrier of A
holds (Exec(I,s) +* (o,a)).x = Exec(I,s).x
proof
let x be object such that
x in the carrier of A;
per cases;
suppose
A6: x = o;
A7: Exec(I,s).o is Element of Values o by MEMSTR_0:77;
thus (Exec(I,s) +* (o,a)).x = a by A4,A6,FUNCT_7:31
.= Exec(I,s).x by A1,A6,A7,ZFMISC_1:def 10;
end;
suppose
x <> o;
hence thesis by FUNCT_7:32;
end;
end;
dom (Exec(I,s) +* (o,a)) = the carrier of A by PARTFUN1:def 2;
hence contradiction by A2,A3,A4,A5,FUNCT_1:2;
end;
theorem
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
proof
let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
N, I be Instruction of A, o be Object of A;
A1: Input I c= Out_U_Inp I by XBOOLE_1:36;
assume Values o is trivial;
hence thesis by A1,Th7;
end;
theorem
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
proof
let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
N, I be Instruction of A, o be Object of A;
assume
A1: Values o is trivial;
Output I c= Out_U_Inp I by Th4;
hence thesis by A1,Th7;
end;
theorem Th10:
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
proof
let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
N, I be Instruction of A;
thus I is halting implies Output I is empty
proof
assume
A1: for s being State of A holds Exec(I,s) = s;
assume not thesis;
then consider o being Object of A such that
A2: o in Output I;
ex s being State of A st s.o <> Exec(I,s).o by A2,Def3;
hence thesis by A1;
end;
assume
A3: Output I is empty;
let s be State of A;
assume
A4: Exec(I,s) <> s;
dom s = the carrier of A & dom Exec(I,s) = the carrier of A
by PARTFUN1:def 2;
then ex x being object st x in the carrier of A & Exec(I,s).x <> s.x by A4,
FUNCT_1:2;
hence contradiction by A3,Def3;
end;
theorem Th11:
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
proof
let A be with_non_trivial_ObjectKinds IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N, I be Instruction of A such that
A1: I is halting;
Out_\_Inp I c= Output I by Th3;
then Out_\_Inp I c= {} by A1,Th10;
hence thesis;
end;
theorem Th12:
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
proof
let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
N, I be Instruction of A such that
A1: for s being State of A holds Exec(I,s) = s;
assume not thesis;
then consider o being Object of A such that
A2: o in Out_U_Inp I;
consider s being State of A, a being Element of Values o such that
A3: Exec(I,s+*(o,a)) <> Exec(I,s) +* (o,a) by A2,Def5;
Exec(I,s+*(o,a)) = s+*(o,a) by A1
.= Exec(I,s) +* (o,a) by A1;
hence thesis by A3;
end;
theorem Th13:
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
proof
let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
N, I be Instruction of A;
assume I is halting;
then Input I = {} \ Out_\_Inp I by Th12
.= {};
hence thesis;
end;
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;
coherence by Th13;
cluster Output I -> empty;
coherence by Th10;
cluster Out_U_Inp I -> empty;
coherence by Th12;
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;
existence
proof
take STC N;
thus thesis;
end;
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;
coherence by Th11;
end;
registration
let N;
cluster with_non_trivial_Instructions
IC-Ins-separated
for non empty with_non-empty_values AMI-Struct over N;
existence
proof
take STC N;
thus thesis;
end;
end;
theorem
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
proof
let A be standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N, I be Instruction of A;
set t = the State of A;
set l = IC A;
reconsider sICt = IC t + 1 as Element of NAT;
reconsider w = sICt as Element of Values l by MEMSTR_0:def 6;
set s = t +* (l,w);
assume for s being State of A holds Exec(I,s).IC A = IC s + 1;
then
A1: Exec(I,t).l = IC t + 1 & Exec(I,s).l = IC s + 1;
dom t = the carrier of A by PARTFUN1:def 2;
then s.l = w by FUNCT_7:31;
then Exec(I,t) <> Exec(I,s) by A1,NAT_1:16;
hence thesis by Def4;
end;
theorem
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 by Def3;
registration
let N;
cluster standard for IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
existence
proof
take STC N;
thus thesis;
end;
end;
theorem
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
proof
let A be standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N, I be Instruction of A such that
A1: for s being State of A holds Exec(I, s).IC A = IC s + 1;
set s = the State of A;
Exec(I,s).IC A = IC s + 1 by A1;
then Exec(I,s).IC A <> IC s by NAT_1:16;
hence thesis by Def3;
end;
theorem Th17:
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
proof
let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
N, I be Instruction of A;
assume ex s being State of A st Exec(I,s).IC A <> IC s;
then
A1: IC A in Output I by Def3;
Output I c= Out_U_Inp I by Th4;
hence thesis by A1;
end;
theorem
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
proof
let A be standard IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N, I be Instruction of A;
set s = the State of A;
assume for s being State of A holds Exec(I,s).IC A = IC s + 1;
then Exec(I,s).IC A = IC s + 1;
then Exec(I,s).IC A <> IC s by NAT_1:16;
hence thesis by Th17;
end;
theorem
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
proof
let A be IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N, I be Instruction of A,
o be Object of A;
assume
A1: for s being State of A, o being Object of A, J being Instruction of
A st InsCode I = InsCode J & o in Data-Locations A holds Exec(J,s).o = s.o;
assume o in Output I;
then ex s being State of A st s.o <> Exec(I,s).o by Def3;
then
A2: not o in Data-Locations A by A1;
o in the carrier of A;
then o in {IC A} \/ Data-Locations A by STRUCT_0:4;
then o in {IC A} by A2,XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;