### Nuprl Lemma : decidable-last-rel

`∀[T:Type]. ∀[P:(T List) ⟶ T ⟶ ℙ].`
`  ((∀L:T List. ∀x:T.  Dec(P[L;x])) `` (∀L:T List. Dec(∃L':T List. ∃x:T. ((L = (L' @ [x]) ∈ (T List)) ∧ P[L';x]))))`

Proof

Definitions occuring in Statement :  append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` uimplies: `b supposing a` top: `Top` decidable: `Dec(P)` or: `P ∨ Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` so_apply: `x[s]` guard: `{T}` not: `¬A` false: `False` exists: `∃x:A. B[x]` and: `P ∧ Q` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` uiff: `uiff(P;Q)` cons: `[a / b]` bfalse: `ff` cand: `A c∧ B` int_seg: `{i..j-}` lelt: `i ≤ j < k` ge: `i ≥ j ` le: `A ≤ B` satisfiable_int_formula: `satisfiable_int_formula(fmla)` sq_type: `SQType(T)` squash: `↓T` true: `True` iff: `P `⇐⇒` Q`
Lemmas referenced :  decidable__assert null_wf3 subtype_rel_list top_wf list_wf all_wf decidable_wf list-cases null_nil_lemma btrue_wf null_cons_lemma bfalse_wf append_is_nil cons_wf nil_wf and_wf equal_wf btrue_neq_bfalse product_subtype_list exists_wf append_wf length_wf length-append last_lemma last_wf not_wf last_singleton_append assert_elim not_assert_elim assert_wf firstn_append non_neg_length decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma lelt_wf firstn_length firstn_wf subtype_base_sq int_subtype_base squash_wf true_wf length_append iff_weakening_equal length_of_cons_lemma length_of_nil_lemma decidable__equal_int add-is-int-iff intformeq_wf int_formula_prop_eq_lemma false_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination hypothesisEquality applyEquality hypothesis independent_isectElimination lambdaEquality isect_memberEquality voidElimination voidEquality because_Cache sqequalRule unionElimination cumulativity functionExtensionality functionEquality universeEquality inrFormation productElimination equalitySymmetry dependent_set_memberEquality independent_pairFormation equalityTransitivity applyLambdaEquality setElimination rename independent_functionElimination promote_hyp hypothesis_subsumption productEquality inlFormation dependent_pairFormation addLevel hyp_replacement levelHypothesis natural_numberEquality int_eqEquality intEquality computeAll addEquality instantiate imageElimination imageMemberEquality baseClosed pointwiseFunctionality baseApply closedConclusion

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}L:T  List.  \mforall{}x:T.    Dec(P[L;x]))
{}\mRightarrow{}  (\mforall{}L:T  List.  Dec(\mexists{}L':T  List.  \mexists{}x:T.  ((L  =  (L'  @  [x]))  \mwedge{}  P[L';x]))))

Date html generated: 2018_05_21-PM-07_21_22
Last ObjectModification: 2017_07_26-PM-05_05_16

Theory : general

Home Index