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