### Nuprl Lemma : interleaving_singleton

`∀[T:Type]`
`  ∀L:T List. ∀i:ℕ||L||.`
`    ∃L2:T List`
`     ∃f1:ℕ1 ⟶ ℕ||L||. ∃f2:ℕ||L2|| ⟶ ℕ||L||. (interleaving_occurence(T;[L[i]];L2;L;f1;f2) ∧ ((f1 0) = i ∈ ℤ))`

Proof

Definitions occuring in Statement :  interleaving_occurence: `interleaving_occurence(T;L1;L2;L;f1;f2)` select: `L[n]` length: `||as||` cons: `[a / b]` nil: `[]` list: `T List` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  and: `P ∧ Q` exists: `∃x:A. B[x]` implies: `P `` Q` int_seg: `{i..j-}` member: `t ∈ T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` prop: `ℙ` top: `Top` not: `¬A` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` squash: `↓T` less_than: `a < b` or: `P ∨ Q` decidable: `Dec(P)` lelt: `i ≤ j < k` guard: `{T}` ge: `i ≥ j ` nat: `ℕ` less_than': `less_than'(a;b)` le: `A ≤ B` increasing: `increasing(f;k)` interleaving_occurence: `interleaving_occurence(T;L1;L2;L;f1;f2)` cons: `[a / b]` select: `L[n]` sq_type: `SQType(T)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` subtype_rel: `A ⊆r B` true: `True` subtract: `n - m` sq_stable: `SqStable(P)` uiff: `uiff(P;Q)` so_apply: `x[s]` so_lambda: `λ2x.t[x]` length: `||as||` list_ind: list_ind nil: `[]` it: `⋅` cand: `A c∧ B`
Rules used in proof :  universeEquality productElimination because_Cache sqequalRule independent_functionElimination cumulativity natural_numberEquality hypothesis rename setElimination intEquality lambdaEquality dependent_functionElimination hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution computeAll independent_pairFormation voidEquality voidElimination isect_memberEquality int_eqEquality dependent_pairFormation independent_isectElimination imageElimination unionElimination applyLambdaEquality equalitySymmetry equalityTransitivity dependent_set_memberEquality instantiate baseClosed imageMemberEquality applyEquality functionExtensionality functionEquality productEquality minusEquality addEquality hypothesis_subsumption promote_hyp hyp_replacement lambdaEquality_alt pointwiseFunctionality baseApply closedConclusion approximateComputation dependent_pairFormation_alt Error :memTop,  universeIsType dependent_set_memberEquality_alt lambdaFormation_alt productIsType inhabitedIsType equalityIstype sqequalBase

Latex:
\mforall{}[T:Type]
\mforall{}L:T  List.  \mforall{}i:\mBbbN{}||L||.
\mexists{}L2:T  List
\mexists{}f1:\mBbbN{}1  {}\mrightarrow{}  \mBbbN{}||L||
\mexists{}f2:\mBbbN{}||L2||  {}\mrightarrow{}  \mBbbN{}||L||.  (interleaving\_occurence(T;[L[i]];L2;L;f1;f2)  \mwedge{}  ((f1  0)  =  i))

Date html generated: 2020_05_20-AM-07_48_47
Last ObjectModification: 2020_01_25-PM-10_54_34

Theory : list!

Home Index