---

Step * of Lemma simple-loc-comb1-concat-classrel

∀[Info,A,B:Type]. ∀[f:Id ⟶ A ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ simple-loc-comb1(l,a.concat-lifting1-loc(f;a;l);X)(e);↓∃a:A. (a ∈ X(e) ∧ v ↓∈ f loc(e) a))
BY
{ ((UnivCD THENA Auto)
   THEN InstLemma `simple-loc-comb-concat-classrel` [⌜Info⌝; ⌜B⌝; ⌜1⌝; ⌜λn.[A][n]⌝; ⌜λn.[X][n]⌝; ⌜λl,w. (f l (w 0))⌝; 
   ⌜λl,w. concat-lifting1-loc(f;w 0;l)⌝]⋅
   THEN Try (Complete ((Auto THEN Auto')))) }

1
.....antecedent..... 
1. Info : Type
2. A : Type
3. B : Type
4. f : Id ⟶ A ⟶ bag(B)
5. X : EClass(A)
6. es : EO+(Info)
7. e : E
8. v : B
⊢ ∀x:Id. ∀v:B. ∀bs:k:ℕ1 ⟶ bag((λn.[A][n]) k).
    (v ↓∈ (λl,w. concat-lifting1-loc(f;w 0;l)) x bs
    ⇐⇒ ↓∃vs:k:ℕ1 ⟶ ((λn.[A][n]) k). ((∀k:ℕ1. vs k ↓∈ bs k) ∧ v ↓∈ (λl,w. (f l (w 0))) x vs))

2
1. Info : Type
2. A : Type
3. B : Type
4. f : Id ⟶ A ⟶ bag(B)
5. X : EClass(A)
6. es : EO+(Info)
7. e : E
8. v : B
9. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
     uiff(v ∈ λl,w. concat-lifting1-loc(f;w 0;l)|Loc; λn.[X][n]|(e);↓∃vs:k:ℕ1 ⟶ ((λn.[A][n]) k)
                                                                  ((∀k:ℕ1. vs[k] ∈ λn.[X][n][k](e))
                                                                  ∧ v ↓∈ (λl,w. (f l (w 0))) loc(e) vs))
⊢ uiff(v ∈ simple-loc-comb1(l,a.concat-lifting1-loc(f;a;l);X)(e);↓∃a:A. (a ∈ X(e) ∧ v ↓∈ f loc(e) a))

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:B].
    uiff(v  \mmember{}  simple-loc-comb1(l,a.concat-lifting1-loc(f;a;l);X)(
                      e);\mdownarrow{}\mexists{}a:A.  (a  \mmember{}  X(e)  \mwedge{}  v  \mdownarrow{}\mmember{}  f  loc(e)  a))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  InstLemma  `simple-loc-comb-concat-classrel`  [\mkleeneopen{}Info\mkleeneclose{};  \mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}1\mkleeneclose{};  \mkleeneopen{}\mlambda{}n.[A][n]\mkleeneclose{};  \mkleeneopen{}\mlambda{}n.[X][n]\mkleeneclose{}; 
  \mkleeneopen{}\mlambda{}l,w.  (f  l  (w  0))\mkleeneclose{};  \mkleeneopen{}\mlambda{}l,w.  concat-lifting1-loc(f;w  0;l)\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  ((Auto  THEN  Auto'))))

---

Home Index