Nuprl Lemma : bar-induction

[T:Type]. ∀[R,A:(T List) ⟶ ℙ].
  ((∀s:T List. Dec(R[s]))
   (∀s:T List. (R[s]  A[s]))
   (∀s:T List. ((∀t:T. A[s [t]])  A[s]))
   (∀s:T List. ((∀alpha:ℕ ⟶ T. (↓∃n:ℕR[s map(alpha;upto(n))]))  A[s])))


Proof




Definitions occuring in Statement :  upto: upto(n) map: map(f;as) append: as bs cons: [a b] nil: [] list: List nat: decidable: Dec(P) uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] squash: T implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] member: t ∈ T so_apply: x[s] nat: so_apply: x[s1;s2] prop: so_lambda: λ2x.t[x] subtype_rel: A ⊆B uimplies: supposing a le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A guard: {T} top: Top ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] int_seg: {i..j-} lelt: i ≤ j < k squash: T true: True iff: ⇐⇒ Q seq-adjoin: s++t seq-append: seq-append(n;m;s1;s2) less_than: a < b bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  label: ...$L... t rev_implies:  Q bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b cand: c∧ B
Lemmas referenced :  bar_induction list_wf map_wf int_seg_wf upto_wf nat_wf all_wf seq-adjoin_wf squash_wf exists_wf append_wf subtype_rel_dep_function int_seg_subtype_nat false_wf cons_wf nil_wf decidable_wf list_extensionality length-append map-length length_of_cons_lemma length_of_nil_lemma length_upto nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_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_add_lemma int_term_value_var_lemma int_formula_prop_wf le_wf select-map subtype_rel_list top_wf less_than_wf true_wf length_append iff_weakening_equal add_functionality_wrt_eq length_wf map_length_nat length-singleton lelt_wf length-map intformless_wf int_formula_prop_less_lemma lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int equal_wf select_upto decidable__equal_int intformeq_wf int_formula_prop_eq_lemma decidable__lt eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot select-cons-hd subtract_wf itermSubtract_wf int_term_value_subtract_lemma select-append select-upto length_wf_nat select_wf int_seg_properties seq-append_wf add_nat_wf add-is-int-iff non_neg_length
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule hypothesisEquality lambdaEquality applyEquality functionExtensionality cumulativity hypothesis natural_numberEquality setElimination rename because_Cache functionEquality independent_functionElimination dependent_functionElimination addEquality independent_isectElimination independent_pairFormation universeEquality hyp_replacement equalitySymmetry isect_memberEquality voidElimination voidEquality dependent_set_memberEquality unionElimination dependent_pairFormation int_eqEquality intEquality computeAll imageElimination equalityTransitivity productElimination imageMemberEquality baseClosed lessCases sqequalAxiom equalityElimination promote_hyp instantiate applyLambdaEquality pointwiseFunctionality baseApply closedConclusion

Latex:
\mforall{}[T:Type].  \mforall{}[R,A:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}s:T  List.  Dec(R[s]))
    {}\mRightarrow{}  (\mforall{}s:T  List.  (R[s]  {}\mRightarrow{}  A[s]))
    {}\mRightarrow{}  (\mforall{}s:T  List.  ((\mforall{}t:T.  A[s  @  [t]])  {}\mRightarrow{}  A[s]))
    {}\mRightarrow{}  (\mforall{}s:T  List.  ((\mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  R[s  @  map(alpha;upto(n))]))  {}\mRightarrow{}  A[s])))



Date html generated: 2017_04_17-AM-08_59_46
Last ObjectModification: 2017_02_27-PM-05_16_39

Theory : list_1


Home Index