---

Step * 1 of Lemma assert-ctt-term-is


1. s : Atom
2. term(CttOp) ≡ coterm-fun(CttOp;term(CttOp))
3. f : CttOp
4. bts : (varname() List × term(CttOp)) List
5. mkterm(f;bts) ∈ term(CttOp)
6. ↑wf-term(λx.ctt-arity(x);λt.ctt-kind(t);mkterm(f;bts))
7. (||bts|| = ||ctt-arity(f)|| ∈ ℤ)
∧ (∀i:ℕ||bts||
     ((||fst(bts[i])|| = (fst(ctt-arity(f)[i])) ∈ ℤ)
     ∧ (ctt-kind(snd(bts[i])) = (snd(ctt-arity(f)[i])) ∈ ℤ)
     ∧ (↑wf-term(λx.ctt-arity(x);λt.ctt-kind(t);snd(bts[i])))))
8. ↑ctt-term-is(s;mkterm(f;bts))
⊢ {(¬↑isvarterm(mkterm(f;bts)))
∧ (term-opr(mkterm(f;bts)) = <"opid", s> ∈ CttOp)
∧ (||term-bts(mkterm(f;bts))|| = ||ctt-opid-arity(s)|| ∈ ℤ)
∧ (∀i:ℕ||term-bts(mkterm(f;bts))||
     ((||fst(term-bts(mkterm(f;bts))[i])|| = (fst(ctt-opid-arity(s)[i])) ∈ ℤ)
     ∧ (ctt-kind(snd(term-bts(mkterm(f;bts))[i])) = (snd(ctt-opid-arity(s)[i])) ∈ ℤ)))
∧ (mkterm(f;bts) ~ mkwfterm(term-opr(mkterm(f;bts));term-bts(mkterm(f;bts))))}
BY
{ ((Assert term-opr(mkterm(f;bts)) ∈ CttOp BY
          Auto)
   THEN DVar `f'
   THEN RepUR ``ctt-term-is isvarterm mkterm`` -2
   THEN DVar `k'
   THEN (Assert (k ∈ ``opid nType nterm univ``) BY
               (Unhide THEN Auto))
   THEN Repeat ((GenListD (-1) THEN D -1))
   THEN Eliminate ⌜k⌝⋅
   THEN All Reduce
   THEN Try (Trivial)
   THEN (Assert (f1 ∈ ctt-tokens()) BY
               Auto)
   THEN (RW assert_pushdownC (-4) THENA Auto)
   THEN Eliminate ⌜f1⌝⋅
   THEN All (RepUR ``term-opr term-bts mkterm mkwfterm ctt-arity isvarterm``)
   THEN ExRepD
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  Atom
2.  term(CttOp)  \mequiv{}  coterm-fun(CttOp;term(CttOp))
3.  f  :  CttOp
4.  bts  :  (varname()  List  \mtimes{}  term(CttOp))  List
5.  mkterm(f;bts)  \mmember{}  term(CttOp)
6.  \muparrow{}wf-term(\mlambda{}x.ctt-arity(x);\mlambda{}t.ctt-kind(t);mkterm(f;bts))
7.  (||bts||  =  ||ctt-arity(f)||)
\mwedge{}  (\mforall{}i:\mBbbN{}||bts||
          ((||fst(bts[i])||  =  (fst(ctt-arity(f)[i])))
          \mwedge{}  (ctt-kind(snd(bts[i]))  =  (snd(ctt-arity(f)[i])))
          \mwedge{}  (\muparrow{}wf-term(\mlambda{}x.ctt-arity(x);\mlambda{}t.ctt-kind(t);snd(bts[i])))))
8.  \muparrow{}ctt-term-is(s;mkterm(f;bts))
\mvdash{}  \{(\mneg{}\muparrow{}isvarterm(mkterm(f;bts)))
\mwedge{}  (term-opr(mkterm(f;bts))  =  <"opid",  s>)
\mwedge{}  (||term-bts(mkterm(f;bts))||  =  ||ctt-opid-arity(s)||)
\mwedge{}  (\mforall{}i:\mBbbN{}||term-bts(mkterm(f;bts))||
          ((||fst(term-bts(mkterm(f;bts))[i])||  =  (fst(ctt-opid-arity(s)[i])))
          \mwedge{}  (ctt-kind(snd(term-bts(mkterm(f;bts))[i]))  =  (snd(ctt-opid-arity(s)[i])))))
\mwedge{}  (mkterm(f;bts)  \msim{}  mkwfterm(term-opr(mkterm(f;bts));term-bts(mkterm(f;bts))))\}


By

---

Latex:
((Assert  term-opr(mkterm(f;bts))  \mmember{}  CttOp  BY
                Auto)
  THEN  DVar  `f'
  THEN  RepUR  ``ctt-term-is  isvarterm  mkterm``  -2
  THEN  DVar  `k'
  THEN  (Assert  (k  \mmember{}  ``opid  nType  nterm  univ``)  BY
                          (Unhide  THEN  Auto))
  THEN  Repeat  ((GenListD  (-1)  THEN  D  -1))
  THEN  Eliminate  \mkleeneopen{}k\mkleeneclose{}\mcdot{}
  THEN  All  Reduce
  THEN  Try  (Trivial)
  THEN  (Assert  (f1  \mmember{}  ctt-tokens())  BY
                          Auto)
  THEN  (RW  assert\_pushdownC  (-4)  THENA  Auto)
  THEN  Eliminate  \mkleeneopen{}f1\mkleeneclose{}\mcdot{}
  THEN  All  (RepUR  ``term-opr  term-bts  mkterm  mkwfterm  ctt-arity  isvarterm``)
  THEN  ExRepD
  THEN  D  0
  THEN  Auto)

---

Home Index