Step
*
of Lemma
sp-meet-join-distrib
∀[x,y,z:Sierpinski]. (x ∨ y ∧ z = x ∧ z ∨ y ∧ z ∈ Sierpinski)
BY
{ TACTIC:(Auto
THEN (BLemma `Sierpinski-equal2` THENA Auto)
THEN (RWO "sp-meet-is-top" 0 THENA Auto)
THEN (RWO "Sierpinski-equal" 0 THENA Auto)
THEN (RWO "sp-join-is-bottom" 0 THENA Auto)) }
1
1. x : Sierpinski
2. y : Sierpinski
3. z : Sierpinski
⊢ ((x = ⊥ ∈ Sierpinski) ∧ (y = ⊥ ∈ Sierpinski)
⇐⇒ ⊤ = ⊥ ∈ Sierpinski) ∧ (z = ⊥ ∈ Sierpinski
⇐⇒ ⊤ = ⊥ ∈ Sierpinski)
⇐⇒ (x ∧ z = ⊥ ∈ Sierpinski) ∧ (y ∧ z = ⊥ ∈ Sierpinski)
⇐⇒ ⊤ = ⊥ ∈ Sierpinski
Latex:
Latex:
\mforall{}[x,y,z:Sierpinski]. (x \mvee{} y \mwedge{} z = x \mwedge{} z \mvee{} y \mwedge{} z)
By
Latex:
TACTIC:(Auto
THEN (BLemma `Sierpinski-equal2` THENA Auto)
THEN (RWO "sp-meet-is-top" 0 THENA Auto)
THEN (RWO "Sierpinski-equal" 0 THENA Auto)
THEN (RWO "sp-join-is-bottom" 0 THENA Auto))
Home
Index