Closed olaure01 closed 3 years ago
Reducing the top-most cut to the left generates error:
"Bad request: invalid proof: Premises conclusion do not match expected premises conclusion after applying rule {\"rule\":\"tensor\",\"formulaPosition\":3}}"
https://ccll.linear-logic.org/?s=N&n=N%2C%21%28X-oX%29-o%21%28X-oX%29&proof_transformation=1&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJRzl9eyXig67oHQyYTslN0vePncDNqmC0%2BGDWpnpdCAR6c9SAGSHm%2BINkWc8IfafrwTqc8V8eb49BHr9D2VBF1BL%2BKEgEsR74aISfi5GhXrx%2B6qjsOHwacUkK%2Fz0Q5qzdB9zzMd5o6kYl20dBjYWgaRm%2BvbctQ%2Bq5EIJXnXnUlfna%2FzGbTT7YbqJLDG8QAninjet678FVKxTkbkY%2FdOzc%2BoNNKACNJC1e%2FEMbJ0fXP8exnNqMPhp62OzCG4haAUVgCRwkUrP4BtWexCzRXZ%2Fl1NXvhFn5fiKCe3lAhVlm%2Betbq7ezMafVqfwKij1VX28bDMWFHSHZRmNQDFwiL7NWsxx9%2BWT72R3qYBGuejU81yaD8cpQ0tNgdUggX8dtfK7sIrttV3%2BfOAUrL2%2F2gsEMSr4F2THofhLDK0z4ty3Lakc0pT3i3Vz26IKPx4CsJYP6PxhbG407X0JadwMcbCIhCUEnb4hkl6r3CI0kwF2aGCNWmGs%2FjFCLdbRt0UTe9N2BHrBkuYhNIzJacNt57hd8MsYdfxpxKsdKQS%2BJ7lbLHq0bBcDwjJgkUDbU9%2BLGiZLSvAy%2F8R%2FzvzDVJ8CtCFuVX8vGHq%2Fnx4MMrFvHuYzFLJIKWqWPhpmCo7aDn29h6C2ocMkR2O6uRwU62KrJsYgwybTPH%2F%2FfPgK%2B17b%2Bu1GYneokeDpccoNLdqXpHtTbO%2FHVA4EZpLAsVxOAhnJEHalw%2F4s01LxvE9dlLniJwYtc7xviWhxVUo9n6R%2FkHwhvombBJyZ8p16PizU2vEiLRIPApqtE%2BCG6LBCGEuesS4HsM5TOjkV6msfmZKWsmT1a5S%2BXbFXw25WQttUYKnkxfdxoblcgQQ5viHJyIL4xY%2B40FbV8c45v5Ub1ewpH6fUJz%2F7WyppW0QAaSgfOiorkltC2il35rM1hCKN%2B3wM3mpYqKTZtc4vmJ6XxxHOQ852bzisligfqPOdR5V2QEO%2FPtj%2BpqhurYD6zgBEF8QKifbjUvI26g9kjQpW16%2B%2B77a79LiF3vn8aVV9nJTWjwf6aV0Pst728oB%2FvXoDg%3D%3D
Reducing the top-most cut to the left generates error:
https://ccll.linear-logic.org/?s=N&n=N%2C%21%28X-oX%29-o%21%28X-oX%29&proof_transformation=1&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJRzl9eyXig67oHQyYTslN0vePncDNqmC0%2BGDWpnpdCAR6c9SAGSHm%2BINkWc8IfafrwTqc8V8eb49BHr9D2VBF1BL%2BKEgEsR74aISfi5GhXrx%2B6qjsOHwacUkK%2Fz0Q5qzdB9zzMd5o6kYl20dBjYWgaRm%2BvbctQ%2Bq5EIJXnXnUlfna%2FzGbTT7YbqJLDG8QAninjet678FVKxTkbkY%2FdOzc%2BoNNKACNJC1e%2FEMbJ0fXP8exnNqMPhp62OzCG4haAUVgCRwkUrP4BtWexCzRXZ%2Fl1NXvhFn5fiKCe3lAhVlm%2Betbq7ezMafVqfwKij1VX28bDMWFHSHZRmNQDFwiL7NWsxx9%2BWT72R3qYBGuejU81yaD8cpQ0tNgdUggX8dtfK7sIrttV3%2BfOAUrL2%2F2gsEMSr4F2THofhLDK0z4ty3Lakc0pT3i3Vz26IKPx4CsJYP6PxhbG407X0JadwMcbCIhCUEnb4hkl6r3CI0kwF2aGCNWmGs%2FjFCLdbRt0UTe9N2BHrBkuYhNIzJacNt57hd8MsYdfxpxKsdKQS%2BJ7lbLHq0bBcDwjJgkUDbU9%2BLGiZLSvAy%2F8R%2FzvzDVJ8CtCFuVX8vGHq%2Fnx4MMrFvHuYzFLJIKWqWPhpmCo7aDn29h6C2ocMkR2O6uRwU62KrJsYgwybTPH%2F%2FfPgK%2B17b%2Bu1GYneokeDpccoNLdqXpHtTbO%2FHVA4EZpLAsVxOAhnJEHalw%2F4s01LxvE9dlLniJwYtc7xviWhxVUo9n6R%2FkHwhvombBJyZ8p16PizU2vEiLRIPApqtE%2BCG6LBCGEuesS4HsM5TOjkV6msfmZKWsmT1a5S%2BXbFXw25WQttUYKnkxfdxoblcgQQ5viHJyIL4xY%2B40FbV8c45v5Ub1ewpH6fUJz%2F7WyppW0QAaSgfOiorkltC2il35rM1hCKN%2B3wM3mpYqKTZtc4vmJ6XxxHOQ852bzisligfqPOdR5V2QEO%2FPtj%2BpqhurYD6zgBEF8QKifbjUvI26g9kjQpW16%2B%2B77a79LiF3vn8aVV9nJTWjwf6aV0Pst728oB%2FvXoDg%3D%3D