---

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

.....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> ∈ (Atom × Atom)
BY
{ (Eliminate ⌜k⌝⋅ THEN All Reduce) }

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

---

Latex:

---

Latex:
.....truecase..... 
1.  k  :  \{k:Atom|  (k  \mmember{}  ``opid  nType  nterm  univ``)\} 
2.  f1  :  \{f:Atom|  (f  \mmember{}  ctt-tokens())\} 
3.  s  :  Atom
4.  \muparrow{}(k  =a  "opid"  \mwedge{}\msubb{}  f1  =a  s)
5.  k  =  "opid"
\mvdash{}  <k,  f1>  =  <"opid",  s>


By

---

Latex:
(Eliminate  \mkleeneopen{}k\mkleeneclose{}\mcdot{}  THEN  All  Reduce)

---

Home Index