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