Nuprl Lemma : prec-sub_wf

[P:Type]. ∀[a:Atom ⟶ 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: 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: λ2y.t[x; y] so_apply: x[s1;s2] all: x:A. B[x] implies:  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 ⊆B uimplies: 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: 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 then else 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