---

Step * of Lemma assert-wf-mkterm

No Annotations
∀[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]))))))
BY
{ ((Intros THEN RW  (AddrC [1;1] (UnfoldTopC `wf-term`)) 0)
   THEN Reduce 0
   THEN (GenConcl ⌜(arity f) = ns ∈ ((ℕ × ℕ) List)⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN AutoBoolCase ⌜(||ns|| =z ||bts||)⌝⋅
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN Unfold `l_all` 0
   THEN (Subst' ||zip(ns;bts)|| ~ ||bts|| 0 THENA Auto)
   THEN (RWO "select_zip" 0 THENA Auto)
   THEN Reduce 0
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN ((D -1 THEN ParallelLast) ORELSE ((D 0 THEN Try (Eq)) THEN ParallelLast))
   THEN (MoveToConcl (-1) THEN (GenConclTerm ⌜bts[i]⌝⋅ THENA Auto))
   THEN D -2
   THEN Reduce 0
   THEN RW assert_pushdownC 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\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]))))))


By

---

Latex:
((Intros  THEN  RW    (AddrC  [1;1]  (UnfoldTopC  `wf-term`))  0)
  THEN  Reduce  0
  THEN  (GenConcl  \mkleeneopen{}(arity  f)  =  ns\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  AutoBoolCase  \mkleeneopen{}(||ns||  =\msubz{}  ||bts||)\mkleeneclose{}\mcdot{}
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  Unfold  `l\_all`  0
  THEN  (Subst'  ||zip(ns;bts)||  \msim{}  ||bts||  0  THENA  Auto)
  THEN  (RWO  "select\_zip"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  ((D  -1  THEN  ParallelLast)  ORELSE  ((D  0  THEN  Try  (Eq))  THEN  ParallelLast))
  THEN  (MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}bts[i]\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  D  -2
  THEN  Reduce  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto)

---

Home Index