Re: CoS and computability logic

>No. The case with two pidgeons is
>
>   [ ( [ a, b] , [ c, d] , [ e, f] ) ,
>     ( [-a, g] , [-c, h] , [-e, k] ) ,
>     ( [-b,-g] , [-d,-h] , [-f,-k] ) ]
>
>which can be done without contraction via medial.

No Lutz, this formula looks falsifiable to me, the case with two 
pigeons should be

    [ ( [ a, b] , [ c, d] ) ,
      ( [-a, e] , [-c, f] ) ,
      ( [-b,-e] , [-d,-f] ) ] .

I couldn't quickly find a proof inside BKS, can you show one?

-Alessio