theorem noBot : Provable (~⊥)

theorem noContradiction : Provable (~(p⋀~p))

def subTabForEx2 : ClosedTableau ({·'r', ~(□p), □(p⋀q)}, ∅)

Equations

• One or more equations did not get rendered due to their size.

def termR : Lean.ParserDescr

Equations

• termR = Lean.ParserDescr.node `termR 1024 (Lean.ParserDescr.symbol "r")