---

Step * of Lemma assert-ctt-term-is

No Annotations
∀s:Atom. ∀t:CttTerm.
  ((↑ctt-term-is(s;t))
  ⇒ {(¬↑isvarterm(t))
     ∧ (term-opr(t) = <"opid", s> ∈ CttOp)
     ∧ (||term-bts(t)|| = ||ctt-opid-arity(s)|| ∈ ℤ)
     ∧ (∀i:ℕ||term-bts(t)||
          ((||fst(term-bts(t)[i])|| = (fst(ctt-opid-arity(s)[i])) ∈ ℤ)
          ∧ (ctt-kind(snd(term-bts(t)[i])) = (snd(ctt-opid-arity(s)[i])) ∈ ℤ)))
     ∧ (t ~ mkwfterm(term-opr(t);term-bts(t)))})
BY
{ (RepeatFor 2 (Intro)
   THEN D -1
   THEN (Assert ↑wf-term(λx.ctt-arity(x);λt.ctt-kind(t);t) BY
               Auto)
   THEN MoveToConcl (-1)
   THEN Thin (-1)
   THEN (InstLemma `term-ext` [⌜parm{i'}⌝;⌜CttOp⌝]⋅ THENA Auto)
   THEN (GenConcl ⌜t = a ∈ coterm-fun(CttOp;term(CttOp))⌝⋅ THENA Auto)
   THEN ThinVar `t'
   THEN (Assert a ∈ term(CttOp) BY
               Auto)
   THEN (D -2
         THENL [(RepUR ``ctt-term-is isvarterm`` 0 THEN Auto)
               ; (D -2 THEN All (Fold  `mkterm`) THEN RenameVar `f' (-3) THEN RenameVar `bts' (-2))]
   )
   THEN (D 0 THENA Auto)
   THEN DupHyp (-1)
   THEN (RWO "assert-wf-mkterm" (-1) THENA Auto)
   THEN Reduce -1
   THEN (D 0 THENA Auto)) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}s:Atom.  \mforall{}t:CttTerm.
    ((\muparrow{}ctt-term-is(s;t))
    {}\mRightarrow{}  \{(\mneg{}\muparrow{}isvarterm(t))
          \mwedge{}  (term-opr(t)  =  <"opid",  s>)
          \mwedge{}  (||term-bts(t)||  =  ||ctt-opid-arity(s)||)
          \mwedge{}  (\mforall{}i:\mBbbN{}||term-bts(t)||
                    ((||fst(term-bts(t)[i])||  =  (fst(ctt-opid-arity(s)[i])))
                    \mwedge{}  (ctt-kind(snd(term-bts(t)[i]))  =  (snd(ctt-opid-arity(s)[i])))))
          \mwedge{}  (t  \msim{}  mkwfterm(term-opr(t);term-bts(t)))\})


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  D  -1
  THEN  (Assert  \muparrow{}wf-term(\mlambda{}x.ctt-arity(x);\mlambda{}t.ctt-kind(t);t)  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  Thin  (-1)
  THEN  (InstLemma  `term-ext`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}CttOp\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}t  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `t'
  THEN  (Assert  a  \mmember{}  term(CttOp)  BY
                          Auto)
  THEN  (D  -2
              THENL  [(RepUR  ``ctt-term-is  isvarterm``  0  THEN  Auto)
                          ;  (D  -2  THEN  All  (Fold    `mkterm`)  THEN  RenameVar  `f'  (-3)  THEN  RenameVar  `bts'  (-2))]
  )
  THEN  (D  0  THENA  Auto)
  THEN  DupHyp  (-1)
  THEN  (RWO  "assert-wf-mkterm"  (-1)  THENA  Auto)
  THEN  Reduce  -1
  THEN  (D  0  THENA  Auto))

---

Home Index