Nuprl Lemma : prec-ext

[P:Type]. ∀[a:Atom ⟶ 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: 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 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 ⊆B so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] implies:  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: supposing a top: Top has-value: (a)↓ bfalse: ff ifthenelse: if then else 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 ≥  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: 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: ⇐⇒ 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