---

Step * 1 of Lemma term-ind_wf_wfterm


1. opr : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
4. P : wfterm(opr;sort;arity) ⟶ ℙ
5. v : v:{v:varname()| ¬(v = nullvar() ∈ varname())}  ⟶ P[varterm(v)]
6. m : f:opr ⟶ bts:wf-bound-terms(opr;sort;arity;f) ⟶ ((i:ℕ||bts|| ⟶ P[snd(bts[i])]) ⇒ P[mkwfterm(f;bts)])
7. t : wfterm(opr;sort;arity)
8. ∀[varcase:v:{v:varname()| ¬(v = nullvar() ∈ varname())}  ⟶ P[varterm(v)] supposing True].
   ∀[mktermcase:f:opr
                ⟶ bts:(bound-term(opr) List)
                ⟶ ((i:ℕ||bts|| ⟶ P[snd(bts[i])] supposing ↑wf-term(arity;sort;snd(bts[i])))
                   ⇒ P[mkterm(f;bts)] supposing ↑wf-term(arity;sort;mkterm(f;bts)))]. ∀[t:term(opr)].
     (term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t) ∈ P[t] supposing ↑wf-term(arity;sort;t))
9. f : opr
10. bts : bound-term(opr) List
11. r : i:ℕ||wfbts(mkterm(f;bts))|| ⟶ P[snd(wfbts(mkterm(f;bts))[i])] 
                                       supposing ↑wf-term(arity;sort;snd(wfbts(mkterm(f;bts))[i]))
12. ↑wf-term(arity;sort;mkterm(f;bts))
13. mkterm(f;bts) ∈ wfterm(opr;sort;arity)
14. i : ℕ||wfbts(mkterm(f;bts))||
15. (r i) = (r i) ∈ P[snd(wfbts(mkterm(f;bts))[i])] supposing ↑wf-term(arity;sort;snd(wfbts(mkterm(f;bts))[i]))
⊢ P[snd(wfbts(mkterm(f;bts))[i])] supposing ↑wf-term(arity;sort;snd(wfbts(mkterm(f;bts))[i]))
    ⊆r P[snd(wfbts(mkterm(f;bts))[i])]
BY
{ ((Subst' wf-term(arity;sort;snd(wfbts(mkterm(f;bts))[i])) ~ tt 0
    THENA ((GenConclTerm ⌜wfbts(mkterm(f;bts))[i]⌝⋅ THENA Auto) THEN RepeatFor 2 (D -2) THEN Reduce 0 THEN Auto)
    )
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  sort  :  term(opr)  {}\mrightarrow{}  \mBbbN{}
3.  arity  :  opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)
4.  P  :  wfterm(opr;sort;arity)  {}\mrightarrow{}  \mBbbP{}
5.  v  :  v:\{v:varname()|  \mneg{}(v  =  nullvar())\}    {}\mrightarrow{}  P[varterm(v)]
6.  m  :  f:opr
{}\mrightarrow{}  bts:wf-bound-terms(opr;sort;arity;f)
{}\mrightarrow{}  ((i:\mBbbN{}||bts||  {}\mrightarrow{}  P[snd(bts[i])])  {}\mRightarrow{}  P[mkwfterm(f;bts)])
7.  t  :  wfterm(opr;sort;arity)
8.  \mforall{}[varcase:v:\{v:varname()|  \mneg{}(v  =  nullvar())\}    {}\mrightarrow{}  P[varterm(v)]  supposing  True].
      \mforall{}[mktermcase:f:opr
                                {}\mrightarrow{}  bts:(bound-term(opr)  List)
                                {}\mrightarrow{}  ((i:\mBbbN{}||bts||  {}\mrightarrow{}  P[snd(bts[i])]  supposing  \muparrow{}wf-term(arity;sort;snd(bts[i])))
                                      {}\mRightarrow{}  P[mkterm(f;bts)]  supposing  \muparrow{}wf-term(arity;sort;mkterm(f;bts)))].
      \mforall{}[t:term(opr)].
          (term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t)  \mmember{}  P[t]  supposing  \muparrow{}wf-term(arity;sort;t))
9.  f  :  opr
10.  bts  :  bound-term(opr)  List
11.  r  :  i:\mBbbN{}||wfbts(mkterm(f;bts))||  {}\mrightarrow{}  P[snd(wfbts(mkterm(f;bts))[i])] 
                                                                              supposing  \muparrow{}wf-term(arity;sort;snd(wfbts(mkterm(f;bts))[i]))
12.  \muparrow{}wf-term(arity;sort;mkterm(f;bts))
13.  mkterm(f;bts)  \mmember{}  wfterm(opr;sort;arity)
14.  i  :  \mBbbN{}||wfbts(mkterm(f;bts))||
15.  (r  i)  =  (r  i)
\mvdash{}  P[snd(wfbts(mkterm(f;bts))[i])]  supposing  \muparrow{}wf-term(arity;sort;snd(wfbts(mkterm(f;bts))[i]))
        \msubseteq{}r  P[snd(wfbts(mkterm(f;bts))[i])]


By

---

Latex:
((Subst'  wf-term(arity;sort;snd(wfbts(mkterm(f;bts))[i]))  \msim{}  tt  0
    THENA  ((GenConclTerm  \mkleeneopen{}wfbts(mkterm(f;bts))[i]\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  RepeatFor  2  (D  -2)
                  THEN  Reduce  0
                  THEN  Auto)
    )
  THEN  Reduce  0
  THEN  Auto)

---

Home Index