---

Step * of Lemma concat-lifting-3_wf

∀[A,B,C,D:Type]. ∀[f:A ⟶ B ⟶ C ⟶ bag(D)].  (concat-lifting-3(f) ∈ bag(A) ⟶ bag(B) ⟶ bag(C) ⟶ bag(D))
BY
{ (ProveWfLemma
   THEN InstLemma `concat-lifting_wf` [⌜D⌝; ⌜3⌝; ⌜λn.[A; B; C][n]⌝; ⌜λn.[a; b; c][n]⌝; ⌜f⌝]⋅
   THEN Try (Complete (Auto'))
   THEN Try (Complete (((MemCD THENA Auto) THEN IntSegCases (-1) THEN Reduce 0 THEN Auto)))
   THEN Unfold `funtype` 0
   THEN RepeatFor 2 (((RWO "primrec-unroll" 0 THENM Reduce 0) THENA Auto))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C,D:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C  {}\mrightarrow{}  bag(D)].
    (concat-lifting-3(f)  \mmember{}  bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C)  {}\mrightarrow{}  bag(D))


By

---

Latex:
(ProveWfLemma
  THEN  InstLemma  `concat-lifting\_wf`  [\mkleeneopen{}D\mkleeneclose{};  \mkleeneopen{}3\mkleeneclose{};  \mkleeneopen{}\mlambda{}n.[A;  B;  C][n]\mkleeneclose{};  \mkleeneopen{}\mlambda{}n.[a;  b;  c][n]\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto'))
  THEN  Try  (Complete  (((MemCD  THENA  Auto)  THEN  IntSegCases  (-1)  THEN  Reduce  0  THEN  Auto)))
  THEN  Unfold  `funtype`  0
  THEN  RepeatFor  2  (((RWO  "primrec-unroll"  0  THENM  Reduce  0)  THENA  Auto))
  THEN  Auto)

---

Home Index