---

Step * 1 of Lemma swapped_select


1. T : Type
2. L1 : T List
3. L2 : T List
4. i : ℕ||L1||
5. j : ℕ||L1||
6. L2 = swap(L1;i;j) ∈ (T List)
⊢ {(((L2[i] = L1[j] ∈ T) ∧ (L2[j] = L1[i] ∈ T)) ∧ (||L2|| = ||L1|| ∈ ℤ) ∧ (L1 = swap(L2;i;j) ∈ (T List)))
∧ (∀[x:ℕ||L2||]. (L2[x] = L1[x] ∈ T) supposing ((¬(x = j ∈ ℤ)) and (¬(x = i ∈ ℤ))))}
BY
{ (AssertBY ||L2|| = ||L1|| ∈ ℤ    ((HypSubst (-1) 0) THEN Auto THEN BackThruLemma `swap_length` THEN Auto)⋅
   THEN AssertBY L2 = swap(L1;i;j) ∈ {L:T List| ||L|| = ||L1|| ∈ ℤ}      (EqTypeCD THEN Auto)⋅
   THEN Unfold `guard` 0
   THEN Auto
   THEN HypSubst 8 0
   THEN Auto
   THEN Try (((D (-1)) THEN Complete (Auto)))
   THEN Try (((RWO "swap_select" 0 THENA Auto)
              THEN Unfold `flip` 0
              THEN Reduce 0
              THEN Repeat (SplitOnConclITE THEN Auto)⋅
              THEN (HypSubstSq (-1) 0)
              THEN Auto))) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L1  :  T  List
3.  L2  :  T  List
4.  i  :  \mBbbN{}||L1||
5.  j  :  \mBbbN{}||L1||
6.  L2  =  swap(L1;i;j)
\mvdash{}  \{(((L2[i]  =  L1[j])  \mwedge{}  (L2[j]  =  L1[i]))  \mwedge{}  (||L2||  =  ||L1||)  \mwedge{}  (L1  =  swap(L2;i;j)))
\mwedge{}  (\mforall{}[x:\mBbbN{}||L2||].  (L2[x]  =  L1[x])  supposing  ((\mneg{}(x  =  j))  and  (\mneg{}(x  =  i))))\}


By

---

Latex:
(AssertBY  ||L2||  =  ||L1||      ((HypSubst  (-1)  0)
                                                            THEN  Auto
                                                            THEN  BackThruLemma  `swap\_length`
                                                            THEN  Auto)\mcdot{}
  THEN  AssertBY  L2  =  swap(L1;i;j)        (EqTypeCD  THEN  Auto)\mcdot{}
  THEN  Unfold  `guard`  0
  THEN  Auto
  THEN  HypSubst  8  0
  THEN  Auto
  THEN  Try  (((D  (-1))  THEN  Complete  (Auto)))
  THEN  Try  (((RWO  "swap\_select"  0  THENA  Auto)
                        THEN  Unfold  `flip`  0
                        THEN  Reduce  0
                        THEN  Repeat  (SplitOnConclITE  THEN  Auto)\mcdot{}
                        THEN  (HypSubstSq  (-1)  0)
                        THEN  Auto)))

---

Home Index