Tableau Examples

As a sanity check we construct tableaux/proofs for some examples.

def atP : ℕ

Equations

• atP = 1

def atQ : ℕ

Equations

• atQ = 2

def atR : ℕ

Equations

• atR = 3

def atA : ℕ

Equations

• atA = 4

@[reducible, inline]

abbrev p : Formula

Equations

• p = ·atP

@[reducible, inline]

abbrev q : Formula

Equations

• q = ·atQ

@[reducible, inline]

abbrev r : Formula

Equations

• r = ·atR

@[reducible, inline]

abbrev a : Program

Equations

• a = ·atA

def subTabForEx2 : Tableau [([r⋀(~⌈a⌉p), ~ r⋀(~⌈a⌉p⋀q)], [], none)] ([r, ~⌈a⌉p, ⌈a⌉p⋀q], [], none)

Preparation for Example 2 from MB.

Equations

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

theorem endNodesOf_cast_helper {X Y : Sequent} {h : X = Y} (ltX : LocalTableau X) : endNodesOf (h ▸ ltX) = endNodesOf ltX