---

Step * 1 of Lemma rec-comb_wf2


1. Info : Type
2. n : ℕ
3. m : ℕ
4. A : {m..n-} ─→ Type
5. X : i:{m..n-} ─→ es:EO+(Info) ─→ e:E ─→ bag(A i)
6. T : Type
7. f : Id ─→ (i:{m..n-} ─→ bag(A i)) ─→ bag(T) ─→ bag(T)
8. init : Id ─→ bag(T)
⊢ rec-comb(X;f;init) ∈ es:EO+(Info) ─→ e:E ─→ bag(T)
BY
{ ((ExtWith [`es'] [⌈Top ─→ Top⌉]⋅ THEN Try (Complete (Auto)) THEN Try ((RecUnfold `rec-comb` 0 THEN Complete (Auto))))
   THEN ExtWith [`e'] [⌈Top ─→ Top⌉]⋅
   THEN Try (Complete (Auto))
   THEN Try ((RecUnfold `rec-comb` 0 THEN Reduce 0 THEN Complete (Auto)))
   THEN MoveToConcl (-1)
   THEN CausalInd'
   THEN RecUnfold `rec-comb` 0⋅
   THEN RepUR ``primed-class-opt`` 0
   THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))
   THEN Try ((D -2 THEN BackThruSomeHyp THEN Auto))
   THEN BLemma `es-local-pred_wf2`
   THEN Try (Complete (Auto))
   THEN RepeatFor 3 (MemCD)
   THEN Try (Complete (Auto))
   THEN D -1
   THEN BackThruSomeHyp
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  A  :  \{m..n\msupminus{}\}  {}\mrightarrow{}  Type
5.  X  :  i:\{m..n\msupminus{}\}  {}\mrightarrow{}  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A  i)
6.  T  :  Type
7.  f  :  Id  {}\mrightarrow{}  (i:\{m..n\msupminus{}\}  {}\mrightarrow{}  bag(A  i))  {}\mrightarrow{}  bag(T)  {}\mrightarrow{}  bag(T)
8.  init  :  Id  {}\mrightarrow{}  bag(T)
\mvdash{}  rec-comb(X;f;init)  \mmember{}  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(T)


By

---

Latex:
((ExtWith  [`es']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}
    THEN  Try  (Complete  (Auto))
    THEN  Try  ((RecUnfold  `rec-comb`  0  THEN  Complete  (Auto))))
  THEN  ExtWith  [`e']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((RecUnfold  `rec-comb`  0  THEN  Reduce  0  THEN  Complete  (Auto)))
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'
  THEN  RecUnfold  `rec-comb`  0\mcdot{}
  THEN  RepUR  ``primed-class-opt``  0
  THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  Try  ((D  -2  THEN  BackThruSomeHyp  THEN  Auto))
  THEN  BLemma  `es-local-pred\_wf2`
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  3  (MemCD)
  THEN  Try  (Complete  (Auto))
  THEN  D  -1
  THEN  BackThruSomeHyp
  THEN  Auto)\mcdot{}

---

Home Index