---

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


1. f : CttOp
2. s : Atom
3. ↑ctt-opr-is(f;s)
⊢ f = <"opid", s> ∈ CttOp
BY
{ (D 1 THEN RepUR ``ctt-opr-is`` -1 THEN (SplitOnHypITE 2  THENA Auto)) }

1
.....truecase..... 
1. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
2. f1 : {f:Atom| (f ∈ ctt-tokens())} 
3. s : Atom
4. ↑(k =a "opid" ∧b f1 =a s)
5. k = "opid" ∈ Atom
⊢ <k, f1> = <"opid", s> ∈ CttOp

2
.....falsecase..... 
1. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
2. f1 : if k =a "nType" then Type
if k =a "nterm" then T:Type × T
else ℕ
fi 
3. s : Atom
4. ↑(k =a "opid" ∧b f1 =a s)
5. ¬(k = "opid" ∈ Atom)
⊢ <k, f1> = <"opid", s> ∈ CttOp

---

Latex:

---

Latex:

1.  f  :  CttOp
2.  s  :  Atom
3.  \muparrow{}ctt-opr-is(f;s)
\mvdash{}  f  =  <"opid",  s>


By

---

Latex:
(D  1  THEN  RepUR  ``ctt-opr-is``  -1  THEN  (SplitOnHypITE  2    THENA  Auto))

---

Home Index