### Nuprl Lemma : prec-size-unfold

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

Proof

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: `T 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 b of inl(x) => s[x] | inr(y) => t[y]` union: `left + right` add: `n + m` natural_number: `\$n` int: `ℤ` atom: `Atom` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` ext-eq: `A ≡ B` and: `P ∧ Q` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` implies: `P `` Q` prec-size: `||i;x||` so_lambda: `λ2x y.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: `b supposing a` ge: `i ≥ j ` 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: `T 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

Latex:
\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)].
(||i;x||
=  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(\$_{}\$)  =>
0;a[lbl;i];z))

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

Theory : tuples

Home Index