Nuprl Lemma : accum_split_prefix

[A,T:Type]. ∀[x:A]. ∀[g:(T List × A) ⟶ A]. ∀[f:(T List × A) ⟶ 𝔹]. ∀[L:T List].
  ↑(f (snd(accum_split(g;x;f;concat(map(λp.(fst(p));fst(accum_split(g;x;f;L)))))))) 
  supposing ¬↑null(fst(accum_split(g;x;f;L)))


Proof




Definitions occuring in Statement :  accum_split: accum_split(g;x;f;L) null: null(as) concat: concat(ll) map: map(f;as) list: List assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] pi1: fst(t) pi2: snd(t) not: ¬A apply: a lambda: λx.A[x] function: x:A ⟶ B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] implies:  Q prop: subtype_rel: A ⊆B top: Top so_apply: x[s] all: x:A. B[x] pi1: fst(t) guard: {T} accum_split: accum_split(g;x;f;L) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] assert: b ifthenelse: if then else fi  btrue: tt concat: concat(ll) pi2: snd(t) not: ¬A true: True false: False spreadn: spread3 bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) and: P ∧ Q is_accum_splitting: is_accum_splitting(T;A;L;LL;L2;f;g;x) bfalse: ff iff: ⇐⇒ Q rev_implies:  Q squash: T
Lemmas referenced :  last_induction not_wf assert_wf null_wf3 list_wf accum_split_wf concat_wf map_wf pi1_wf_top set_wf is_accum_splitting_wf equal_wf pi2_wf assert_witness subtype_rel_product top_wf subtype_rel_list bool_wf list_accum_nil_lemma null_nil_lemma map_nil_lemma reduce_nil_lemma true_wf list_accum_cons_lemma uiff_transitivity equal-wf-T-base eqtt_to_assert assert_of_null iff_transitivity bnot_wf iff_weakening_uiff eqff_to_assert assert_of_bnot list_accum_append accum_split_inverse map_append_sq map_cons_lemma concat_append concat-single squash_wf append_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality because_Cache applyEquality hypothesis functionExtensionality productEquality cumulativity productElimination independent_pairEquality isect_memberEquality voidElimination voidEquality spreadEquality lambdaFormation setElimination rename equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination independent_isectElimination universeEquality natural_numberEquality unionElimination equalityElimination baseClosed independent_pairFormation impliesFunctionality hyp_replacement applyLambdaEquality setEquality imageElimination imageMemberEquality

Latex:
\mforall{}[A,T:Type].  \mforall{}[x:A].  \mforall{}[g:(T  List  \mtimes{}  A)  {}\mrightarrow{}  A].  \mforall{}[f:(T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    \muparrow{}(f  (snd(accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));fst(accum\_split(g;x;f;L)))))))) 
    supposing  \mneg{}\muparrow{}null(fst(accum\_split(g;x;f;L)))



Date html generated: 2018_05_21-PM-08_07_23
Last ObjectModification: 2017_07_26-PM-05_43_18

Theory : general


Home Index