---

Step * 1 of Lemma bag-member-implies-hd-append

.....antecedent..... 
1. T : Type
2. L : T List
3. i : ℕ
4. i < ||L||
⊢ permutation(T;L;[L[i] / L\[i]])
BY
{ ((BLemma `permutation_inversion` THENA Auto)
   THEN (BLemma `permutation-cons` THENA Auto)
   THEN (InstLemma `firstn_nth_tl_decomp` [⌜T⌝;⌜L⌝;⌜i⌝]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN InstConcl [⌜firstn(i;L)⌝;⌜nth_tl(1 + i;L)⌝]⋅
   THEN Auto
   THEN Try (Complete ((RWO "-1<" 0 THEN Auto)))
   THEN (BLemma `permutation_weakening` THENA Auto)
   THEN RWO "reject_eq_firstn_nth_tl" 0
   THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  L  :  T  List
3.  i  :  \mBbbN{}
4.  i  <  ||L||
\mvdash{}  permutation(T;L;[L[i]  /  L\mbackslash{}[i]])


By

---

Latex:
((BLemma  `permutation\_inversion`  THENA  Auto)
  THEN  (BLemma  `permutation-cons`  THENA  Auto)
  THEN  (InstLemma  `firstn\_nth\_tl\_decomp`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  InstConcl  [\mkleeneopen{}firstn(i;L)\mkleeneclose{};\mkleeneopen{}nth\_tl(1  +  i;L)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((RWO  "-1<"  0  THEN  Auto)))
  THEN  (BLemma  `permutation\_weakening`  THENA  Auto)
  THEN  RWO  "reject\_eq\_firstn\_nth\_tl"  0
  THEN  Auto)

---

Home Index