let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Output I
let A be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Output I
let I be Instruction of A; :: thesis: for o being Object of A st ObjectKind o is trivial holds
not o in Output I
let o be Object of A; :: thesis: ( ObjectKind o is trivial implies not o in Output I )
assume A1: ObjectKind o is trivial ; :: thesis: not o in Output I
Output I c= Out_U_Inp I by Th11;
hence not o in Output I by A1, Th15; :: thesis: verum