Nuprl Lemma : prec-ext

`∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P].`
`  prec(lbl,p.a[lbl;p];i) ≡ labl:{lbl:Atom| 0 < ||a[lbl;i]||}  × tuple-type(map(λx.case x`
`                                                    of inl(y) =>`
`                                                    case y`
`                                                     of inl(p) =>`
`                                                     prec(lbl,p.a[lbl;p];p)`
`                                                     | inr(p) =>`
`                                                     prec(lbl,p.a[lbl;p];p) List`
`                                                    | inr(E) =>`
`                                                    E;a[labl;i]))`

Proof

Definitions occuring in Statement :  prec: `prec(lbl,p.a[lbl; p];i)` tuple-type: `tuple-type(L)` length: `||as||` map: `map(f;as)` list: `T List` ext-eq: `A ≡ B` less_than: `a < b` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` set: `{x:A| B[x]} ` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` product: `x:A × B[x]` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` union: `left + right` natural_number: `\$n` atom: `Atom` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` ext-family: `F ≡ G` all: `∀x:A. B[x]` ptuple: `ptuple(lbl,p.a[lbl; p];X)` ext-eq: `A ≡ B` and: `P ∧ Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` so_apply: `x[s]` so_lambda: `λ2x.t[x]` prop: `ℙ` pi2: `snd(t)` pi1: `fst(t)` prec: `prec(lbl,p.a[lbl; p];i)` guard: `{T}` nat: `ℕ` uimplies: `b supposing a` top: `Top` has-value: `(a)↓` bfalse: `ff` ifthenelse: `if b then t else f fi ` btrue: `tt` unit: `Unit` bool: `𝔹` less_than': `less_than'(a;b)` squash: `↓T` less_than: `a < b` sq_type: `SQType(T)` it: `⋅` nil: `[]` colength: `colength(L)` decidable: `Dec(P)` cons: `[a / b]` or: `P ∨ Q` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` ge: `i ≥ j ` false: `False` tuple-sum: `tuple-sum(f;L;x)` add-sz: `add-sz(sz;L;x)` map: `map(f;as)` list_ind: list_ind le: `A ≤ B` cand: `A c∧ B` int_seg: `{i..j-}` lelt: `i ≤ j < k` null: `null(as)` istype: `istype(T)` uiff: `uiff(P;Q)` reduce: `reduce(f;k;as)` l_sum: `l_sum(L)` sq_stable: `SqStable(P)` iff: `P `⇐⇒` Q` true: `True`
Lemmas referenced :  pcorec-ext prec_wf istype-atom istype-less_than length_wf tuple-type_wf map_wf list_wf istype-universe pi1_wf pcorec_wf less_than_wf pi2_wf subtype_rel_weakening ext-eq_inversion pcorec-size_wf int-value-type istype-int le_wf set-value-type nat_wf has-value_wf-partial istype-void unroll-pcorec-size add-sz_wf termination has-value_wf_base value-type-has-value int_subtype_base set_subtype_base partial_subtype_base istype-nat null_wf null-map tupletype_cons_lemma map_cons_lemma int_term_value_add_lemma int_term_value_subtract_lemma itermAdd_wf itermSubtract_wf subtract_wf decidable__equal_int spread_cons_lemma int_formula_prop_eq_lemma intformeq_wf subtype_base_sq subtract-1-ge-0 istype-le int_formula_prop_not_lemma intformnot_wf decidable__le colength_wf_list colength-cons-not-zero product_subtype_list unit_wf2 nil_wf tupletype_nil_lemma map_nil_lemma list-cases ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf full-omega-unsat nat_properties bool_subtype_base bool_wf null_cons_lemma subtype_partial_sqtype_base add-zero l_sum_cons_lemma l_sum_nil_lemma cons_wf partial_wf l_sum-wf-partial-nat null_nil_lemma subtype_rel-equal btrue_neq_bfalse nat-partial-nat istype-false add-wf-partial-nat select-map subtype_rel_tuple-type map-length length_wf_nat int_seg_wf subtype_rel_list top_wf select_wf int_seg_properties decidable__lt is-exception_wf subtype_rel_dep_function add-has-value-iff sq_stable__has-value iff_weakening_equal subtype_rel_self add_functionality_wrt_eq istype-base true_wf squash_wf zero-add
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination sqequalRule independent_pairFormation Error :lambdaEquality_alt,  Error :universeIsType,  applyEquality Error :inhabitedIsType,  Error :productIsType,  Error :setIsType,  natural_numberEquality instantiate unionEquality cumulativity universeEquality equalityTransitivity equalitySymmetry Error :lambdaFormation_alt,  unionElimination Error :equalityIstype,  independent_functionElimination Error :unionIsType,  setElimination rename productElimination independent_pairEquality axiomEquality Error :functionIsType,  Error :dependent_pairEquality_alt,  atomEquality setEquality applyLambdaEquality productEquality because_Cache intEquality independent_isectElimination Error :dependent_set_memberEquality_alt,  voidElimination Error :isect_memberEquality_alt,  closedConclusion baseApply baseClosed callbyvalueAdd equalityElimination imageElimination hypothesis_subsumption promote_hyp sqequalBase Error :functionIsTypeImplies,  int_eqEquality Error :dependent_pairFormation_alt,  approximateComputation intWeakElimination addEquality sqleReflexivity divergentSqle axiomSqleEquality imageMemberEquality

Latex:
\mforall{}[P:Type].  \mforall{}[a:Atom  {}\mrightarrow{}  P  {}\mrightarrow{}  ((P  +  P  +  Type)  List)].  \mforall{}[i:P].
prec(lbl,p.a[lbl;p];i)  \mequiv{}  labl:\{lbl:Atom|  0  <  ||a[lbl;i]||\}    \mtimes{}  tuple-type(map(\mlambda{}x.case  x
of  inl(y)  =>
case  y
of  inl(p)  =>
prec(lbl,p.a[lbl;p];p)
|  inr(p)  =>
prec(lbl,p.a[lbl;p];p)  List
|  inr(E)  =>
E;a[labl;i]))

Date html generated: 2019_06_20-PM-02_04_53
Last ObjectModification: 2019_03_28-PM-02_51_54

Theory : tuples

Home Index