---

Step * of Lemma alpha-aux-mkterm

No Annotations
∀[opr:Type]
  ∀a,b:opr. ∀as,bs:bound-term(opr) List. ∀vs,ws:varname() List.
    (alpha-aux(opr;vs;ws;mkterm(a;as);mkterm(b;bs))
    ⇐⇒ (a = b ∈ opr)
        ∧ (||as|| = ||bs|| ∈ ℤ)
        ∧ (∀i:ℕ||as||
             (alpha-aux(opr;rev(fst(as[i])) + vs;rev(fst(bs[i])) + ws;snd(as[i]);snd(bs[i]))
             ∧ (||fst(as[i])|| = ||fst(bs[i])|| ∈ ℤ))))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN InductionOnList
   THEN Intros
   THEN RW (AddrC [1] (UnfoldC `alpha-aux`)) 0
   THEN RepUR ``mkterm`` 0
   THEN (((DVar `u' THEN DVar `u1' THEN Reduce 0)
          THEN Fold `mkterm` 0
          THEN (RW assert_pushdownC 0 THENA Auto)
          THEN RWO "7" 0
          THEN Auto)
   ORELSE (Try ((Assert 0 ≤ ||v|| BY Auto)) THEN Try (RW  assert_pushdownC 0) THEN Auto)
   )
   THEN ((((D -1 With ⌜0⌝  THENA Auto) THEN Reduce -1 THEN D -1 THEN Trivial)
         ORELSE ((D -2 With ⌜i + 1⌝  THENA Complete (Auto)) THEN RWO  "select_cons_tl" (-1) THEN Auto)
         )
   ORELSE (CaseNat 0 `i' THEN Reduce 0 THEN (Trivial ORELSE (RWO "select_cons_tl" 0 THEN Auto)))
   )) }

1
1. [opr] : Type
2. a : opr
3. b : opr
4. u2 : varname() List
5. u3 : term(opr)
6. v : bound-term(opr) List
7. ∀bs:bound-term(opr) List. ∀vs,ws:varname() List.
     (alpha-aux(opr;vs;ws;mkterm(a;v);mkterm(b;bs))
     ⇐⇒ (a = b ∈ opr)
         ∧ (||v|| = ||bs|| ∈ ℤ)
         ∧ (∀i:ℕ||v||
              (alpha-aux(opr;rev(fst(v[i])) + vs;rev(fst(bs[i])) + ws;snd(v[i]);snd(bs[i]))
              ∧ (||fst(v[i])|| = ||fst(bs[i])|| ∈ ℤ))))
8. u4 : varname() List
9. u5 : term(opr)
10. v1 : bound-term(opr) List
11. ∀vs,ws:varname() List.
      (alpha-aux(opr;vs;ws;mkterm(a;[<u2, u3> / v]);mkterm(b;v1))
      ⇐⇒ (a = b ∈ opr)
          ∧ ((||v|| + 1) = ||v1|| ∈ ℤ)
          ∧ (∀i:ℕ||v|| + 1
               (alpha-aux(opr;rev(fst([<u2, u3> / v][i])) + vs;rev(fst(v1[i])) + ws;snd([<u2, u3> / v][i]);snd(v1[i]))
               ∧ (||fst([<u2, u3> / v][i])|| = ||fst(v1[i])|| ∈ ℤ))))
12. vs : varname() List
13. ws : varname() List
14. a = b ∈ opr
15. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
16. i : ℕ||v||
17. alpha-aux(opr;rev(fst(v[(i + 1) - 1])) + vs;rev(fst(v1[(i + 1) - 1])) + ws;snd(v[(i + 1) - 1]);snd(v1[(i + 1) - 1]))
18. ||fst(v[(i + 1) - 1])|| = ||fst(v1[(i + 1) - 1])|| ∈ ℤ
⊢ alpha-aux(opr;rev(fst(v[i])) + vs;rev(fst(v1[i])) + ws;snd(v[i]);snd(v1[i]))

2
1. opr : Type
2. a : opr
3. b : opr
4. u2 : varname() List
5. u3 : term(opr)
6. v : bound-term(opr) List
7. ∀bs:bound-term(opr) List. ∀vs,ws:varname() List.
     (alpha-aux(opr;vs;ws;mkterm(a;v);mkterm(b;bs))
     ⇐⇒ (a = b ∈ opr)
         ∧ (||v|| = ||bs|| ∈ ℤ)
         ∧ (∀i:ℕ||v||
              (alpha-aux(opr;rev(fst(v[i])) + vs;rev(fst(bs[i])) + ws;snd(v[i]);snd(bs[i]))
              ∧ (||fst(v[i])|| = ||fst(bs[i])|| ∈ ℤ))))
8. u4 : varname() List
9. u5 : term(opr)
10. v1 : bound-term(opr) List
11. ∀vs,ws:varname() List.
      (alpha-aux(opr;vs;ws;mkterm(a;[<u2, u3> / v]);mkterm(b;v1))
      ⇐⇒ (a = b ∈ opr)
          ∧ ((||v|| + 1) = ||v1|| ∈ ℤ)
          ∧ (∀i:ℕ||v|| + 1
               (alpha-aux(opr;rev(fst([<u2, u3> / v][i])) + vs;rev(fst(v1[i])) + ws;snd([<u2, u3> / v][i]);snd(v1[i]))
               ∧ (||fst([<u2, u3> / v][i])|| = ||fst(v1[i])|| ∈ ℤ))))
12. vs : varname() List
13. ws : varname() List
14. a = b ∈ opr
15. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
16. i : ℕ||v||
17. alpha-aux(opr;rev(fst(v[(i + 1) - 1])) + vs;rev(fst(v1[(i + 1) - 1])) + ws;snd(v[(i + 1) - 1]);snd(v1[(i + 1) - 1]))
18. ||fst(v[(i + 1) - 1])|| = ||fst(v1[(i + 1) - 1])|| ∈ ℤ
⊢ ||fst(v[i])|| = ||fst(v1[i])|| ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}a,b:opr.  \mforall{}as,bs:bound-term(opr)  List.  \mforall{}vs,ws:varname()  List.
        (alpha-aux(opr;vs;ws;mkterm(a;as);mkterm(b;bs))
        \mLeftarrow{}{}\mRightarrow{}  (a  =  b)
                \mwedge{}  (||as||  =  ||bs||)
                \mwedge{}  (\mforall{}i:\mBbbN{}||as||
                          (alpha-aux(opr;rev(fst(as[i]))  +  vs;rev(fst(bs[i]))  +  ws;snd(as[i]);snd(bs[i]))
                          \mwedge{}  (||fst(as[i])||  =  ||fst(bs[i])||))))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  InductionOnList
  THEN  Intros
  THEN  RW  (AddrC  [1]  (UnfoldC  `alpha-aux`))  0
  THEN  RepUR  ``mkterm``  0
  THEN  (((DVar  `u'  THEN  DVar  `u1'  THEN  Reduce  0)
                THEN  Fold  `mkterm`  0
                THEN  (RW  assert\_pushdownC  0  THENA  Auto)
                THEN  RWO  "7"  0
                THEN  Auto)
  ORELSE  (Try  ((Assert  0  \mleq{}  ||v||  BY  Auto))  THEN  Try  (RW    assert\_pushdownC  0)  THEN  Auto)
  )
  THEN  ((((D  -1  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto)  THEN  Reduce  -1  THEN  D  -1  THEN  Trivial)
              ORELSE  ((D  -2  With  \mkleeneopen{}i  +  1\mkleeneclose{}    THENA  Complete  (Auto))  THEN  RWO    "select\_cons\_tl"  (-1)  THEN  Auto)
              )
  ORELSE  (CaseNat  0  `i'  THEN  Reduce  0  THEN  (Trivial  ORELSE  (RWO  "select\_cons\_tl"  0  THEN  Auto)))
  ))

---

Home Index