---

Step * of Lemma add-sz_wf

∀[P:Type]. ∀[X:P ⟶ Type]. ∀[sz:i:P ⟶ (X i) ⟶ partial(ℕ)]. ∀[L:(P + P + Type) List].
∀[x:tuple-type(map(λx.case x of inl(y) => case y of inl(p) => X p | inr(p) => (X p) List | inr(E) => E;L))].
  (add-sz(sz;L;x) ∈ partial(ℕ))
BY
{ (Auto
   THEN Unfold `add-sz` 0
   THEN BLemma `tuple-sum-wf-partial`
   THEN Reduce 0
   THEN (((FunExt THENA Auto)
          THEN ((DProdsAndUnions THEN Reduce 0)
                THENL [Auto; ((FunExt THENA Auto) THEN Reduce 0 THEN BLemma `l_sum-wf-partial-nat` THEN Auto); Auto]
               )
          )
   ORELSE Auto
   )) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[X:P  {}\mrightarrow{}  Type].  \mforall{}[sz:i:P  {}\mrightarrow{}  (X  i)  {}\mrightarrow{}  partial(\mBbbN{})].  \mforall{}[L:(P  +  P  +  Type)  List].
\mforall{}[x:tuple-type(map(\mlambda{}x.case  x
                                              of  inl(y)  =>
                                              case  y  of  inl(p)  =>  X  p  |  inr(p)  =>  (X  p)  List
                                              |  inr(E)  =>
                                              E;L))].
    (add-sz(sz;L;x)  \mmember{}  partial(\mBbbN{}))


By

---

Latex:
(Auto
  THEN  Unfold  `add-sz`  0
  THEN  BLemma  `tuple-sum-wf-partial`
  THEN  Reduce  0
  THEN  (((FunExt  THENA  Auto)
                THEN  ((DProdsAndUnions  THEN  Reduce  0)
                            THENL  [Auto
                                        ;  ((FunExt  THENA  Auto)
                                              THEN  Reduce  0
                                              THEN  BLemma  `l\_sum-wf-partial-nat`
                                              THEN  Auto)
                                        ;  Auto]
                          )
                )
  ORELSE  Auto
  ))

---

Home Index