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