### Nuprl Lemma : prec-sub_wf

`∀[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)].`
`  (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: `prec(lbl,p.a[lbl; p];i)` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` member: `t ∈ T` function: `x:A ⟶ B[x]` union: `left + right` atom: `Atom` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` prec-sub: `prec-sub(P;lbl,p.a[lbl; p];j;x;i;y)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` let: let prec-arg-types: `prec-arg-types(lbl,p.a[lbl; p];i;lbl)` prop: `ℙ` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` int_seg: `{i..j-}` lelt: `i ≤ j < k` less_than: `a < b` squash: `↓T` cand: `A c∧ B` top: `Top` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` isl: `isl(x)` outl: `outl(x)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff`
Lemmas referenced :  dest-prec_wf istype-atom int_seg_wf length_wf select-tuple_wf map_wf prec_wf list_wf int_seg_subtype_nat istype-false map-length istype-void int_seg_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermVar_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_formula_prop_wf select-map subtype_rel_list top_wf assert_wf or_wf equal_wf select_wf decidable__le intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma true_wf bfalse_wf btrue_wf btrue_neq_bfalse l_member_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule Error :lambdaEquality_alt,  applyEquality Error :inhabitedIsType,  hypothesis Error :lambdaFormation_alt,  productElimination setElimination rename productEquality natural_numberEquality instantiate unionEquality cumulativity universeEquality equalityTransitivity equalitySymmetry unionElimination Error :equalityIstype,  dependent_functionElimination independent_functionElimination Error :unionIsType,  independent_isectElimination independent_pairFormation imageElimination Error :isect_memberEquality_alt,  voidElimination approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality Error :universeIsType,  because_Cache applyLambdaEquality Error :inlEquality_alt,  hyp_replacement Error :dependent_set_memberEquality_alt,  Error :productIsType,  Error :inrEquality_alt,  axiomEquality Error :isectIsTypeImplies,  Error :functionIsType

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)].
(prec-sub(P;lbl,p.a[lbl;p];j;x;i;y)  \mmember{}  \mBbbP{})

Date html generated: 2019_06_20-PM-02_05_38
Last ObjectModification: 2019_02_22-PM-07_07_59

Theory : tuples

Home Index