let N be with_zero set ; :: thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A
for o being Object of A st Values o is trivial holds
not o in Out_U_Inp I
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for I being Instruction of A
for o being Object of A st Values o is trivial holds
not o in Out_U_Inp I
let I be Instruction of A; :: thesis: for o being Object of A st Values o is trivial holds
not o in Out_U_Inp I
let o be Object of A; :: thesis: ( Values o is trivial implies not o in Out_U_Inp I )
assume A1: Values o is trivial ; :: thesis: not o in Out_U_Inp I
assume o in Out_U_Inp I ; :: thesis: contradiction
then consider s being State of A, a being Element of Values o such that
A2: Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) by Def5;
s . o is Element of Values o by MEMSTR_0:77;
then s . o = a by A1, ZFMISC_1:def 10;
then A3: Exec (I,(s +* (o,a))) = Exec (I,s) by FUNCT_7:35;
A4: dom (Exec (I,s)) = the carrier of A by PARTFUN1:def 2;
A5: for x being object st x in the carrier of A holds
((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x
proof
let x be object ; :: thesis: ( x in the carrier of A implies ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x )
assume x in the carrier of A ; :: thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x
per cases ( x = o or x <> o ) ;
suppose A6: x = o ; :: thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x
A7: (Exec (I,s)) . o is Element of Values o by MEMSTR_0:77;
thus ((Exec (I,s)) +* (o,a)) . x = a by A4, A6, FUNCT_7:31
.= (Exec (I,s)) . x by A1, A6, A7, ZFMISC_1:def 10 ; :: thesis: verum
end;
suppose x <> o ; :: thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x
hence ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x by FUNCT_7:32; :: thesis: verum
end;
end;
end;
dom ((Exec (I,s)) +* (o,a)) = the carrier of A by PARTFUN1:def 2;
hence contradiction by A2, A3, A4, A5, FUNCT_1:2; :: thesis: verum