parameter (ticket nat) ;
storage unit;
code
  { CAR ;
    PUSH (pair nat nat) (Pair 1 2) ; SWAP;
    SPLIT_TICKET; ASSERT_SOME; UNPAIR;
    READ_TICKET; CDDR; PUSH nat 1; ASSERT_CMPEQ;
    DROP;
    READ_TICKET; CDDR; PUSH nat 2; ASSERT_CMPEQ;
    DROP;
    UNIT ; NIL operation ; PAIR } ;