### Nuprl Lemma : dest-prec_wf

`∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. ∀[x:prec(lbl,p.a[lbl;p];i)].`
`  (dest-prec(x) ∈ lbl:{lbl:Atom| 0 < ||a[lbl;i]||}  × tuple-type(prec-arg-types(lbl,p.a[lbl;p];i;lbl)))`

Proof

Definitions occuring in Statement :  dest-prec: `dest-prec(x)` prec-arg-types: `prec-arg-types(lbl,p.a[lbl; p];i;lbl)` prec: `prec(lbl,p.a[lbl; p];i)` tuple-type: `tuple-type(L)` length: `||as||` list: `T List` less_than: `a < b` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` product: `x:A × B[x]` union: `left + right` natural_number: `\$n` atom: `Atom` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` guard: `{T}` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q` uimplies: `b supposing a` dest-prec: `dest-prec(x)` prec-arg-types: `prec-arg-types(lbl,p.a[lbl; p];i;lbl)`
Lemmas referenced :  prec-ext subtype_rel_weakening prec_wf istype-atom less_than_wf length_wf tuple-type_wf map_wf list_wf prec-arg-types_wf istype-universe
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality sqequalRule Error :lambdaEquality_alt,  Error :inhabitedIsType,  productEquality setEquality atomEquality natural_numberEquality instantiate unionEquality cumulativity universeEquality equalityTransitivity equalitySymmetry Error :lambdaFormation_alt,  unionElimination Error :equalityIstype,  dependent_functionElimination independent_functionElimination Error :unionIsType,  setElimination rename independent_isectElimination productElimination Error :dependent_pairEquality_alt,  Error :universeIsType,  Error :functionIsType

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)].
(dest-prec(x)  \mmember{}  lbl:\{lbl:Atom|  0  <  ||a[lbl;i]||\}    \mtimes{}  tuple-type(prec-arg-types(lbl,p.a[lbl;p];i;lbl\000C)))

Date html generated: 2019_06_20-PM-02_05_18
Last ObjectModification: 2019_02_22-PM-06_29_20

Theory : tuples

Home Index