---

Step * of Lemma rec-combined-loc-class_wf

∀[Info:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[X:i:ℕn ⟶ EClass(A i)]. ∀[T:Type]. ∀[f:Id
                                                                                ⟶ (i:ℕn ⟶ bag(A i))
                                                                                ⟶ bag(T)
                                                                                ⟶ bag(T)].
  (f|Loc, X, Prior(self)| ∈ EClass(T))
BY
{ (Auto
   THEN All (Unfold `eclass`)
   THEN (ExtWith [`es'] [⌜Top ⟶ Top⌝]⋅
         THEN Auto
         THEN Try ((RecUnfold `rec-combined-loc-class` 0 THEN Complete (Auto))))
   THEN ExtWith [`e'] [⌜Top ⟶ Top⌝]⋅
   THEN Auto
   THEN Try ((RecUnfold `rec-combined-loc-class` 0 THEN Reduce 0 THEN Complete (Auto)))
   THEN MoveToConcl (-1)
   THEN CausalInd'
   THEN RecUnfold `rec-combined-loc-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 : Id ⟶ (i:ℕn ⟶ bag(A i)) ⟶ bag(T) ⟶ bag(T)
7. es : EO+(Info)
8. e : E@i
9. ∀e1:E. ((e1 < e) ⇒ (f|Loc, X, Prior(self)| es e1 ∈ bag(T)))
⊢ case last(λe'.0 <z #(f|Loc, X, Prior(self)| es e')) e of inl(e') => f|Loc, X, Prior(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:Id
                                                                                                                                                                {}\mrightarrow{}  (i:\mBbbN{}n
                                                                                                                                                                      {}\mrightarrow{}  bag(A  i))
                                                                                                                                                                {}\mrightarrow{}  bag(T)
                                                                                                                                                                {}\mrightarrow{}  bag(T)].
    (f|Loc,  X,  Prior(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-loc-class`  0  THEN  Complete  (Auto))))
  THEN  ExtWith  [`e']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((RecUnfold  `rec-combined-loc-class`  0  THEN  Reduce  0  THEN  Complete  (Auto)))
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'
  THEN  RecUnfold  `rec-combined-loc-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