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