ComputerAidedLL / click-and-collect

A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml
GNU Lesser General Public License v2.1
17 stars 2 forks source link

Technical Error #170

Open Nick-Munnich opened 2 years ago

Nick-Munnich commented 2 years ago

https://click-and-collect.linear-logic.org/?s=%E2%8A%A2+%CE%93%2C+A%E2%8A%97B%2C+%CE%94%2C+C%E2%8A%97D%2C+%CE%A3&proofTransformation=1&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJRzl9eyXig67oHQyYTsldG6YZbhWWsYD%2Bm1Ufjzjq9ksYKzro5MROgUqT%2FImzIdJCz9y6kbhiXXSyLrQ2CPzaAY7yKRtfYfgqaIudpaEMyZjOszausXhdoJ%2Bv2lvAHARxDM8eCyrw0sE2n1aAnWopmHp9A52tsxPtcqjKhYhr8WjXFyQi4MJapewiKkrqZANvZbHM7g9k8WuifhCHDIYN4QJB58CT0R7IdcehTEGvQAfQdUh31rCLptOZRC%2F%2BAuwSIwGajCI4tNL19nxph3uHOYlEAOMlaGcHSL2cNmG9JGUtVTrK2AJJwxQ6oDmnwmg5U38OU1mT6V1KwBGXj8if0RIQ1BGdlogUm8PvtpCvozp4Vh%2FUgiASu5U2xyssKb1ET1V0eKr%2FShgcnfFKrazVzh2x3fUyAh2tXPVQuq6hvc%2F8WG4lo%3D

In this proof, if you commute the bottom cut left a technical error appears