`∀[A:Type]`
`  ∀i:ℕ. ∀L:A List.`
`    ∃X,Y:A List`
`     ((L = (X @ [L[i]; L[i + 1]] @ Y) ∈ (A List)) ∧ (swap(L;i;i + 1) = (X @ [L[i + 1]; L[i]] @ Y) ∈ (A List))) `
`    supposing i + 1 < ||L||`

Proof

Definitions occuring in Statement :  swap: `swap(L;i;j)` select: `L[n]` length: `||as||` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q` add: `n + m` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` less_than: `a < b` squash: `↓T` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` ge: `i ≥ j ` so_apply: `x[s]` nat: `ℕ` cand: `A c∧ B` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` listp: `A List+` sq_type: `SQType(T)` select: `L[n]` cons: `[a / b]` subtract: `n - m` int_seg: `{i..j-}` lelt: `i ≤ j < k`
Lemmas referenced :  all_wf list_wf isect_wf less_than_wf subtract_wf length_wf exists_wf equal_wf append_wf cons_wf select_wf subtract-add-cancel decidable__le full-omega-unsat 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 nil_wf list_ind_cons_lemma list_ind_nil_lemma length-append length_of_cons_lemma non_neg_length set_wf primrec-wf2 nat_properties itermAdd_wf int_term_value_add_lemma nat_wf member-less_than tl_wf false_wf list_extensionality listp_properties length_tl iff_weakening_equal decidable__equal_int intformeq_wf int_formula_prop_eq_lemma squash_wf true_wf subtype_rel_self subtype_base_sq int_subtype_base select_cons_tl select_tl lelt_wf add-associates add-swap add-commutes zero-add swap_wf swap_length swapped_select and_wf list_decomp hd_wf length_wf_nat swap_cons add-subtract-cancel int_seg_wf le_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin rename setElimination introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesisEquality hypothesis sqequalRule lambdaEquality addEquality natural_numberEquality because_Cache productEquality independent_isectElimination dependent_functionElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation imageElimination productElimination applyLambdaEquality equalityTransitivity equalitySymmetry universeEquality applyEquality imageMemberEquality baseClosed dependent_set_memberEquality instantiate minusEquality hyp_replacement

Latex:
\mforall{}[A:Type]
\mforall{}i:\mBbbN{}.  \mforall{}L:A  List.
\mexists{}X,Y:A  List
((L  =  (X  @  [L[i];  L[i  +  1]]  @  Y))  \mwedge{}  (swap(L;i;i  +  1)  =  (X  @  [L[i  +  1];  L[i]]  @  Y)))
supposing  i  +  1  <  ||L||

Date html generated: 2018_05_21-PM-06_21_09
Last ObjectModification: 2018_05_19-PM-05_34_38

Theory : list!

Home Index