---

Step * 2 2 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. t = mkterm(f1;b1) ∈ term(opr)
9. f : opr
10. bts : {bt:bound-term(opr)| bound-term-size(bt) < term-size(t')}  List
11. t' = mkterm(f;bts) ∈ term(opr)
⊢ term-opr(mkterm(f1;b1)) = term-opr(mkterm(f;bts)) ∈ opr
BY
{ (RepUR ``term-opr mkterm`` 0 THEN (Assert alpha-eq-terms(opr;mkterm(f1;b1);mkterm(f;bts)) BY Auto)) }

1
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. t = mkterm(f1;b1) ∈ term(opr)
9. f : opr
10. bts : {bt:bound-term(opr)| bound-term-size(bt) < term-size(t')}  List
11. t' = mkterm(f;bts) ∈ term(opr)
12. alpha-eq-terms(opr;mkterm(f1;b1);mkterm(f;bts))
⊢ f1 = f ∈ opr

---

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.  t  =  mkterm(f1;b1)
9.  f  :  opr
10.  bts  :  \{bt:bound-term(opr)|  bound-term-size(bt)  <  term-size(t')\}    List
11.  t'  =  mkterm(f;bts)
\mvdash{}  term-opr(mkterm(f1;b1))  =  term-opr(mkterm(f;bts))


By

---

Latex:
(RepUR  ``term-opr  mkterm``  0  THEN  (Assert  alpha-eq-terms(opr;mkterm(f1;b1);mkterm(f;bts))  BY  Auto))

---

Home Index