---

Step * 1 1 of Lemma peval-pnegate


1. x1 : formula()
2. v : {a:formula()| a ⊆ pnot(x1) ∧ (↑pvar?(a))}  ⟶ 𝔹
3. peval(v;pnegate(x1)) = ¬bpeval(v;x1)
⊢ peval(v;x1) = ¬b¬bpeval(v;x1)
BY
{ xxx(AutoBoolCase ⌜peval(v;x1)⌝⋅
      THEN Auto
      THEN DoSubsume
      THEN Auto
      THEN SubtypeReasoning
      THEN Auto
      THEN (Unfold `psub` 0 THEN Reduce 0 THEN Fold `psub` 0 THEN Auto)⋅)xxx }

---

Latex:

---

Latex:

1.  x1  :  formula()
2.  v  :  \{a:formula()|  a  \msubseteq{}  pnot(x1)  \mwedge{}  (\muparrow{}pvar?(a))\}    {}\mrightarrow{}  \mBbbB{}
3.  peval(v;pnegate(x1))  =  \mneg{}\msubb{}peval(v;x1)
\mvdash{}  peval(v;x1)  =  \mneg{}\msubb{}\mneg{}\msubb{}peval(v;x1)


By

---

Latex:
xxx(AutoBoolCase  \mkleeneopen{}peval(v;x1)\mkleeneclose{}\mcdot{}
        THEN  Auto
        THEN  DoSubsume
        THEN  Auto
        THEN  SubtypeReasoning
        THEN  Auto
        THEN  (Unfold  `psub`  0  THEN  Reduce  0  THEN  Fold  `psub`  0  THEN  Auto)\mcdot{})xxx

---

Home Index