---

Step * 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) = ¬bpeval(v;pnot(x1))
BY
{ xxx((RW  (AddrC [3;1] (LemmaC `peval-unroll`)) 0⋅ THENA Auto)
      THEN (RW (SweepUpC UnrollRecursionC) 0
            THENM Reduce 0
            THENM ((RWO "peval-unroll<" 0 THENA Auto) THEN RepUR ``extend-val`` 0))
      )xxx }

1
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)

---

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{}peval(v;pnot(x1))


By

---

Latex:
xxx((RW    (AddrC  [3;1]  (LemmaC  `peval-unroll`))  0\mcdot{}  THENA  Auto)
        THEN  (RW  (SweepUpC  UnrollRecursionC)  0
                    THENM  Reduce  0
                    THENM  ((RWO  "peval-unroll<"  0  THENA  Auto)  THEN  RepUR  ``extend-val``  0))
        )xxx

---

Home Index