Nuprl Lemma : list_match-aux-cons

[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
  ((∀a:A. ∀b:B.  SqStable(R[a;b]))
   (∀bs:B List. ∀u:A. ∀v:A List. ∀used:ℤ List.
        (list-match-aux([u v];bs;used;a,b.R[a;b])
        ⇐⇒ ∃j:ℕ||bs||. ((¬↑j ∈b used) ∧ R[u;bs[j]] ∧ list-match-aux(v;bs;[j 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]) select: L[n] length: ||as|| deq-member: x ∈b L cons: [a b] list: List int-deq: IntDeq int_seg: {i..j-} assert: b sq_stable: SqStable(P) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q not: ¬A implies:  Q and: P ∧ Q function: x:A ⟶ B[x] natural_number: $n 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_apply: x[s1;s2] so_apply: x[s] prop: iff: ⇐⇒ Q and: P ∧ Q so_lambda: λ2y.t[x; y] rev_implies:  Q int_seg: {i..j-} uimplies: supposing a guard: {T} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top less_than: a < b squash: T subtype_rel: A ⊆B list-match-aux: list-match-aux(L1;L2;used;a,b.R[a; b]) sq_exists: x:A [B[x]] le: A ≤ B less_than': less_than'(a;b) nat_plus: + true: True uiff: uiff(P;Q) cand: c∧ B sq_stable: SqStable(P) select: L[n] cons: [a b] subtract: m ge: i ≥  nat: inject: Inj(A;B;f) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b nequal: a ≠ b ∈  label: ...$L... t
Lemmas referenced :  deq-member_wf int-deq_wf list_wf all_wf sq_stable_wf list-match-aux_wf cons_wf exists_wf int_seg_wf length_wf not_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 length_of_cons_lemma false_wf add_nat_plus length_wf_nat less_than_wf nat_plus_wf nat_plus_properties add-is-int-iff itermAdd_wf intformeq_wf int_term_value_add_lemma int_formula_prop_eq_lemma equal_wf lelt_wf assert-deq-member l_member_wf and_wf squash_wf le_wf add-member-int_seg2 subtract_wf itermSubtract_wf int_term_value_subtract_lemma non_neg_length nat_wf nat_properties decidable__equal_int select-cons-tl add-subtract-cancel cons_member inject_wf sq_stable__and sq_stable__inject sq_stable__all sq_stable__not eq_int_wf bool_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int subtype_rel_self eqtt_to_assert assert_of_eq_int member_wf set_subtype_base int_subtype_base select-cons-hd select_cons_tl iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesis hypothesisEquality sqequalRule lambdaEquality applyEquality functionEquality cumulativity universeEquality independent_pairFormation natural_numberEquality productEquality dependent_functionElimination setElimination rename functionExtensionality because_Cache independent_isectElimination productElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality imageElimination dependent_set_memberEquality imageMemberEquality baseClosed equalityTransitivity equalitySymmetry applyLambdaEquality pointwiseFunctionality promote_hyp baseApply closedConclusion addEquality addLevel impliesFunctionality hyp_replacement instantiate dependent_set_memberFormation equalityElimination inlFormation levelHypothesis impliesLevelFunctionality inrFormation

Latex:
\mforall{}[A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a:A.  \mforall{}b:B.    SqStable(R[a;b]))
    {}\mRightarrow{}  (\mforall{}bs:B  List.  \mforall{}u:A.  \mforall{}v:A  List.  \mforall{}used:\mBbbZ{}  List.
                (list-match-aux([u  /  v];bs;used;a,b.R[a;b])
                \mLeftarrow{}{}\mRightarrow{}  \mexists{}j:\mBbbN{}||bs||.  ((\mneg{}\muparrow{}j  \mmember{}\msubb{}  used)  \mwedge{}  R[u;bs[j]]  \mwedge{}  list-match-aux(v;bs;[j  /  used];a,b.R[a;b])))))



Date html generated: 2018_05_21-PM-00_47_06
Last ObjectModification: 2018_05_19-AM-06_54_51

Theory : list_1


Home Index