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 Output 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 Output I
let I be Instruction of A; :: thesis: for o being Object of A st Values o is trivial holds
not o in Output I
let o be Object of A; :: thesis: ( Values o is trivial implies not o in Output I )
assume A1: Values o is trivial ; :: thesis: not o in Output I
Output I c= Out_U_Inp I by Th4;
hence not o in Output I by A1, Th7; :: thesis: verum