### Nuprl Lemma : isl-first-success

`∀[T:Type]. ∀[A:T ⟶ Type].`
`  ∀f:x:T ⟶ (A[x]?). ∀L:T List.`
`    ((↑isl(first-success(f;L)))`
`    `` (fst(outl(first-success(f;L))) < ||L||`
`       ∧ ((f L[fst(outl(first-success(f;L)))])`
`         = (inl (snd(outl(first-success(f;L)))))`
`         ∈ (A[L[fst(outl(first-success(f;L)))]]?))`
`       ∧ (∀x∈firstn(fst(outl(first-success(f;L)));L).↑isr(f x))))`

Proof

Definitions occuring in Statement :  firstn: `firstn(n;as)` l_all: `(∀x∈L.P[x])` first-success: `first-success(f;L)` select: `L[n]` length: `||as||` list: `T List` outl: `outl(x)` assert: `↑b` isr: `isr(x)` isl: `isl(x)` less_than: `a < b` uall: `∀[x:A]. B[x]` so_apply: `x[s]` pi1: `fst(t)` pi2: `snd(t)` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` unit: `Unit` apply: `f a` function: `x:A ⟶ B[x]` inl: `inl x` union: `left + right` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` prop: `ℙ` less_than: `a < b` squash: `↓T` isl: `isl(x)` outl: `outl(x)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` pi1: `fst(t)` pi2: `snd(t)` iff: `P `⇐⇒` Q` cand: `A c∧ B` unit: `Unit` bfalse: `ff`
Lemmas referenced :  first-success_wf select_wf int_seg_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma first-success-is-inl true_wf false_wf equal_wf assert_wf isl_wf int_seg_wf length_wf unit_wf2 list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesisEquality sqequalRule lambdaEquality applyEquality functionExtensionality hypothesis unionEquality productEquality because_Cache independent_isectElimination setElimination rename productElimination dependent_functionElimination unionElimination natural_numberEquality dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageElimination independent_functionElimination equalityElimination equalityTransitivity equalitySymmetry functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[A:T  {}\mrightarrow{}  Type].
\mforall{}f:x:T  {}\mrightarrow{}  (A[x]?).  \mforall{}L:T  List.
((\muparrow{}isl(first-success(f;L)))
{}\mRightarrow{}  (fst(outl(first-success(f;L)))  <  ||L||
\mwedge{}  ((f  L[fst(outl(first-success(f;L)))])  =  (inl  (snd(outl(first-success(f;L))))))
\mwedge{}  (\mforall{}x\mmember{}firstn(fst(outl(first-success(f;L)));L).\muparrow{}isr(f  x))))

Date html generated: 2017_04_14-AM-09_23_42
Last ObjectModification: 2017_02_27-PM-03_58_26

Theory : list_1

Home Index