let N be with_zero set ; :: thesis: for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N
for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I)
let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N; :: thesis: for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I)
let I be Instruction of A; :: thesis: Out_\_Inp I = (Output I) \ (Input I)
for o being Object of A holds
( o in Out_\_Inp I iff o in (Output I) \ (Input I) )
proof
let o be Object of A; :: thesis: ( o in Out_\_Inp I iff o in (Output I) \ (Input I) )
hereby :: thesis: ( o in (Output I) \ (Input I) implies o in Out_\_Inp I )
A1: Out_\_Inp I c= Output I by Th3;
assume A2: o in Out_\_Inp I ; :: thesis: o in (Output I) \ (Input I)
Out_\_Inp I misses Input I by XBOOLE_1:85;
then not o in Input I by A2, XBOOLE_0:3;
hence o in (Output I) \ (Input I) by A2, A1, XBOOLE_0:def 5; :: thesis: verum
end;
assume A3: o in (Output I) \ (Input I) ; :: thesis: o in Out_\_Inp I
then A4: not o in Input I by XBOOLE_0:def 5;
per cases ( not o in Out_U_Inp I or o in Out_\_Inp I ) by A4, XBOOLE_0:def 5;
end;
end;
hence Out_\_Inp I = (Output I) \ (Input I) by SUBSET_1:3; :: thesis: verum