Step
*
1
of Lemma
in-simple-loc-comb-1-concat
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. Singlevalued(X)@i'
9. ∀i:Id. ∀a:A. (#(f i a) ≤ 1)@i
⊢ e ∈b f@(Loc, X) = e ∈b X ∧b (¬bbag-null(f loc(e) X(e)))
BY
{ ((With ⌈es⌉ (D (-2))⋅ THENM InstHyp [⌈e⌉] (-1)⋅) THENA Auto) }
1
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. ∀i:Id. ∀a:A. (#(f i a) ≤ 1)@i
9. ∀e:E. (#(X es e) ≤ 1)@i'
10. #(X es e) ≤ 1
⊢ e ∈b f@(Loc, X) = e ∈b X ∧b (¬bbag-null(f loc(e) X(e)))
Latex:
Latex:
1. Info : Type
2. A : Type
3. B : Type
4. f : Id {}\mrightarrow{} A {}\mrightarrow{} bag(B)
5. X : EClass(A)
6. es : EO+(Info)
7. e : E
8. Singlevalued(X)@i'
9. \mforall{}i:Id. \mforall{}a:A. (\#(f i a) \mleq{} 1)@i
\mvdash{} e \mmember{}\msubb{} f@(Loc, X) = e \mmember{}\msubb{} X \mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(f loc(e) X(e)))
By
Latex:
((With \mkleeneopen{}es\mkleeneclose{} (D (-2))\mcdot{} THENM InstHyp [\mkleeneopen{}e\mkleeneclose{}] (-1)\mcdot{}) THENA Auto)
Home
Index