| "STRICT" :: "ORDER" :: tl -> k T.OK ("ORDER" :: "STRICT" :: outs) tl
| "ORDER" :: tl -> k T.OK ("ORDER" :: outs) tl
| "MAXIMUM" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
| "STRICT" :: "ORDER" :: tl -> k T.OK ("ORDER" :: "STRICT" :: outs) tl
| "ORDER" :: tl -> k T.OK ("ORDER" :: outs) tl
| "MAXIMUM" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
| "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl
| "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl
| "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl
| "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl
| "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl
| "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl
| "PREDECESSOR" :: tl -> k T.OK ("PREDECESSOR" :: outs) tl
| "SUCCESSOR" :: tl -> k T.OK ("SUCCESSOR" :: outs) tl
| "NAT-INJECTION" :: tl -> k T.OK ("NAT-INJECTION" :: outs) tl
| "PREDECESSOR" :: tl -> k T.OK ("PREDECESSOR" :: outs) tl
| "SUCCESSOR" :: tl -> k T.OK ("SUCCESSOR" :: outs) tl
| "NAT-INJECTION" :: tl -> k T.OK ("NAT-INJECTION" :: outs) tl