Step
*
2
1
of Lemma
permute-to-front-permutation
1. [T] : Type
2. L : T List
3. idxs : ℕ List
⊢ Inj(ℕ||L||;ℕ||L||;λi.filter(λi.int-list-member(i;idxs);upto(||L||))
@ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[i])
BY
{ xxx(GenConclAtAddrType ℕ||L|| List [3;1;2]⋅ THENA Auto)xxx }
1
1. [T] : Type
2. L : T List
3. idxs : ℕ List
4. v : ℕ||L|| List
5. (filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||)))
= v
∈ (ℕ||L|| List)
⊢ Inj(ℕ||L||;ℕ||L||;λi.v[i])
Latex:
Latex:
1. [T] : Type
2. L : T List
3. idxs : \mBbbN{} List
\mvdash{} Inj(\mBbbN{}||L||;\mBbbN{}||L||;\mlambda{}i.filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))
@ filter(\mlambda{}i.(\mneg{}\msubb{}int-list-member(i;idxs));upto(||L||))[i])
By
Latex:
xxx(GenConclAtAddrType \mBbbN{}||L|| List [3;1;2]\mcdot{} THENA Auto)xxx
Home
Index