consider p being FinSeqLen of 1;
consider f being Function of (1 -tuples_on BOOLEAN),BOOLEAN;
take 1GateCircStr (p,f) ; :: thesis: ( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity & 1GateCircStr (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2isBoolean & not 1GateCircStr (p,f) is void & 1GateCircStr (p,f) is strict )
thus ( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity & 1GateCircStr (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2isBoolean & not 1GateCircStr (p,f) is void & 1GateCircStr (p,f) is strict ) ; :: thesis: verum