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
for o being Object of A st ObjectKind o is trivial holds
not o in Input 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
for o being Object of A st ObjectKind o is trivial holds
not o in Input I
let A be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N; :: thesis: for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Input I
let I be Instruction of A; :: thesis: for o being Object of A st ObjectKind o is trivial holds
not o in Input I
let o be Object of A; :: thesis: ( ObjectKind o is trivial implies not o in Input I )
assume A1: ObjectKind o is trivial ; :: thesis: not o in Input I
Input I c= Out_U_Inp I by XBOOLE_1:36;
hence not o in Input I by A1, Th15; :: thesis: verum