Step
*
1
of Lemma
dep-accum_wf
1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. f : very-dep-fun(A;B;a,b.C[a;b])
5. g : a:A ⟶ b:B ⟶ C[a;b]
6. n : ℕ
7. bs : B List
8. ∀b1:B List
(||b1|| < ||bs||
⇒ (dep-accum(L,b.f[L;b];a,b.g[a;b];b1) ∈ {L:(a:A × b:B × C[a;b]) List|
vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = b1 ∈ (B List))} ))
9. bs ~ if (||bs|| =z 0) then [] else firstn(||bs|| - 1;bs) @ [last(bs)] fi
10. ¬(||bs|| = 0 ∈ ℤ)
11. dep-accum(L,b.f[L;b];a,b.g[a;b];firstn(||bs|| - 1;bs)) ∈ {L:(a:A × b:B × C[a;b]) List|
vdf-eq(A;f;L)
∧ (map(λx.(fst(snd(x)));L)
= firstn(||bs|| - 1;bs)
∈ (B List))}
12. v : {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = firstn(||bs|| - 1;bs) ∈ (B List))}
13. dep-accum(L,b.f[L;b];a,bb.g[a;bb];firstn(||bs|| - 1;bs))
= v
∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = firstn(||bs|| - 1;bs) ∈ (B List))}
⊢ v @ let a = f[v;last(bs)] in [<a, last(bs), g[a;last(bs)]>] ∈ {L:(a:A × b:B × C[a;b]) List|
vdf-eq(A;f;L)
∧ (map(λx.(fst(snd(x)));L)
= (firstn(||bs|| - 1;bs) @ [last(bs)])
∈ (B List))}
BY
{ ((InstLemma `very-dep-fun-subtype` [⌜A⌝;⌜B⌝;⌜C⌝;⌜f⌝]⋅ THENA Auto)
THEN (GenConclTerm ⌜f[v;last(bs)]⌝⋅ THENA Auto)
THEN RepUR ``let`` 0
THEN RenameVar `a' (-2)) }
1
1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. f : very-dep-fun(A;B;a,b.C[a;b])
5. g : a:A ⟶ b:B ⟶ C[a;b]
6. n : ℕ
7. bs : B List
8. ∀b1:B List
(||b1|| < ||bs||
⇒ (dep-accum(L,b.f[L;b];a,b.g[a;b];b1) ∈ {L:(a:A × b:B × C[a;b]) List|
vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = b1 ∈ (B List))} ))
9. bs ~ if (||bs|| =z 0) then [] else firstn(||bs|| - 1;bs) @ [last(bs)] fi
10. ¬(||bs|| = 0 ∈ ℤ)
11. dep-accum(L,b.f[L;b];a,b.g[a;b];firstn(||bs|| - 1;bs)) ∈ {L:(a:A × b:B × C[a;b]) List|
vdf-eq(A;f;L)
∧ (map(λx.(fst(snd(x)));L)
= firstn(||bs|| - 1;bs)
∈ (B List))}
12. v : {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = firstn(||bs|| - 1;bs) ∈ (B List))}
13. dep-accum(L,b.f[L;b];a,bb.g[a;bb];firstn(||bs|| - 1;bs))
= v
∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = firstn(||bs|| - 1;bs) ∈ (B List))}
14. f ∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L)} ⟶ B ⟶ A
15. a : A
16. f[v;last(bs)] = a ∈ A
⊢ v @ [<a, last(bs), g[a;last(bs)]>] ∈ {L:(a:A × b:B × C[a;b]) List|
vdf-eq(A;f;L)
∧ (map(λx.(fst(snd(x)));L) = (firstn(||bs|| - 1;bs) @ [last(bs)]) ∈ (B List))}
Latex:
Latex:
1. A : Type
2. B : Type
3. C : A {}\mrightarrow{} B {}\mrightarrow{} Type
4. f : very-dep-fun(A;B;a,b.C[a;b])
5. g : a:A {}\mrightarrow{} b:B {}\mrightarrow{} C[a;b]
6. n : \mBbbN{}
7. bs : B List
8. \mforall{}b1:B List
(||b1|| < ||bs||
{}\mRightarrow{} (dep-accum(L,b.f[L;b];a,b.g[a;b];b1) \mmember{} \{L:(a:A \mtimes{} b:B \mtimes{} C[a;b]) List|
vdf-eq(A;f;L) \mwedge{} (map(\mlambda{}x.(fst(snd(x)));L) = b1)\} ))
9. bs \msim{} if (||bs|| =\msubz{} 0) then [] else firstn(||bs|| - 1;bs) @ [last(bs)] fi
10. \mneg{}(||bs|| = 0)
11. dep-accum(L,b.f[L;b];a,b.g[a;b];firstn(||bs|| - 1;bs)) \mmember{} \{L:(a:A \mtimes{} b:B \mtimes{} C[a;b]) List|
vdf-eq(A;f;L)
\mwedge{} (map(\mlambda{}x.(fst(snd(x)));L)
= firstn(||bs|| - 1;bs))\}
12. v : \{L:(a:A \mtimes{} b:B \mtimes{} C[a;b]) List|
vdf-eq(A;f;L) \mwedge{} (map(\mlambda{}x.(fst(snd(x)));L) = firstn(||bs|| - 1;bs))\}
13. dep-accum(L,b.f[L;b];a,bb.g[a;bb];firstn(||bs|| - 1;bs)) = v
\mvdash{} v @ let a = f[v;last(bs)] in [<a, last(bs), g[a;last(bs)]>] \mmember{} \{L:(a:A \mtimes{} b:B \mtimes{} C[a;b]) List|
vdf-eq(A;f;L)
\mwedge{} (map(\mlambda{}x.(fst(snd(x)));L)
= (firstn(||bs|| - 1;bs)
@ [last(bs)]))\}
By
Latex:
((InstLemma `very-dep-fun-subtype` [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (GenConclTerm \mkleeneopen{}f[v;last(bs)]\mkleeneclose{}\mcdot{} THENA Auto)
THEN RepUR ``let`` 0
THEN RenameVar `a' (-2))
Home
Index