---

Step * 2 of Lemma alpha-aux-trans


1. [opr] : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀b,c:term(opr). ∀us,vs,ws:varname() List.
           (alpha-aux(opr;us;vs;snd(bt);b) ⇒ alpha-aux(opr;vs;ws;b;c) ⇒ alpha-aux(opr;us;ws;snd(bt);c))))
4. f : opr
5. b1 : bound-term(opr) List
6. ∀bt:bound-term(opr)
     ((bt ∈ b1)
     ⇒ (∀c:term(opr). ∀us,vs,ws:varname() List.
           (alpha-aux(opr;us;vs;mkterm(f;bts);snd(bt))
           ⇒ alpha-aux(opr;vs;ws;snd(bt);c)
           ⇒ alpha-aux(opr;us;ws;mkterm(f;bts);c))))
7. f1 : opr
8. b2 : bound-term(opr) List
9. ∀bt:bound-term(opr)
     ((bt ∈ b2)
     ⇒ (∀us,vs,ws:varname() List.
           (alpha-aux(opr;us;vs;mkterm(f;bts);mkterm(f1;b1))
           ⇒ alpha-aux(opr;vs;ws;mkterm(f1;b1);snd(bt))
           ⇒ alpha-aux(opr;us;ws;mkterm(f;bts);snd(bt)))))
10. f2 : opr
11. us : varname() List
12. vs : varname() List
13. ws : varname() List
14. alpha-aux(opr;us;vs;mkterm(f;bts);mkterm(f1;b1))
15. alpha-aux(opr;vs;ws;mkterm(f1;b1);mkterm(f2;b2))
⊢ alpha-aux(opr;us;ws;mkterm(f;bts);mkterm(f2;b2))
BY
{ ((All (RWO "alpha-aux-mkterm") THENA Auto)
   THEN ExRepD
   THEN SplitAndConcl
   THEN Try (Eq)
   THEN (ParallelOp -4 THEN (D -3 With ⌜i⌝  THENA Auto))
   THEN ExRepD
   THEN D 0
   THEN Try (Eq)
   THEN FHyp 3 [-4;-2]
   THEN Auto) }

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  bts  :  bound-term(opr)  List
3.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  bts)
          {}\mRightarrow{}  (\mforall{}b,c:term(opr).  \mforall{}us,vs,ws:varname()  List.
                      (alpha-aux(opr;us;vs;snd(bt);b)
                      {}\mRightarrow{}  alpha-aux(opr;vs;ws;b;c)
                      {}\mRightarrow{}  alpha-aux(opr;us;ws;snd(bt);c))))
4.  f  :  opr
5.  b1  :  bound-term(opr)  List
6.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  b1)
          {}\mRightarrow{}  (\mforall{}c:term(opr).  \mforall{}us,vs,ws:varname()  List.
                      (alpha-aux(opr;us;vs;mkterm(f;bts);snd(bt))
                      {}\mRightarrow{}  alpha-aux(opr;vs;ws;snd(bt);c)
                      {}\mRightarrow{}  alpha-aux(opr;us;ws;mkterm(f;bts);c))))
7.  f1  :  opr
8.  b2  :  bound-term(opr)  List
9.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  b2)
          {}\mRightarrow{}  (\mforall{}us,vs,ws:varname()  List.
                      (alpha-aux(opr;us;vs;mkterm(f;bts);mkterm(f1;b1))
                      {}\mRightarrow{}  alpha-aux(opr;vs;ws;mkterm(f1;b1);snd(bt))
                      {}\mRightarrow{}  alpha-aux(opr;us;ws;mkterm(f;bts);snd(bt)))))
10.  f2  :  opr
11.  us  :  varname()  List
12.  vs  :  varname()  List
13.  ws  :  varname()  List
14.  alpha-aux(opr;us;vs;mkterm(f;bts);mkterm(f1;b1))
15.  alpha-aux(opr;vs;ws;mkterm(f1;b1);mkterm(f2;b2))
\mvdash{}  alpha-aux(opr;us;ws;mkterm(f;bts);mkterm(f2;b2))


By

---

Latex:
((All  (RWO  "alpha-aux-mkterm")  THENA  Auto)
  THEN  ExRepD
  THEN  SplitAndConcl
  THEN  Try  (Eq)
  THEN  (ParallelOp  -4  THEN  (D  -3  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto))
  THEN  ExRepD
  THEN  D  0
  THEN  Try  (Eq)
  THEN  FHyp  3  [-4;-2]
  THEN  Auto)

---

Home Index