### Nuprl Lemma : append_functionality_wrt_permutation

`∀[A:Type]`
`  ∀as1,as2,bs1,bs2:A List.  (permutation(A;as1;bs1) `` permutation(A;as2;bs2) `` permutation(A;as1 @ as2;bs1 @ bs2))`

Proof

Definitions occuring in Statement :  permutation: `permutation(T;L1;L2)` append: `as @ bs` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uimplies: `b supposing a` permutation: `permutation(T;L1;L2)` exists: `∃x:A. B[x]` and: `P ∧ Q` prop: `ℙ` top: `Top` int_seg: `{i..j-}` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` guard: `{T}` not: `¬A` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` subtype_rel: `A ⊆r B` less_than: `a < b` le: `A ≤ B` lelt: `i ≤ j < k` less_than': `less_than'(a;b)` inject: `Inj(A;B;f)` nat: `ℕ` squash: `↓T` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` true: `True` cand: `A c∧ B`
Lemmas referenced :  permutation-length permutation_wf list_wf length-append bnot_wf le_wf le_int_wf less_than_wf assert_wf equal-wf-T-base bool_wf length_wf lt_int_wf uiff_transitivity eqtt_to_assert assert_of_lt_int eqff_to_assert assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int equal_wf int_formula_prop_wf int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermConstant_wf itermAdd_wf itermVar_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le int_seg_properties non_neg_length int_seg_subtype lelt_wf int_seg_wf int_formula_prop_eq_lemma intformeq_wf add-member-int_seg1 int_formula_prop_less_lemma intformless_wf decidable__lt int_term_value_subtract_lemma itermSubtract_wf subtract_wf inject_wf append_wf permute_list_wf subtype_rel_function false_wf length_append subtype_rel_list top_wf full-omega-unsat nat_properties length_wf_nat decidable__equal_int add-is-int-iff list_extensionality nat_wf iff_weakening_equal add_functionality_wrt_eq true_wf squash_wf permute_list_length select_wf permute_list_select subtype_rel_self select_append_front select_append_back and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis because_Cache productElimination universeEquality isect_memberEquality voidElimination voidEquality sqequalRule lambdaEquality baseClosed equalitySymmetry equalityTransitivity cumulativity rename setElimination unionElimination equalityElimination independent_functionElimination dependent_functionElimination computeAll intEquality int_eqEquality dependent_pairFormation applyLambdaEquality addEquality independent_pairFormation dependent_set_memberEquality natural_numberEquality functionExtensionality applyEquality productEquality approximateComputation imageElimination closedConclusion baseApply promote_hyp pointwiseFunctionality imageMemberEquality instantiate hyp_replacement

Latex:
\mforall{}[A:Type]
\mforall{}as1,as2,bs1,bs2:A  List.
(permutation(A;as1;bs1)  {}\mRightarrow{}  permutation(A;as2;bs2)  {}\mRightarrow{}  permutation(A;as1  @  as2;bs1  @  bs2))

Date html generated: 2019_06_20-PM-01_37_49
Last ObjectModification: 2018_08_21-PM-11_00_37

Theory : list_1

Home Index