---

Step * of Lemma Wless-Wadd

∀[A:Type]. ∀[B:A ⟶ Type].
  ∀zero:A ⟶ 𝔹. ((∀a:A. (¬↑(zero a) ⇐⇒ B[a])) ⇒ (∀w3,w2,w1:W(A;a.B[a]).  ((w2 <  w3) ⇒ ((w1 + w2) <  (w1 + w3)))))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN RepeatFor 2 (UseWInductionLemma)
   THEN Auto
   THEN RepeatFor 2 (ReduceWcmp (-1))
   THEN D -1
   THEN (RecUnfold `Wadd` 0
         THEN Unfold `Wsup` 0
         THEN Reduce 0
         THEN Fold `Wsup` 0
         THEN RepeatFor 2 (AutoSplit)
         THEN Try ((ReduceWcmp 0 THEN With ⌜x⌝ (D 0)⋅ THEN Auto))⋅
         THEN Try ((ReduceWcmp 0⋅ THEN Auto))
         THEN Try ((BLemma `Wleq-Wadd3` THEN Auto))
         THEN Try (OnMaybeHyp 14 (\h. (FHyp 4 [h] THEN Complete (Auto)))))⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}zero:A  {}\mrightarrow{}  \mBbbB{}
        ((\mforall{}a:A.  (\mneg{}\muparrow{}(zero  a)  \mLeftarrow{}{}\mRightarrow{}  B[a]))
        {}\mRightarrow{}  (\mforall{}w3,w2,w1:W(A;a.B[a]).    ((w2  <    w3)  {}\mRightarrow{}  ((w1  +  w2)  <    (w1  +  w3)))))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  RepeatFor  2  (UseWInductionLemma)
  THEN  Auto
  THEN  RepeatFor  2  (ReduceWcmp  (-1))
  THEN  D  -1
  THEN  (RecUnfold  `Wadd`  0
              THEN  Unfold  `Wsup`  0
              THEN  Reduce  0
              THEN  Fold  `Wsup`  0
              THEN  RepeatFor  2  (AutoSplit)
              THEN  Try  ((ReduceWcmp  0  THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))\mcdot{}
              THEN  Try  ((ReduceWcmp  0\mcdot{}  THEN  Auto))
              THEN  Try  ((BLemma  `Wleq-Wadd3`  THEN  Auto))
              THEN  Try  (OnMaybeHyp  14  (\mbackslash{}h.  (FHyp  4  [h]  THEN  Complete  (Auto)))))\mcdot{})

---

Home Index