---

Step * of Lemma ctt-op-meaning_wf

No Annotations
∀[X:?CubicalContext]. ∀[vs:varname() List]. ∀[f:CttOp].
∀[L:{L:CttMeaningTriple List| 
     vdf-eq(?CubicalContext;ctt-binder-context X vs f;L)
     ∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);mkterm(f;map(λx.(fst(snd(x)));L))))} ].
  (ctt-op-meaning{i:l}(X; vs; f; L) ∈ [[X;mkterm(f;map(λx.(fst(snd(x)));L))]])
BY
{ (Intros
   THEN Unhide
   THEN RepeatFor 2 (D -1)
   THEN (FLemma `vdf-eq-implies2` [-2] THENA Auto)
   THEN (RWO "assert-wf-mkterm" (-2) THENA Auto)
   THEN Reduce -2
   THEN (RWO "length-map" (-2) THENA Auto)
   THEN D -2
   THEN D 3
   THEN (SplitOnHypITE 4  THENA Auto)
   THEN (HypSubst' (-1) 0
   ORELSE ((SplitOnHypITE 4  THENA Auto) THEN (HypSubst' (-1) 0 ORELSE (SplitOnHypITE 4  THENA Auto)))
   )) }

1
1. X : ?CubicalContext
2. vs : varname() List
3. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
4. f1 : {f:Atom| (f ∈ ctt-tokens())} 
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
⊢ ctt-op-meaning{i:l}(X; vs; <"opid", f1>; L) ∈ [[X;mkterm(<"opid", f1>;map(λx.(fst(snd(x)));L))]]

2
1. X : ?CubicalContext
2. vs : varname() List
3. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
4. f1 : Type
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
⊢ ctt-op-meaning{i:l}(X; vs; <"nType", f1>; L) ∈ [[X;mkterm(<"nType", f1>;map(λx.(fst(snd(x)));L))]]

3
.....truecase..... 
1. X : ?CubicalContext
2. vs : varname() List
3. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
4. f1 : T:Type × T
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))]]

4
.....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))]]

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:?CubicalContext].  \mforall{}[vs:varname()  List].  \mforall{}[f:CttOp].
\mforall{}[L:\{L:CttMeaningTriple  List| 
          vdf-eq(?CubicalContext;ctt-binder-context  X  vs  f;L)
          \mwedge{}  (\muparrow{}wf-term(\mlambda{}f.ctt-arity(f);\mlambda{}t.ctt-kind(t);mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))))\}  ].
    (ctt-op-meaning\{i:l\}(X;  vs;  f;  L)  \mmember{}  [[X;mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))]])


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  RepeatFor  2  (D  -1)
  THEN  (FLemma  `vdf-eq-implies2`  [-2]  THENA  Auto)
  THEN  (RWO  "assert-wf-mkterm"  (-2)  THENA  Auto)
  THEN  Reduce  -2
  THEN  (RWO  "length-map"  (-2)  THENA  Auto)
  THEN  D  -2
  THEN  D  3
  THEN  (SplitOnHypITE  4    THENA  Auto)
  THEN  (HypSubst'  (-1)  0
  ORELSE  ((SplitOnHypITE  4    THENA  Auto)  THEN  (HypSubst'  (-1)  0  ORELSE  (SplitOnHypITE  4    THENA  Auto)))
  ))

---

Home Index