Nuprl Lemma : decidable__list-match-aux

[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
  ((∀a:A. ∀b:B.  Dec(R[a;b]))  (∀bs:B List. ∀as:A List. ∀used:ℤ List.  Dec(list-match-aux(as;bs;used;a,b.R[a;b]))))


Proof




Definitions occuring in Statement :  list-match-aux: list-match-aux(L1;L2;used;a,b.R[a; b]) list: List decidable: Dec(P) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] int: universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] member: t ∈ T so_lambda: λ2x.t[x] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] so_apply: x[s] prop: decidable: Dec(P) or: P ∨ Q subtype_rel: A ⊆B uimplies: supposing a top: Top and: P ∧ Q int_seg: {i..j-} guard: {T} lelt: i ≤ j < k not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False less_than: a < b squash: T iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  list_induction all_wf list_wf decidable_wf list-match-aux_wf list_match-aux-nil subtype_rel_list top_wf not_wf nil_wf deq-member_wf int-deq_wf decidable_functionality cons_wf exists_wf int_seg_wf length_wf assert_wf select_wf int_seg_properties decidable__le full-omega-unsat 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 list_match-aux-cons sq_stable_from_decidable decidable__exists_int_seg decidable__and2 decidable__not decidable__assert
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality intEquality hypothesis applyEquality independent_functionElimination rename because_Cache dependent_functionElimination functionEquality cumulativity universeEquality inlFormation independent_isectElimination isect_memberEquality voidElimination voidEquality functionExtensionality natural_numberEquality productEquality setElimination productElimination unionElimination approximateComputation dependent_pairFormation int_eqEquality independent_pairFormation imageElimination instantiate

Latex:
\mforall{}[A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a:A.  \mforall{}b:B.    Dec(R[a;b]))
    {}\mRightarrow{}  (\mforall{}bs:B  List.  \mforall{}as:A  List.  \mforall{}used:\mBbbZ{}  List.    Dec(list-match-aux(as;bs;used;a,b.R[a;b]))))



Date html generated: 2018_05_21-PM-00_47_19
Last ObjectModification: 2018_05_19-AM-06_50_16

Theory : list_1


Home Index