---

Step * of Lemma peval-pnegate

∀[x:formula()]. ∀[v:{a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹].  peval(v;pnegate(x)) = ¬bpeval(v;x)
BY
{ xxx((D 0 THENA Auto)
      THEN SimpleDatatypeInduction (-1)
      THEN Auto
      THEN ∀h:hyp. ((InstHyp [⌜v⌝] h⋅ THENM Thin h)
                    THENA (DoSubsume
                           THEN Auto
                           THEN SubtypeReasoning
                           THEN Auto
                           THEN (Unfold `psub` 0 THEN Reduce 0 THEN Fold `psub` 0 THEN Auto)⋅)
                    ) 
      THEN RepUR ``pnegate`` 0
      THEN Try (Fold `pnegate` 0)
      THEN Try ((((RWO "peval-unroll" 0
                   THENM RW (SweepUpC UnrollRecursionC) 0
                   THENM Reduce 0
                   THENM RWO "peval-unroll<" 0)
                  THENA Auto
                  )
                 THEN RepUR ``extend-val`` 0
                 THEN HypSubst' (-2) 0
                 THEN HypSubst' (-1) 0
                 THEN Auto
                 THEN AutoBoolCase ⌜peval(v;left)⌝⋅
                 THEN Auto
                 THEN DoSubsume
                 THEN Auto
                 THEN SubtypeReasoning
                 THEN Auto
                 THEN (Unfold `psub` 0 THEN Reduce 0 THEN Fold `psub` 0 THEN Auto)⋅)))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) = ¬bpeval(v;pnot(x1))

---

Latex:

---

Latex:
\mforall{}[x:formula()].  \mforall{}[v:\{a:formula()|  a  \msubseteq{}  x  \mwedge{}  (\muparrow{}pvar?(a))\}    {}\mrightarrow{}  \mBbbB{}].    peval(v;pnegate(x))  =  \mneg{}\msubb{}peval(v;x)


By

---

Latex:
xxx((D  0  THENA  Auto)
        THEN  SimpleDatatypeInduction  (-1)
        THEN  Auto
        THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}v\mkleeneclose{}]  h\mcdot{}  THENM  Thin  h)
                                    THENA  (DoSubsume
                                                  THEN  Auto
                                                  THEN  SubtypeReasoning
                                                  THEN  Auto
                                                  THEN  (Unfold  `psub`  0  THEN  Reduce  0  THEN  Fold  `psub`  0  THEN  Auto)\mcdot{})
                                    ) 
        THEN  RepUR  ``pnegate``  0
        THEN  Try  (Fold  `pnegate`  0)
        THEN  Try  ((((RWO  "peval-unroll"  0
                                  THENM  RW  (SweepUpC  UnrollRecursionC)  0
                                  THENM  Reduce  0
                                  THENM  RWO  "peval-unroll<"  0)
                                THENA  Auto
                                )
                              THEN  RepUR  ``extend-val``  0
                              THEN  HypSubst'  (-2)  0
                              THEN  HypSubst'  (-1)  0
                              THEN  Auto
                              THEN  AutoBoolCase  \mkleeneopen{}peval(v;left)\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