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