let N be non empty with_non-empty_elements set ; for A being non empty stored-program IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N
for I being Instruction of A holds Out_\_Inp I c= Output I
let A be non empty stored-program IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N; for I being Instruction of A holds Out_\_Inp I c= Output I
let I be Instruction of A; Out_\_Inp I c= Output I
for o being Object of A st o in Out_\_Inp I holds
o in Output I
proof
let o be
Object of
A;
( o in Out_\_Inp I implies o in Output I )
consider s being
State of
A,
a being
Element of
ObjectKind o;
consider w being
set such that A1:
w in ObjectKind o
and A2:
w <> a
by YELLOW15:4;
reconsider w =
w as
Element of
ObjectKind o by A1;
set t =
s +* (
o,
w);
A3:
dom (s +* (o,w)) = the
carrier of
A
by PARTFUN1:def 4;
A4:
dom s = the
carrier of
A
by PARTFUN1:def 4;
assume A5:
(
o in Out_\_Inp I & not
o in Output I )
;
contradiction
then A6:
(Exec (I,((s +* (o,w)) +* (o,a)))) . o =
((s +* (o,w)) +* (o,a)) . o
by Def3
.=
a
by A3, FUNCT_7:33
;
(Exec (I,(s +* (o,w)))) . o =
(s +* (o,w)) . o
by A5, Def3
.=
w
by A4, FUNCT_7:33
;
hence
contradiction
by A5, A2, A6, Def4;
verum
end;
hence
Out_\_Inp I c= Output I
by SUBSET_1:7; verum