### Nuprl Lemma : interleaving_of_cons

`∀[T:Type]`
`  ∀x:T. ∀L,L1,L2:T List.`
`    (interleaving(T;L1;L2;[x / L])`
`    `⇐⇒` (0 < ||L1|| c∧ ((L1[0] = x ∈ T) ∧ interleaving(T;tl(L1);L2;L)))`
`        ∨ (0 < ||L2|| c∧ ((L2[0] = x ∈ T) ∧ interleaving(T;L1;tl(L2);L))))`

Proof

Definitions occuring in Statement :  interleaving: `interleaving(T;L1;L2;L)` select: `L[n]` length: `||as||` tl: `tl(l)` cons: `[a / b]` list: `T List` less_than: `a < b` uall: `∀[x:A]. B[x]` cand: `A c∧ B` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q` and: `P ∧ Q` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  or: `P ∨ Q` decidable: `Dec(P)` member: `t ∈ T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` prop: `ℙ` cand: `A c∧ B` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` guard: `{T}` true: `True` squash: `↓T` less_than: `a < b` nat_plus: `ℕ+` cons: `[a / b]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff` disjoint_sublists: `disjoint_sublists(T;L1;L2;L)` interleaving: `interleaving(T;L1;L2;L)` subtype_rel: `A ⊆r B` lelt: `i ≤ j < k` int_seg: `{i..j-}` inject: `Inj(A;B;f)` unit: `Unit` bool: `𝔹` sq_type: `SQType(T)` nat: `ℕ` ge: `i ≥ j ` subtract: `n - m` increasing: `increasing(f;k)` rev_uimplies: `rev_uimplies(P;Q)` colength: `colength(L)`
Rules used in proof :  universeEquality universeIsType inhabitedIsType unionElimination hypothesis hypothesisEquality isectElimination thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution productElimination independent_isectElimination sqequalRule baseClosed lambdaFormation isect_memberEquality voidElimination voidEquality hyp_replacement equalitySymmetry applyLambdaEquality cumulativity because_Cache productEquality natural_numberEquality independent_pairFormation equalityTransitivity imageElimination intEquality int_eqEquality lambdaEquality dependent_pairFormation approximateComputation closedConclusion baseApply promote_hyp pointwiseFunctionality rename setElimination imageMemberEquality dependent_set_memberEquality independent_functionElimination inrFormation functionEquality addEquality productIsType equalityIsType1 lambdaEquality_alt dependent_pairFormation_alt dependent_set_memberEquality_alt isect_memberEquality_alt inlFormation_alt unionIsType equalityIsType3 inrFormation_alt equalityIsType4 applyEquality equalityElimination instantiate functionExtensionality sqequalBase equalityIstype Error :memTop,  functionIsType inlFormation minusEquality hypothesis_subsumption functionIsTypeImplies axiomEquality intWeakElimination

Latex:
\mforall{}[T:Type]
\mforall{}x:T.  \mforall{}L,L1,L2:T  List.
(interleaving(T;L1;L2;[x  /  L])
\mLeftarrow{}{}\mRightarrow{}  (0  <  ||L1||  c\mwedge{}  ((L1[0]  =  x)  \mwedge{}  interleaving(T;tl(L1);L2;L)))
\mvee{}  (0  <  ||L2||  c\mwedge{}  ((L2[0]  =  x)  \mwedge{}  interleaving(T;L1;tl(L2);L))))

Date html generated: 2020_05_20-AM-07_48_41
Last ObjectModification: 2020_04_06-PM-06_47_41

Theory : list!

Home Index