---

Step * 4 of Lemma ctt-op-meaning_wf

.....falsecase..... 
1. X : ?CubicalContext
2. vs : varname() List
3. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
4. f1 : ℕ
5. L : CttMeaningTriple List
6. vdf-eq(?CubicalContext;ctt-binder-context X vs <k, f1>;L)
7. ||L|| = ||ctt-arity(<k, f1>)|| ∈ ℤ
8. ∀i:ℕ||L||
     ((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<k, f1>)[i])) ∈ ℤ)
     ∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<k, f1>)[i])) ∈ ℤ)
     ∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
9. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <k, f1> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext)
10. ¬(k = "opid" ∈ Atom)
11. ¬(k = "nType" ∈ Atom)
12. ¬(k = "nterm" ∈ Atom)
⊢ ctt-op-meaning{i:l}(X; vs; <k, f1>; L) ∈ [[X;mkterm(<k, f1>;map(λx.(fst(snd(x)));L))]]
BY
{ (RenameVar `n' 4
   THEN (Subst' k = "univ" ∈ Atom 0
         THENA (DVar `k' THEN RepeatFor 4 ((GenListD 4 THEN D 4 THEN Try (Trivial))) THEN GenListD 4)
         )
   THEN RepUR ``ctt_meaning ctt-meaning-type mkwfterm isvarterm mkterm term-opr`` 0
   THEN RepUR ``ctt-op-sort ctt-op-meaning univ-meaning`` 0
   THEN (Unfold `uimplies` 0 THEN (MemTypeCD THENW Auto))
   THEN ProvisionCD
   THEN Auto) }

---

Latex:

---

Latex:
.....falsecase..... 
1.  X  :  ?CubicalContext
2.  vs  :  varname()  List
3.  k  :  \{k:Atom|  (k  \mmember{}  ``opid  nType  nterm  univ``)\} 
4.  f1  :  \mBbbN{}
5.  L  :  CttMeaningTriple  List
6.  vdf-eq(?CubicalContext;ctt-binder-context  X  vs  <k,  f1>L)
7.  ||L||  =  ||ctt-arity(<k,  f1>)||
8.  \mforall{}i:\mBbbN{}||L||
          ((||fst(map(\mlambda{}x.(fst(snd(x)));L)[i])||  =  (fst(ctt-arity(<k,  f1>)[i])))
          \mwedge{}  (ctt-kind(snd(map(\mlambda{}x.(fst(snd(x)));L)[i]))  =  (snd(ctt-arity(<k,  f1>)[i])))
          \mwedge{}  (\muparrow{}wf-term(\mlambda{}f.ctt-arity(f);\mlambda{}t.ctt-kind(t);snd(map(\mlambda{}x.(fst(snd(x)));L)[i]))))
9.  \mforall{}[i:\mBbbN{}||L||].  ((fst(L[i]))  =  (ctt-binder-context  X  vs  <k,  f1>  firstn(i;L)  (fst(snd(L[i])))))
10.  \mneg{}(k  =  "opid")
11.  \mneg{}(k  =  "nType")
12.  \mneg{}(k  =  "nterm")
\mvdash{}  ctt-op-meaning\{i:l\}(X;  vs;  <k,  f1>  L)  \mmember{}  [[X;mkterm(<k,  f1>map(\mlambda{}x.(fst(snd(x)));L))]]


By

---

Latex:
(RenameVar  `n'  4
  THEN  (Subst'  k  =  "univ"  0
              THENA  (DVar  `k'  THEN  RepeatFor  4  ((GenListD  4  THEN  D  4  THEN  Try  (Trivial)))  THEN  GenListD  4)
              )
  THEN  RepUR  ``ctt\_meaning  ctt-meaning-type  mkwfterm  isvarterm  mkterm  term-opr``  0
  THEN  RepUR  ``ctt-op-sort  ctt-op-meaning  univ-meaning``  0
  THEN  (Unfold  `uimplies`  0  THEN  (MemTypeCD  THENW  Auto))
  THEN  ProvisionCD
  THEN  Auto)

---

Home Index