Nuprl Lemma : assert-wf-mkterm
∀[opr:Type]
  ∀sort:term(opr) ⟶ ℕ. ∀arity:opr ⟶ ((ℕ × ℕ) List). ∀f:opr. ∀bts:(varname() List × term(opr)) List.
    uiff(↑wf-term(arity;sort;mkterm(f;bts));(||bts|| = ||arity f|| ∈ ℤ)
    ∧ (∀i:ℕ||bts||
         ((||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ)
         ∧ ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ)
         ∧ (↑wf-term(arity;sort;snd(bts[i]))))))
Proof
Error : references
Latex:
\mforall{}[opr:Type]
    \mforall{}sort:term(opr)  {}\mrightarrow{}  \mBbbN{}.  \mforall{}arity:opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List).  \mforall{}f:opr.
    \mforall{}bts:(varname()  List  \mtimes{}  term(opr))  List.
        uiff(\muparrow{}wf-term(arity;sort;mkterm(f;bts));(||bts||  =  ||arity  f||)
        \mwedge{}  (\mforall{}i:\mBbbN{}||bts||
                  ((||fst(bts[i])||  =  (fst(arity  f[i])))
                  \mwedge{}  ((sort  (snd(bts[i])))  =  (snd(arity  f[i])))
                  \mwedge{}  (\muparrow{}wf-term(arity;sort;snd(bts[i]))))))
Date html generated:
2020_05_19-PM-09_58_18
Last ObjectModification:
2020_03_09-PM-04_10_15
Theory : terms
Home
Index