⨯
Derivation rules
{"s":{"cons":[{"t":"litt","v":"A"},{"t":"dual","v":{"t":"litt","v":"A"}}]},"ar":{"rr":{"r":"axiom"},"p":[]}}
{"s":{"cons":[{"t":"one"}]},"ar":{"rr":{"r":"one"},"p":[]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"bottom"},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"bottom","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"Δ"}]},"ar":null}]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"top"},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"top","fp":1},"p":[]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"tensor","v1":{"t":"litt","v":"A"},"v2":{"t":"litt","v":"B"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"tensor","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"}]},"ar":null},{"s":{"cons":[{"t":"litt","v":"B"},{"t":"litt","v":"Δ"}]},"ar":null}]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"par","v1":{"t":"litt","v":"A"},"v2":{"t":"litt","v":"B"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"par","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"},{"t":"litt","v":"B"},{"t":"litt","v":"Δ"}]},"ar":null}]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"with","v1":{"t":"litt","v":"A"},"v2":{"t":"litt","v":"B"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"with","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"},{"t":"litt","v":"Δ"}]},"ar":null},{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"B"},{"t":"litt","v":"Δ"}]},"ar":null}]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"plus","v1":{"t":"litt","v":"A"},"v2":{"t":"litt","v":"B"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"plus_left","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"},{"t":"litt","v":"Δ"}]},"ar":null}]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"plus","v1":{"t":"litt","v":"A"},"v2":{"t":"litt","v":"B"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"plus_right","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"B"},{"t":"litt","v":"Δ"}]},"ar":null}]}}
{"s":{"cons":[{"t":"whynot","v":{"t":"litt","v":"Γ"}},{"t":"ofcourse","v":{"t":"litt","v":"A"}},{"t":"whynot","v":{"t":"litt","v":"Δ"}}]},"ar":{"rr":{"r":"promotion","fp":1},"p":[{"s":{"cons":[{"t":"whynot","v":{"t":"litt","v":"Γ"}},{"t":"litt","v":"A"},{"t":"whynot","v":{"t":"litt","v":"Δ"}}]},"ar":null}]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"weakening","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"Δ"}]},"ar":null}]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"dereliction","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"},{"t":"litt","v":"Δ"}]},"ar":null}]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"contraction","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"litt","v":"Δ"}]},"ar":null}]}}
{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"cut","formula":{"t":"litt","v":"A"},"fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"}]},"ar":null},{"s":{"cons":[{"t":"dual","v":{"t":"litt","v":"A"}},{"t":"litt","v":"Δ"}]},"ar":null}]}}