Step
*
1
2
1
2
1
of Lemma
simple-loc-comb2-classrel
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ C
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. ↓∃vs:k:ℕ2 ─→ [A; B][k]. ((∀k:ℕ2. vs[k] ∈ [X; Y][k](e)) ∧ (v = (f loc(e) (vs 0) (vs 1)) ∈ C))
supposing v ∈ λl,w. lifting2-loc(f;l;w 0;w 1)|Loc; λ2k.[X; Y][k]|(e)
12. v ∈ λl,w. lifting2-loc(f;l;w 0;w 1)|Loc; λ2k.[X; Y][k]|(e)
supposing ↓∃vs:k:ℕ2 ─→ [A; B][k]. ((∀k:ℕ2. vs[k] ∈ [X; Y][k](e)) ∧ (v = (f loc(e) (vs 0) (vs 1)) ∈ C))
⊢ λl,w. lifting2-loc(f;l;w 0;w 1)|Loc; λz.[X; Y][z]| ∈ EClass(C)
BY
{ (InstLemma `simple-loc-comb_wf` [⌈Info⌉; ⌈C⌉; ⌈2⌉; ⌈λx.[A; B][x]⌉; ⌈λx.[X; Y][x]⌉; ⌈λl,w. lifting2-loc(f;l;w 0;w 1)⌉]⋅
THEN Try (Complete (Auto'))
) }
Latex:
Latex:
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} C
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. \mdownarrow{}\mexists{}vs:k:\mBbbN{}2 {}\mrightarrow{} [A; B][k]. ((\mforall{}k:\mBbbN{}2. vs[k] \mmember{} [X; Y][k](e)) \mwedge{} (v = (f loc(e) (vs 0) (vs 1))))
supposing v \mmember{} \mlambda{}l,w. lifting2-loc(f;l;w 0;w 1)|Loc; \mlambda{}\msubtwo{}k.[X; Y][k]|(e)
12. v \mmember{} \mlambda{}l,w. lifting2-loc(f;l;w 0;w 1)|Loc; \mlambda{}\msubtwo{}k.[X; Y][k]|(e)
supposing \mdownarrow{}\mexists{}vs:k:\mBbbN{}2 {}\mrightarrow{} [A; B][k]
((\mforall{}k:\mBbbN{}2. vs[k] \mmember{} [X; Y][k](e)) \mwedge{} (v = (f loc(e) (vs 0) (vs 1))))
\mvdash{} \mlambda{}l,w. lifting2-loc(f;l;w 0;w 1)|Loc; \mlambda{}z.[X; Y][z]| \mmember{} EClass(C)
By
Latex:
(InstLemma `simple-loc-comb\_wf` [\mkleeneopen{}Info\mkleeneclose{}; \mkleeneopen{}C\mkleeneclose{}; \mkleeneopen{}2\mkleeneclose{}; \mkleeneopen{}\mlambda{}x.[A; B][x]\mkleeneclose{}; \mkleeneopen{}\mlambda{}x.[X; Y][x]\mkleeneclose{};
\mkleeneopen{}\mlambda{}l,w. lifting2-loc(f;l;w 0;w 1)\mkleeneclose{}]\mcdot{}
THEN Try (Complete (Auto'))
)
Home
Index