### 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];j;x;i;y)` 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]` function: `x:A ⟶ B[x]` union: `left + right` atom: `Atom` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` squash: `↓T` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` ext-eq: `A ≡ B` nat: `ℕ` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` false: `False` prec: `prec(lbl,p.a[lbl; p];i)` list: `T List` ge: `i ≥ j ` le: `A ≤ B` prec-sub: `prec-sub(P;lbl,p.a[lbl; p];j;x;i;y)` dest-prec: `dest-prec(x)` let: let int_seg: `{i..j-}` lelt: `i ≤ j < k` less_than: `a < b` l_all: `(∀x∈L.P[x])` isl: `isl(x)` outl: `outl(x)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff` less_than': `less_than'(a;b)` cand: `A c∧ B` l_member: `(x ∈ l)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` respects-equality: `respects-equality(S;T)` prec-size: `||i;x||` pcorec-size: `pcorec-size(lbl,p.a[lbl; p])` sq_type: `SQType(T)`
Lemmas referenced :  less_than_wf squash_wf true_wf istype-int prec-size_wf istype-atom prec-size-unfold subtype_rel_self iff_weakening_equal prec-ext tuple-sum_wf prec_wf subtype_rel_universe1 list_wf decidable__le full-omega-unsat intformnot_wf intformle_wf itermConstant_wf int_formula_prop_not_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_wf istype-le nat_properties decidable__lt intformand_wf intformless_wf itermVar_wf itermAdd_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_add_lemma prec-sub_wf member-less_than istype-universe le-tuple-sum int_seg_properties l_sum_wf map_wf l_sum_nonneg non_neg_length nat_wf map_length select_wf length_wf int_seg_wf intformeq_wf int_formula_prop_eq_lemma bfalse_wf btrue_wf btrue_neq_bfalse select-tuple_wf int_seg_subtype_nat istype-false map-length select-map subtype_rel_list top_wf equal_wf subtype_rel-equal respects-equality-set pcorec_wf has-value_wf-partial set-value-type le_wf int-value-type pcorec-size_wf subtype-respects-equality subtype_rel_set change-equality-type istype-less_than le-l_sum subtype_base_sq set_subtype_base int_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut applyEquality thin Error :lambdaEquality_alt,  sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry Error :universeIsType,  Error :inhabitedIsType,  sqequalRule because_Cache natural_numberEquality imageMemberEquality baseClosed instantiate independent_isectElimination productElimination independent_functionElimination promote_hyp hypothesis_subsumption unionEquality cumulativity closedConclusion universeEquality setElimination rename unionElimination Error :unionIsType,  Error :dependent_set_memberEquality_alt,  dependent_functionElimination approximateComputation Error :dependent_pairFormation_alt,  Error :isect_memberEquality_alt,  voidElimination Error :lambdaFormation_alt,  applyLambdaEquality addEquality int_eqEquality independent_pairFormation Error :equalityIstype,  Error :isectIsTypeImplies,  Error :functionIsType,  intEquality functionExtensionality Error :inlEquality_alt,  Error :productIsType,  Error :inrEquality_alt,  hyp_replacement

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_05_47
Last ObjectModification: 2019_02_23-PM-01_13_41

Theory : tuples

Home Index