Nuprl Lemma : prec-size-unfold

[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P Type) List)]. ∀[i:P]. ∀[x:prec(lbl,p.a[lbl;p];i)].
  let lbl,z 
    in 1
       tuple-sum(λc,x. case c
                         of inl(p) =>
                         case of inl(j) => ||j;x|| inr(j) => l_sum(map(λz.||j;z||;x))
                         inr(_) =>
  ∈ ℤ)


Definitions occuring in Statement :  prec-size: ||i;x|| prec: prec(lbl,p.a[lbl; p];i) tuple-sum: tuple-sum(f;L;x) l_sum: l_sum(L) map: map(f;as) list: List uall: [x:A]. B[x] so_apply: x[s1;s2] lambda: λx.A[x] function: x:A ⟶ B[x] spread: spread def decide: case of inl(x) => s[x] inr(y) => t[y] union: left right add: m natural_number: $n int: atom: Atom universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B all: x:A. B[x] implies:  Q prec-size: ||i;x|| so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2] add-sz: add-sz(sz;L;x) squash: T prop: nat: l_all: (∀x∈L.P[x]) uimplies: supposing a ge: i ≥  int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than: a < b decidable: Dec(P) or: P ∨ Q false: False guard: {T} not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] true: True prec: prec(lbl,p.a[lbl; p];i) list: List
Lemmas referenced :  prec-ext unroll-pcorec-size istype-void tuple-sum_wf squash_wf true_wf istype-nat tuple-type_wf map_wf list_wf istype-universe prec_wf istype-atom prec-size_wf l_sum_nonneg map-length select-map subtype_rel_list top_wf non_neg_length int_seg_properties decidable__le select_wf length_wf nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformnot_wf istype-int int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_formula_prop_wf istype-le int_seg_wf nat_wf l_sum_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination applyEquality sqequalRule Error :inhabitedIsType,  Error :lambdaFormation_alt,  Error :isect_memberEquality_alt,  voidElimination setElimination rename addEquality natural_numberEquality instantiate Error :lambdaEquality_alt,  imageElimination equalityTransitivity equalitySymmetry Error :universeIsType,  Error :functionIsType,  cumulativity universeEquality unionEquality unionElimination Error :equalityIstype,  dependent_functionElimination independent_functionElimination Error :unionIsType,  intEquality independent_isectElimination because_Cache Error :dependent_set_memberEquality_alt,  applyLambdaEquality functionExtensionality approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality independent_pairFormation imageMemberEquality baseClosed

\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].  \mforall{}[i:P].  \mforall{}[x:prec(lbl,p.a[lbl;p];i)].
    =  let  lbl,z  =  x 
        in  1
              +  tuple-sum(\mlambda{}c,x.  case  c
                                                  of  inl(p)  =>
                                                  case  p  of  inl(j)  =>  ||j;x||  |  inr(j)  =>  l\_sum(map(\mlambda{}z.||j;z||;x))
                                                  |  inr($_{}$)  =>

Date html generated: 2019_06_20-PM-02_05_07
Last ObjectModification: 2019_02_22-PM-06_23_02

Theory : tuples

Home Index