### Nuprl Lemma : prec-sub+-size

`∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[j:P]. ∀[x:prec(lbl,p.a[lbl;p];j)]. ∀[i:P].`
`∀[y:prec(lbl,p.a[lbl;p];i)].`
`  ||j;x|| < ||i;y|| supposing prec_sub+(P;lbl,p.a[lbl;p]) <j, x> <i, y>`

Proof

Definitions occuring in Statement :  prec_sub+: `prec_sub+(P;lbl,p.a[lbl; p])` prec-size: `||i;x||` prec: `prec(lbl,p.a[lbl; p];i)` list: `T List` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` apply: `f a` function: `x:A ⟶ B[x]` pair: `<a, b>` union: `left + right` atom: `Atom` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` implies: `P `` Q` all: `∀x:A. B[x]` infix_ap: `x f y` rel_plus: `R+` exists: `∃x:A. B[x]` prec_sub+: `prec_sub+(P;lbl,p.a[lbl; p])` less_than: `a < b` squash: `↓T` prop: `ℙ` nat: `ℕ` trans: `Trans(T;x,y.E[x; y])` decidable: `Dec(P)` or: `P ∨ Q` and: `P ∧ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` prec_sub: `prec_sub(P;lbl,p.a[lbl; p])`
Lemmas referenced :  rel_plus_closure prec_wf istype-atom prec_sub_wf less_than_wf prec-size_wf prec_sub+_wf subtype_rel_self member-less_than list_wf istype-universe decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_formula_prop_wf istype-less_than prec-sub-size
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin productEquality hypothesisEquality sqequalRule Error :lambdaEquality_alt,  applyEquality Error :inhabitedIsType,  hypothesis spreadEquality because_Cache Error :productIsType,  Error :universeIsType,  independent_functionElimination Error :lambdaFormation_alt,  dependent_functionElimination Error :dependent_pairEquality_alt,  instantiate universeEquality Error :isect_memberEquality_alt,  setElimination rename equalityTransitivity equalitySymmetry independent_isectElimination Error :isectIsTypeImplies,  Error :functionIsType,  unionEquality cumulativity productElimination unionElimination imageElimination natural_numberEquality approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality voidElimination independent_pairFormation

Latex:
\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].  \mforall{}[j:P].  \mforall{}[x:prec(lbl,p.a[lbl;p];j)].  \mforall{}[i:P].
\mforall{}[y:prec(lbl,p.a[lbl;p];i)].
||j;x||  <  ||i;y||  supposing  prec\_sub+(P;lbl,p.a[lbl;p])  <j,  x>  <i,  y>

Date html generated: 2019_06_20-PM-02_14_25
Last ObjectModification: 2019_02_23-PM-05_06_12

Theory : tuples

Home Index