let N be non empty with_non-empty_elements set ; for A being non empty IC-Ins-separated 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 IC-Ins-separated 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 )
set s = the
State of
A;
set a = the
Element of
ObjectKind o;
consider w being
set such that A1:
w in ObjectKind o
and A2:
w <> the
Element of
ObjectKind o
by YELLOW15:3;
reconsider w =
w as
Element of
ObjectKind o by A1;
set t = the
State of
A +* (
o,
w);
A3:
dom ( the State of A +* (o,w)) = the
carrier of
A
by PARTFUN1:def 2;
A4:
dom the
State of
A = the
carrier of
A
by PARTFUN1:def 2;
assume A5:
(
o in Out_\_Inp I & not
o in Output I )
;
contradiction
then A6:
(Exec (I,(( the State of A +* (o,w)) +* (o, the Element of ObjectKind o)))) . o =
(( the State of A +* (o,w)) +* (o, the Element of ObjectKind o)) . o
by Def3
.=
the
Element of
ObjectKind o
by A3, FUNCT_7:31
;
(Exec (I,( the State of A +* (o,w)))) . o =
( the State of A +* (o,w)) . o
by A5, Def3
.=
w
by A4, FUNCT_7:31
;
hence
contradiction
by A5, A2, A6, Def4;
verum
end;
hence
Out_\_Inp I c= Output I
by SUBSET_1:2; verum