---

Step * of Lemma subterm-mkterm

No Annotations
∀[opr:Type]
  ∀s:term(opr). ∀f:opr. ∀bts:bound-term(opr) List.
    (s << mkterm(f;bts) ⇐⇒ ∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i])))
BY
{ Auto }

1
1. [opr] : Type
2. s : term(opr)
3. f : opr
4. bts : bound-term(opr) List
5. s << mkterm(f;bts)
⊢ ∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i]))

2
1. [opr] : Type
2. s : term(opr)
3. f : opr
4. bts : bound-term(opr) List
5. ∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i]))
⊢ s << mkterm(f;bts)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}s:term(opr).  \mforall{}f:opr.  \mforall{}bts:bound-term(opr)  List.
        (s  <<  mkterm(f;bts)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||bts||.  ((s  =  (snd(bts[i])))  \mvee{}  s  <<  snd(bts[i])))


By

---

Latex:
Auto

---

Home Index