Nuprl Lemma : hd_two_swap_permr

T:Type. ∀as:T List. ∀a,a':T.  ([a; [a' as]] ≡(T) [a'; [a as]])


Proof




Definitions occuring in Statement :  permr: as ≡(T) bs cons: [a b] list: List all: x:A. B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] permr: as ≡(T) bs member: t ∈ T top: Top uall: [x:A]. B[x] cand: c∧ B exists: x:A. B[x] nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: guard: {T} ge: i ≥  decidable: Dec(P) or: P ∨ Q uiff: uiff(P;Q) uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) int_seg: {i..j-} lelt: i ≤ j < k txpose_perm: txpose_perm mk_perm: mk_perm(f;b) perm_f: p.f pi1: fst(t) sym_grp: Sym(n) perm: Perm(T) subtype_rel: A ⊆B less_than: a < b squash: T swap: swap(i;j) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  select: L[n] cons: [a b] subtract: m bfalse: ff so_lambda: λ2x.t[x] so_apply: x[s] sq_type: SQType(T) bnot: ¬bb assert: b nequal: a ≠ b ∈  true: True iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  length_of_cons_lemma istype-void length_wf istype-universe list_wf txpose_perm_wf add_nat_wf length_wf_nat istype-false le_wf nat_properties decidable__le add-is-int-iff full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf istype-int 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_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_wf false_wf non_neg_length decidable__lt intformless_wf int_formula_prop_less_lemma less_than_wf int_seg_wf select_wf cons_wf perm_f_wf int_seg_properties eq_int_wf eqtt_to_assert assert_of_eq_int select-cons-hd eqff_to_assert set_subtype_base lelt_wf int_subtype_base bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int equal_wf squash_wf true_wf subtype_rel_self iff_weakening_equal subtract_wf itermSubtract_wf int_term_value_subtract_lemma select_cons_tl
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalRule cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality_alt voidElimination hypothesis addEquality isectElimination hypothesisEquality natural_numberEquality independent_pairFormation inhabitedIsType universeIsType universeEquality dependent_pairFormation_alt dependent_set_memberEquality_alt equalityTransitivity equalitySymmetry because_Cache applyLambdaEquality setElimination rename unionElimination pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed productElimination independent_isectElimination approximateComputation independent_functionElimination lambdaEquality_alt int_eqEquality equalityIsType1 productIsType functionIsType applyEquality imageElimination equalityElimination equalityIsType2 intEquality instantiate cumulativity productEquality imageMemberEquality

Latex:
\mforall{}T:Type.  \mforall{}as:T  List.  \mforall{}a,a':T.    ([a;  [a'  /  as]]  \mequiv{}(T)  [a';  [a  /  as]])



Date html generated: 2019_10_16-PM-01_00_53
Last ObjectModification: 2018_10_08-AM-10_05_56

Theory : perms_2


Home Index