---

Step * of Lemma rec-combined-class_wf

∀[Info:Type]. ∀[n:ℕ]. ∀[A:ℕn ─→ Type]. ∀[X:i:ℕn ─→ EClass(A i)]. ∀[T:Type]. ∀[f:(i:ℕn ─→ bag(A i)) ─→ bag(T) ─→ bag(T)].
  (f|X,(self)'| ∈ EClass(T))
BY
{ (Auto
   THEN All (Unfold `eclass`)
   THEN (ExtWith [`es'] [⌈Top ─→ Top⌉]⋅ THEN Auto THEN Try ((RecUnfold `rec-combined-class` 0 THEN Complete (Auto))))
   THEN ExtWith [`e'] [⌈Top ─→ Top⌉]⋅
   THEN Auto
   THEN Try ((RecUnfold `rec-combined-class` 0 THEN Reduce 0 THEN Complete (Auto)))
   THEN MoveToConcl (-1)
   THEN CausalInd'
   THEN RecUnfold `rec-combined-class` 0⋅
   THEN Reduce 0
   THEN Auto
   THEN Try ((All (Fold `eclass`) THEN GenConclAtAddr [2;1;1]⋅ THEN Auto)⋅)
   THEN RepUR ``primed-class local-pred-class`` 0) }

1
1. Info : Type
2. n : ℕ
3. A : ℕn ─→ Type
4. X : i:ℕn ─→ es:EO+(Info) ─→ e:E ─→ bag(A i)
5. T : Type
6. f : (i:ℕn ─→ bag(A i)) ─→ bag(T) ─→ bag(T)
7. es : EO+(Info)
8. e : E@i
9. ∀e1:E. ((e1 < e) ⇒ (f|X,(self)'| es e1 ∈ bag(T)))
⊢ case last(λe'.0 <z #(f|X,(self)'| es e')) e of inl(e') => f|X,(self)'| es e' | inr(x) => {} ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[X:i:\mBbbN{}n  {}\mrightarrow{}  EClass(A  i)].  \mforall{}[T:Type].  \mforall{}[f:(i:\mBbbN{}n  {}\mrightarrow{}  bag(A  i))
                                                                                                                                                                {}\mrightarrow{}  bag(T)
                                                                                                                                                                {}\mrightarrow{}  bag(T)].
    (f|X,(self)'|  \mmember{}  EClass(T))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `eclass`)
  THEN  (ExtWith  [`es']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}
              THEN  Auto
              THEN  Try  ((RecUnfold  `rec-combined-class`  0  THEN  Complete  (Auto))))
  THEN  ExtWith  [`e']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((RecUnfold  `rec-combined-class`  0  THEN  Reduce  0  THEN  Complete  (Auto)))
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'
  THEN  RecUnfold  `rec-combined-class`  0\mcdot{}
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((All  (Fold  `eclass`)  THEN  GenConclAtAddr  [2;1;1]\mcdot{}  THEN  Auto)\mcdot{})
  THEN  RepUR  ``primed-class  local-pred-class``  0)

---

Home Index