Nuprl Lemma : tree-secures_wf

[T:Type]. ∀[p:wfd-tree(T)]. ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ].  (tree-secures(T;A;p) ∈ ℙ)


Proof




Definitions occuring in Statement :  tree-secures: tree-secures(T;A;p) wfd-tree: wfd-tree(T) int_seg: {i..j-} nat: uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T wfd-tree: wfd-tree(T) all: x:A. B[x] nat: prop: tree-secures: tree-secures(T;A;p) Wsup: Wsup(a;b) implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  so_lambda: λ2x.t[x] le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A so_apply: x[s] bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b subtype_rel: A ⊆B pcw-pp-barred: Barred(pp) int_seg: {i..j-} lelt: i ≤ j < k ge: i ≥  decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top cw-step: cw-step(A;a.B[a]) pcw-step: pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]) spreadn: spread3 less_than: a < b true: True squash: T isr: isr(x) ext-eq: A ≡ B so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] ext-family: F ≡ G pi1: fst(t) nat_plus: + W-rel: W-rel(A;a.B[a];w) param-W-rel: param-W-rel(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];par;w) pcw-steprel: StepRel(s1;s2) pi2: snd(t) isl: isl(x) pcw-step-agree: StepAgree(s;p1;w) cand: c∧ B
Lemmas referenced :  nat_wf int_seg_wf wfd-tree_wf bool_wf eqtt_to_assert all_wf false_wf le_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot predicate-or-shift_wf W-elimination-facts ifthenelse_wf subtract_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf decidable__lt lelt_wf top_wf less_than_wf true_wf add-subtract-cancel itermAdd_wf int_term_value_add_lemma W-ext param-co-W-ext unit_wf2 it_wf param-co-W_wf ext-eq_inversion subtype_rel_weakening assert_wf btrue_wf bfalse_wf pcw-steprel_wf subtype_rel_dep_function set_subtype_base int_subtype_base decidable__equal_int intformeq_wf int_formula_prop_eq_lemma int_seg_subtype
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin sqequalHypSubstitution dependent_functionElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry sqequalRule axiomEquality functionEquality cumulativity extract_by_obid isectElimination natural_numberEquality setElimination rename universeEquality isect_memberEquality because_Cache lambdaFormation unionElimination equalityElimination productElimination independent_isectElimination lambdaEquality applyEquality functionExtensionality dependent_set_memberEquality independent_pairFormation dependent_pairFormation promote_hyp instantiate independent_functionElimination voidElimination voidEquality strong_bar_Induction int_eqEquality intEquality computeAll lessCases sqequalAxiom imageMemberEquality baseClosed imageElimination addEquality int_eqReduceTrueSq hypothesis_subsumption dependent_pairEquality productEquality inlEquality unionEquality hyp_replacement applyLambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}[p:wfd-tree(T)].  \mforall{}[A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}].    (tree-secures(T;A;p)  \mmember{}  \mBbbP{})



Date html generated: 2017_04_17-AM-09_36_11
Last ObjectModification: 2017_02_27-PM-05_34_42

Theory : fan-theorem


Home Index