Step
*
1
1
1
1
of Lemma
simple-loc-comb2-concat-classrel
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ bag(C)
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. x : Id@i
12. v1 : C@i
13. bs : k:ℕ2 ─→ bag([A; B][k])@i
14. b : bag(C)
15. v1 ↓∈ b
16. x@0 : A
17. x@0 ↓∈ bs 0
18. x@1 : B
19. x@1 ↓∈ bs 1
20. b = (f x x@0 x@1) ∈ bag(C)
⊢ ↓∃vs:k:ℕ2 ─→ [A; B][k]. ((∀k:ℕ2. vs k ↓∈ bs k) ∧ v1 ↓∈ f x (vs 0) (vs 1))
BY
{ (D 0 THEN InstConcl [⌈λn.[x@0; x@1][n]⌉]⋅ THEN Reduce 0)⋅ }
1
.....wf.....
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ bag(C)
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. x : Id@i
12. v1 : C@i
13. bs : k:ℕ2 ─→ bag([A; B][k])@i
14. b : bag(C)
15. v1 ↓∈ b
16. x@0 : A
17. x@0 ↓∈ bs 0
18. x@1 : B
19. x@1 ↓∈ bs 1
20. b = (f x x@0 x@1) ∈ bag(C)
⊢ λn.[x@0; x@1][n] ∈ k:ℕ2 ─→ [A; B][k]
2
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ bag(C)
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. x : Id@i
12. v1 : C@i
13. bs : k:ℕ2 ─→ bag([A; B][k])@i
14. b : bag(C)
15. v1 ↓∈ b
16. x@0 : A
17. x@0 ↓∈ bs 0
18. x@1 : B
19. x@1 ↓∈ bs 1
20. b = (f x x@0 x@1) ∈ bag(C)
⊢ (∀k:ℕ2. [x@0; x@1][k] ↓∈ bs k) ∧ v1 ↓∈ f x x@0 x@1
3
.....wf.....
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ bag(C)
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. x : Id@i
12. v1 : C@i
13. bs : k:ℕ2 ─→ bag([A; B][k])@i
14. b : bag(C)
15. v1 ↓∈ b
16. x@0 : A
17. x@0 ↓∈ bs 0
18. x@1 : B
19. x@1 ↓∈ bs 1
20. b = (f x x@0 x@1) ∈ bag(C)
21. vs : k:ℕ2 ─→ [A; B][k]
⊢ (∀k:ℕ2. vs k ↓∈ bs k) ∧ v1 ↓∈ f x (vs 0) (vs 1) ∈ ℙ
Latex:
Latex:
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} bag(C)
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. x : Id@i
12. v1 : C@i
13. bs : k:\mBbbN{}2 {}\mrightarrow{} bag([A; B][k])@i
14. b : bag(C)
15. v1 \mdownarrow{}\mmember{} b
16. x@0 : A
17. x@0 \mdownarrow{}\mmember{} bs 0
18. x@1 : B
19. x@1 \mdownarrow{}\mmember{} bs 1
20. b = (f x x@0 x@1)
\mvdash{} \mdownarrow{}\mexists{}vs:k:\mBbbN{}2 {}\mrightarrow{} [A; B][k]. ((\mforall{}k:\mBbbN{}2. vs k \mdownarrow{}\mmember{} bs k) \mwedge{} v1 \mdownarrow{}\mmember{} f x (vs 0) (vs 1))
By
Latex:
(D 0 THEN InstConcl [\mkleeneopen{}\mlambda{}n.[x@0; x@1][n]\mkleeneclose{}]\mcdot{} THEN Reduce 0)\mcdot{}
Home
Index