---

Step * 2 2 1 1 1 1 of Lemma term-opr_functionality


1. opr : Type
2. t : term(opr)
3. t' : term(opr)
4. ¬↑isvarterm(t)
5. alpha-eq-terms(opr;t;t')
6. f1 : opr
7. b1 : {bt:bound-term(opr)| bound-term-size(bt) < term-size(t)}  List
8. f : opr
9. bts : {bt:bound-term(opr)| bound-term-size(bt) < term-size(t')}  List
10. alpha-eq-terms(opr;mkterm(f1;b1);mkterm(f;bts))
⊢ f1 = f ∈ opr
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN ListInd (-2)
   THEN InductionOnList
   THEN RW (AddrC [1] (TagC (mk_tag_term 4))) 0
   THEN Reduce 0
   THEN Try (Fold `alpha-eq-terms` 0)
   THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  t  :  term(opr)
3.  t'  :  term(opr)
4.  \mneg{}\muparrow{}isvarterm(t)
5.  alpha-eq-terms(opr;t;t')
6.  f1  :  opr
7.  b1  :  \{bt:bound-term(opr)|  bound-term-size(bt)  <  term-size(t)\}    List
8.  f  :  opr
9.  bts  :  \{bt:bound-term(opr)|  bound-term-size(bt)  <  term-size(t')\}    List
10.  alpha-eq-terms(opr;mkterm(f1;b1);mkterm(f;bts))
\mvdash{}  f1  =  f


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  ListInd  (-2)
  THEN  InductionOnList
  THEN  RW  (AddrC  [1]  (TagC  (mk\_tag\_term  4)))  0
  THEN  Reduce  0
  THEN  Try  (Fold  `alpha-eq-terms`  0)
  THEN  Auto)

---

Home Index