---

Step * of Lemma term-ind_wf_wfterm

No Annotations
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[P:wfterm(opr;sort;arity) ⟶ ℙ].
∀[varcase:∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)]].
∀[mktermcase:∀f:opr. ∀bts:wf-bound-terms(opr;sort;arity;f).  ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkwfterm(f;bts)])].
∀[t:wfterm(opr;sort;arity)].
  (term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t) ∈ P[t])
BY
{ (Intros
   THEN Unhide
   THEN RenameVar `v' 5
   THEN RenameVar `m' 6
   THEN (InstLemma `term-ind_wf` [⌜opr⌝;⌜λ2t.P[t] supposing ↑wf-term(arity;sort;t)⌝]⋅ THENA Auto)
   THEN BHyp -1
   THEN ((RepeatFor 3 ((MemCD THENL [Id; Auto])) THEN Unfold `uimplies` 0 THEN (MemCD THENW Auto)) ORELSE Auto)
   THEN (Assert mkterm(f;bts) ∈ wfterm(opr;sort;arity) BY
               (MemTypeCD THEN Auto))
   THEN (Subst' bts ~ wfbts(mkterm(f;bts)) 0 THENA Computation)
   THEN (Subst' bts ~ wfbts(mkterm(f;bts)) -3 THENA Computation)
   THEN All (RepUR ``all``)
   THEN Auto
   THEN (FunExt THENA Auto)
   THEN DoSubsume
   THEN Auto) }

1
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])]

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[sort:term(opr)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[arity:opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)].
\mforall{}[P:wfterm(opr;sort;arity)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[varcase:\mforall{}v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  .  P[varterm(v)]].
\mforall{}[mktermcase:\mforall{}f:opr.  \mforall{}bts:wf-bound-terms(opr;sort;arity;f).
                              ((\mforall{}i:\mBbbN{}||bts||.  P[snd(bts[i])])  {}\mRightarrow{}  P[mkwfterm(f;bts)])].  \mforall{}[t:wfterm(opr;sort;arity)].
    (term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t)  \mmember{}  P[t])


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  RenameVar  `v'  5
  THEN  RenameVar  `m'  6
  THEN  (InstLemma  `term-ind\_wf`  [\mkleeneopen{}opr\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}t.P[t]  supposing  \muparrow{}wf-term(arity;sort;t)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1
  THEN  ((RepeatFor  3  ((MemCD  THENL  [Id;  Auto]))  THEN  Unfold  `uimplies`  0  THEN  (MemCD  THENW  Auto))
  ORELSE  Auto
  )
  THEN  (Assert  mkterm(f;bts)  \mmember{}  wfterm(opr;sort;arity)  BY
                          (MemTypeCD  THEN  Auto))
  THEN  (Subst'  bts  \msim{}  wfbts(mkterm(f;bts))  0  THENA  Computation)
  THEN  (Subst'  bts  \msim{}  wfbts(mkterm(f;bts))  -3  THENA  Computation)
  THEN  All  (RepUR  ``all``)
  THEN  Auto
  THEN  (FunExt  THENA  Auto)
  THEN  DoSubsume
  THEN  Auto)

---

Home Index