let N be non empty with_non-empty_elements set ; for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A holds Output I c= Out_U_Inp I
let A be non empty stored-program IC-Ins-separated definite AMI-Struct of N; for I being Instruction of A holds Output I c= Out_U_Inp I
let I be Instruction of A; Output I c= Out_U_Inp I
for o being Object of A st o in Output I holds
o in Out_U_Inp I
proof
let o be
Object of
A;
( o in Output I implies o in Out_U_Inp I )
assume A1:
(
o in Output I & not
o in Out_U_Inp I )
;
contradiction
for
s being
State of
A holds
s . o = (Exec I,s) . o
proof
let s be
State of
A;
s . o = (Exec I,s) . o
reconsider so =
s . o as
Element of
ObjectKind o by Th2;
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 4;
hence s . o =
((Exec I,s) +* o,so) . o
by FUNCT_7:33
.=
(Exec I,s) . o
by A2, FUNCT_7:37
;
verum
end;
hence
contradiction
by A1, Def3;
verum
end;
hence
Output I c= Out_U_Inp I
by SUBSET_1:7; verum