---

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


1. s : Atom
2. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
3. f1 : {f:Atom| (f ∈ ctt-tokens())} 
4. f1 = s ∈ Atom
5. k = "opid" ∈ Atom
⊢ <"opid", s> = <"opid", s> ∈ CttOp
BY
{ (Fold `member` 0 THEN Unfold `ctt-op` 0 THEN MemCD) }

1
.....subterm..... T:t
1:n
1. s : Atom
2. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
3. f1 : {f:Atom| (f ∈ ctt-tokens())} 
4. f1 = s ∈ Atom
5. k = "opid" ∈ Atom
⊢ "opid" ∈ {k:Atom| (k ∈ ``opid nType nterm univ``)} 

2
.....subterm..... T:t
2:n
1. s : Atom
2. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
3. f1 : {f:Atom| (f ∈ ctt-tokens())} 
4. f1 = s ∈ Atom
5. k = "opid" ∈ Atom
⊢ s ∈ if "opid" =a "opid" then {f:Atom| (f ∈ ctt-tokens())} 
  if "opid" =a "nType" then Type
  if "opid" =a "nterm" then T:Type × T
  else ℕ
  fi 

3
.....eq aux..... 
1. s : Atom
2. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
3. f1 : {f:Atom| (f ∈ ctt-tokens())} 
4. f1 = s ∈ Atom
5. k = "opid" ∈ Atom
6. k1 : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
⊢ istype(if k1 =a "opid" then {f:Atom| (f ∈ ctt-tokens())} 
if k1 =a "nType" then Type
if k1 =a "nterm" then T:Type × T
else ℕ
fi )

---

Latex:

---

Latex:

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


By

---

Latex:
(Fold  `member`  0  THEN  Unfold  `ctt-op`  0  THEN  MemCD)

---

Home Index