theorem mytaut1 (p : Char) : Tautology ((·p)↣·p)

theorem mytaut2 (p : Char) : Tautology ((~~·p)↣·p)

def myModel : KripkeModel ℕ

Equations

• myModel = { val := fun (x : ℕ) (x : Char) => True, Rel := fun (x v : ℕ) => HEq v 1 }

theorem mysat (p : Char) : HasSat.Satisfiable (·p)

theorem boxTop : Tautology (□⊤)

theorem A3 (X Y : Formula) : Tautology (□(X⋀Y)↣□X⋀□Y)