Nuprl Lemma : mk-prec_wf

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

Proof

Definitions occuring in Statement :  mk-prec: `mk-prec(lbl;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]` union: `left + right` natural_number: `\$n` atom: `Atom` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` prec-arg-types: `prec-arg-types(lbl,p.a[lbl; p];i;lbl)` mk-prec: `mk-prec(lbl;x)` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` so_lambda: `λ2x y.t[x; y]` subtype_rel: `A ⊆r B` ext-eq: `A ≡ B` and: `P ∧ Q`
Lemmas referenced :  prec-ext istype-less_than length_wf tuple-type_wf map_wf prec_wf list_wf prec-arg-types_wf istype-atom istype-universe
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality setElimination rename sqequalRule Error :dependent_pairEquality_alt,  Error :dependent_set_memberEquality_alt,  natural_numberEquality instantiate unionEquality cumulativity universeEquality applyEquality Error :universeIsType,  Error :lambdaEquality_alt,  equalityTransitivity equalitySymmetry Error :inhabitedIsType,  Error :lambdaFormation_alt,  unionElimination Error :equalityIstype,  dependent_functionElimination independent_functionElimination Error :unionIsType,  Error :setIsType,  Error :functionIsType,  productElimination

Latex:
\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].  \mforall{}[i:P].  \mforall{}[labl:\{lbl:Atom|  0  <  ||a[lbl;i]||\}  ].
\mforall{}[x:tuple-type(prec-arg-types(lbl,p.a[lbl;p];i;labl))].
(mk-prec(labl;x)  \mmember{}  prec(lbl,p.a[lbl;p];i))

Date html generated: 2019_06_20-PM-02_05_14
Last ObjectModification: 2019_02_22-PM-06_26_11

Theory : tuples

Home Index