let N be with_zero set ; for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A holds Output I c= Out_U_Inp I
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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
Values o by MEMSTR_0:77;
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 2;
hence s . o =
((Exec (I,s)) +* (o,so)) . o
by FUNCT_7:31
.=
(Exec (I,s)) . o
by A2, FUNCT_7:35
;
verum
end;
hence
contradiction
by A1, Def3;
verum
end;
hence
Output I c= Out_U_Inp I
by SUBSET_1:2; verum