Step
*
1
of Lemma
ctt-op-meaning_wf
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))]]
BY
{ (D 4
THEN Repeat ((GenListD 5 THEN D 5))
THEN Eliminate ⌜f1⌝⋅
THEN Eliminate ⌜k⌝⋅
THEN ThinVar `k'
THEN ThinVar `f1'
THEN RepUR ``ctt-arity ctt-opid-arity`` -3
THEN RepUR ``ctt-op-meaning ctt_meaning ctt-meaning-type isvarterm mkterm term-opr ctt-op-sort`` 0
THEN Try (((Assert ||L|| = 0 ∈ ℤ BY Hypothesis) THEN Auto))
THEN Unfold `uimplies` 0
THEN (MemTypeCD THENW Auto)
THEN CttArityInst 6 ⌜L⌝⋅
THEN Repeat (SimpleCttKindGen )
THEN Try ((Unfolds ``eq0-meaning eq1-meaning meet-meaning join-meaning inv-meaning min-meaning max-meaning`` 0
THEN Reduce 0
THEN ProvisionCD
THEN Auto
THEN NthHypEqGen (-1)
THEN EqCDA
THEN Auto))) }
1
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "Glue">;L)
5. ||L|| = 4 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "Glue">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "Glue">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "Glue"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext\000C)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. X3 : ?CubicalContext
14. b2 : varname() List × CttTerm
15. v6 : [[X3;snd(b2)]]
16. X4 : ?CubicalContext
17. b3 : varname() List × CttTerm
18. v8 : [[X4;snd(b3)]]
19. ||fst(bt)|| = 0 ∈ ℤ
20. ctt-kind(snd(bt)) = 1 ∈ ℤ
21. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
22. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
23. X = X1 ∈ ?CubicalContext
24. context-set(X) = context-set(X1) ∈ CubicalSet'''
25. t : Provisional''''(cttType(context-set(X)))
26. ||fst(b1)|| = 0 ∈ ℤ
27. ctt-kind(snd(b1)) = 0 ∈ ℤ
28. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1))
29. X2 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
30. X = X2 ∈ ?CubicalContext
31. context-set(X) = context-set(X2) ∈ CubicalSet'''
32. t1 : Provisional''''(cttTerm(context-set(X)))
⊢ (||fst(b2)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b2)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2)))
⇒ (X3 = bind-provision(X;ctxt.restrict-cubical-context{i:l}(ctxt;t1)) ∈ ?CubicalContext)
⇒ (||fst(b3)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b3)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b3)))
⇒ (X4 = bind-provision(X;ctxt.restrict-cubical-context{i:l}(ctxt;t1)) ∈ ?CubicalContext)
⇒ (Glue-meaning{i:l}(<X1, bt, t>; <X2, b1, t1>; <X3, b2, v6>; <X4, b3, v8>) ∈ Provisional''''(cttType(context-set(X))))
2
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "case">;L)
5. ||L|| = 4 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "case">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "case">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "case"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext\000C)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. X3 : ?CubicalContext
14. b2 : varname() List × CttTerm
15. v6 : [[X3;snd(b2)]]
16. X4 : ?CubicalContext
17. b3 : varname() List × CttTerm
18. v8 : [[X4;snd(b3)]]
19. ||fst(bt)|| = 0 ∈ ℤ
20. ctt-kind(snd(bt)) = 0 ∈ ℤ
21. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
22. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
23. X = X1 ∈ ?CubicalContext
24. context-set(X) = context-set(X1) ∈ CubicalSet'''
25. t : Provisional''''(cttTerm(context-set(X)))
26. ||fst(b1)|| = 0 ∈ ℤ
27. ctt-kind(snd(b1)) = 0 ∈ ℤ
28. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1))
29. X2 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
30. X = X2 ∈ ?CubicalContext
31. context-set(X) = context-set(X2) ∈ CubicalSet'''
32. t1 : Provisional''''(cttTerm(context-set(X)))
⊢ (||fst(b2)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b2)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2)))
⇒ (X3 = bind-provision(X;ctxt.restrict-cubical-context{i:l}(ctxt;t)) ∈ ?CubicalContext)
⇒ (||fst(b3)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b3)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b3)))
⇒ (X4 = bind-provision(X;ctxt.restrict-cubical-context{i:l}(ctxt;t1)) ∈ ?CubicalContext)
⇒ (case-meaning{i:l}(<X1, bt, t>; <X2, b1, t1>; <X3, b2, v6>; <X4, b3, v8>) ∈ Provisional''''(cttType(context-set(X))))
3
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "sigma">;L)
5. ||L|| = 2 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "sigma">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "sigma">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "sigma"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContex\000Ct)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. v4 : [[X2;snd(b1)]]
14. ||fst(bt)|| = 0 ∈ ℤ
15. ctt-kind(snd(bt)) = 1 ∈ ℤ
16. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
17. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
18. X = X1 ∈ ?CubicalContext
19. context-set(X) = context-set(X1) ∈ CubicalSet'''
20. t : Provisional''''(cttType(context-set(X)))
⊢ (||fst(b1)|| = 1 ∈ ℤ)
⇒ (ctt-kind(snd(b1)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1)))
⇒ (X2 = bind-provision(X;ctxt.ctxt; hd(fst(b1)):fst(t)) ∈ ?CubicalContext)
⇒ (sigma-meaning{i:l}(<X1, bt, t>; <X2, b1, v4>) ∈ Provisional''''(cttType(context-set(X))))
4
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "path">;L)
5. ||L|| = 3 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "path">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "path">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "path"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext\000C)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. X3 : ?CubicalContext
14. b2 : varname() List × CttTerm
15. ||fst(bt)|| = 0 ∈ ℤ
16. ctt-kind(snd(bt)) = 1 ∈ ℤ
17. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
18. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
19. X = X1 ∈ ?CubicalContext
20. context-set(X) = context-set(X1) ∈ CubicalSet'''
21. t : Provisional''''(cttType(context-set(X)))
22. ||fst(b1)|| = 0 ∈ ℤ
23. ctt-kind(snd(b1)) = 0 ∈ ℤ
24. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1))
25. X2 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
26. X = X2 ∈ ?CubicalContext
27. context-set(X) = context-set(X2) ∈ CubicalSet'''
28. t1 : Provisional''''(cttTerm(context-set(X)))
29. ||fst(b2)|| = 0 ∈ ℤ
30. ctt-kind(snd(b2)) = 0 ∈ ℤ
31. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2))
32. X3 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
33. X = X3 ∈ ?CubicalContext
34. context-set(X) = context-set(X3) ∈ CubicalSet'''
35. t2 : Provisional''''(cttTerm(context-set(X)))
⊢ path-meaning{i:l}(<X1, bt, t>; <X2, b1, t1>; <X3, b2, t2>) ∈ Provisional''''(cttType(context-set(X)))
5
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "pi">;L)
5. ||L|| = 2 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "pi">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "pi">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "pi"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. v4 : [[X2;snd(b1)]]
14. ||fst(bt)|| = 0 ∈ ℤ
15. ctt-kind(snd(bt)) = 1 ∈ ℤ
16. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
17. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
18. X = X1 ∈ ?CubicalContext
19. context-set(X) = context-set(X1) ∈ CubicalSet'''
20. t : Provisional''''(cttType(context-set(X)))
⊢ (||fst(b1)|| = 1 ∈ ℤ)
⇒ (ctt-kind(snd(b1)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1)))
⇒ (X2 = bind-provision(X;ctxt.ctxt; hd(fst(b1)):fst(t)) ∈ ?CubicalContext)
⇒ (pi-meaning{i:l}(<X1, bt, t>; <X2, b1, v4>) ∈ Provisional''''(cttType(context-set(X))))
6
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "decode1">;L)
5. ||L|| = 1 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "decode1">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "decode1">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "decode1"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalCont\000Cext)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. ||fst(bt)|| = 0 ∈ ℤ
12. ctt-kind(snd(bt)) = 0 ∈ ℤ
13. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
14. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
15. X = X1 ∈ ?CubicalContext
16. context-set(X) = context-set(X1) ∈ CubicalSet'''
17. t : Provisional''''(cttTerm(context-set(X)))
⊢ decode-meaning{i:l}(0; <X1, bt, t>) ∈ Provisional''''(cttType(context-set(X)))
7
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "decode2">;L)
5. ||L|| = 1 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "decode2">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "decode2">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "decode2"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalCont\000Cext)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. ||fst(bt)|| = 0 ∈ ℤ
12. ctt-kind(snd(bt)) = 0 ∈ ℤ
13. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
14. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
15. X = X1 ∈ ?CubicalContext
16. context-set(X) = context-set(X1) ∈ CubicalSet'''
17. t : Provisional''''(cttTerm(context-set(X)))
⊢ decode-meaning{i:l}(1; <X1, bt, t>) ∈ Provisional''''(cttType(context-set(X)))
8
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "decode3">;L)
5. ||L|| = 1 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "decode3">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "decode3">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "decode3"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalCont\000Cext)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. ||fst(bt)|| = 0 ∈ ℤ
12. ctt-kind(snd(bt)) = 0 ∈ ℤ
13. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
14. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
15. X = X1 ∈ ?CubicalContext
16. context-set(X) = context-set(X1) ∈ CubicalSet'''
17. t : Provisional''''(cttTerm(context-set(X)))
⊢ decode-meaning{i:l}(2; <X1, bt, t>) ∈ Provisional''''(cttType(context-set(X)))
9
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "encode1">;L)
5. ||L|| = 1 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "encode1">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "encode1">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "encode1"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalCont\000Cext)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. ||fst(bt)|| = 0 ∈ ℤ
12. ctt-kind(snd(bt)) = 1 ∈ ℤ
13. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
14. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
15. X = X1 ∈ ?CubicalContext
16. context-set(X) = context-set(X1) ∈ CubicalSet'''
17. t : Provisional''''(cttType(context-set(X)))
⊢ encode-meaning{i:l}(1; <X1, bt, t>) ∈ Provisional''''(cttTerm(context-set(X)))
10
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "encode2">;L)
5. ||L|| = 1 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "encode2">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "encode2">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "encode2"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalCont\000Cext)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. ||fst(bt)|| = 0 ∈ ℤ
12. ctt-kind(snd(bt)) = 1 ∈ ℤ
13. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
14. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
15. X = X1 ∈ ?CubicalContext
16. context-set(X) = context-set(X1) ∈ CubicalSet'''
17. t : Provisional''''(cttType(context-set(X)))
⊢ encode-meaning{i:l}(2; <X1, bt, t>) ∈ Provisional''''(cttTerm(context-set(X)))
11
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "encode3">;L)
5. ||L|| = 1 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "encode3">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "encode3">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "encode3"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalCont\000Cext)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. ||fst(bt)|| = 0 ∈ ℤ
12. ctt-kind(snd(bt)) = 1 ∈ ℤ
13. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
14. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
15. X = X1 ∈ ?CubicalContext
16. context-set(X) = context-set(X1) ∈ CubicalSet'''
17. t : Provisional''''(cttType(context-set(X)))
⊢ encode-meaning{i:l}(3; <X1, bt, t>) ∈ Provisional''''(cttTerm(context-set(X)))
12
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "pathabs">;L)
5. ||L|| = 2 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "pathabs">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "pathabs">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "pathabs"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalCont\000Cext)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. v4 : [[X2;snd(b1)]]
14. ||fst(bt)|| = 0 ∈ ℤ
15. ctt-kind(snd(bt)) = 1 ∈ ℤ
16. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
17. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
18. X = X1 ∈ ?CubicalContext
19. context-set(X) = context-set(X1) ∈ CubicalSet'''
20. t : Provisional''''(cttType(context-set(X)))
⊢ (||fst(b1)|| = 1 ∈ ℤ)
⇒ (ctt-kind(snd(b1)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1)))
⇒ (X2 = bind-provision(X;ctxt.ctxt; hd(fst(b1)):OK(<0, 𝕀>)) ∈ ?CubicalContext)
⇒ (pathabs-meaning{i:l}(<X1, bt, t>; <X2, b1, v4>) ∈ Provisional''''(cttTerm(context-set(X))))
13
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "pathap">;L)
5. ||L|| = 3 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "pathap">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "pathap">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "pathap"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalConte\000Cxt)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. X3 : ?CubicalContext
14. b2 : varname() List × CttTerm
15. ||fst(bt)|| = 0 ∈ ℤ
16. ctt-kind(snd(bt)) = 1 ∈ ℤ
17. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
18. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
19. X = X1 ∈ ?CubicalContext
20. context-set(X) = context-set(X1) ∈ CubicalSet'''
21. t : Provisional''''(cttType(context-set(X)))
22. ||fst(b1)|| = 0 ∈ ℤ
23. ctt-kind(snd(b1)) = 0 ∈ ℤ
24. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1))
25. X2 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
26. X = X2 ∈ ?CubicalContext
27. context-set(X) = context-set(X2) ∈ CubicalSet'''
28. t1 : Provisional''''(cttTerm(context-set(X)))
29. ||fst(b2)|| = 0 ∈ ℤ
30. ctt-kind(snd(b2)) = 0 ∈ ℤ
31. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2))
32. X3 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
33. X = X3 ∈ ?CubicalContext
34. context-set(X) = context-set(X3) ∈ CubicalSet'''
35. t2 : Provisional''''(cttTerm(context-set(X)))
⊢ pathapp-meaning{i:l}(<X1, bt, t>; <X2, b1, t1>; <X3, b2, t2>) ∈ Provisional''''(cttTerm(context-set(X)))
14
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "lambda">;L)
5. ||L|| = 2 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "lambda">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "lambda">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "lambda"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalConte\000Cxt)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. v4 : [[X2;snd(b1)]]
14. ||fst(bt)|| = 0 ∈ ℤ
15. ctt-kind(snd(bt)) = 1 ∈ ℤ
16. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
17. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
18. X = X1 ∈ ?CubicalContext
19. context-set(X) = context-set(X1) ∈ CubicalSet'''
20. t : Provisional''''(cttType(context-set(X)))
⊢ (||fst(b1)|| = 1 ∈ ℤ)
⇒ (ctt-kind(snd(b1)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1)))
⇒ (X2 = bind-provision(X;ctxt.ctxt; hd(fst(b1)):fst(t)) ∈ ?CubicalContext)
⇒ (lambda-meaning{i:l}(<X1, bt, t>; <X2, b1, v4>) ∈ Provisional''''(cttTerm(context-set(X))))
15
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "apply">;L)
5. ||L|| = 3 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "apply">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "apply">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "apply"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContex\000Ct)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. v4 : [[X2;snd(b1)]]
14. X3 : ?CubicalContext
15. b2 : varname() List × CttTerm
16. v6 : [[X3;snd(b2)]]
17. ||fst(bt)|| = 0 ∈ ℤ
18. ctt-kind(snd(bt)) = 0 ∈ ℤ
19. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
20. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
21. X = X1 ∈ ?CubicalContext
22. context-set(X) = context-set(X1) ∈ CubicalSet'''
23. t : Provisional''''(cttTerm(context-set(X)))
⊢ (||fst(b1)|| = 1 ∈ ℤ)
⇒ (ctt-kind(snd(b1)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1)))
⇒ (X2 = bind-provision(X;ctxt.ctxt; hd(fst(b1)):fst(t)) ∈ ?CubicalContext)
⇒ (||fst(b2)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b2)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2)))
⇒ (X3 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext)
⇒ (apply-meaning{i:l}(<X1, bt, t>; <X2, b1, v4>; <X3, b2, v6>) ∈ Provisional''''(cttTerm(context-set(X))))
16
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "pair">;L)
5. ||L|| = 3 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "pair">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "pair">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "pair"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext\000C)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. v4 : [[X2;snd(b1)]]
14. X3 : ?CubicalContext
15. b2 : varname() List × CttTerm
16. v6 : [[X3;snd(b2)]]
17. ||fst(bt)|| = 0 ∈ ℤ
18. ctt-kind(snd(bt)) = 0 ∈ ℤ
19. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
20. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
21. X = X1 ∈ ?CubicalContext
22. context-set(X) = context-set(X1) ∈ CubicalSet'''
23. t : Provisional''''(cttTerm(context-set(X)))
⊢ (||fst(b1)|| = 1 ∈ ℤ)
⇒ (ctt-kind(snd(b1)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1)))
⇒ (X2 = bind-provision(X;ctxt.ctxt; hd(fst(b1)):fst(t)) ∈ ?CubicalContext)
⇒ (||fst(b2)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b2)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2)))
⇒ (X3 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext)
⇒ (pair-meaning{i:l}(<X1, bt, t>; <X2, b1, v4>; <X3, b2, v6>) ∈ Provisional''''(cttTerm(context-set(X))))
17
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "fst">;L)
5. ||L|| = 3 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "fst">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "fst">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "fst"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. v4 : [[X2;snd(b1)]]
14. X3 : ?CubicalContext
15. b2 : varname() List × CttTerm
16. v6 : [[X3;snd(b2)]]
17. ||fst(bt)|| = 0 ∈ ℤ
18. ctt-kind(snd(bt)) = 1 ∈ ℤ
19. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
20. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
21. X = X1 ∈ ?CubicalContext
22. context-set(X) = context-set(X1) ∈ CubicalSet'''
23. t : Provisional''''(cttType(context-set(X)))
⊢ (||fst(b1)|| = 1 ∈ ℤ)
⇒ (ctt-kind(snd(b1)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1)))
⇒ (X2 = bind-provision(X;ctxt.ctxt; hd(fst(b1)):fst(t)) ∈ ?CubicalContext)
⇒ (||fst(b2)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b2)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2)))
⇒ (X3 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext)
⇒ (fst-meaning{i:l}(<X1, bt, t>; <X2, b1, v4>; <X3, b2, v6>) ∈ Provisional''''(cttTerm(context-set(X))))
18
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "snd">;L)
5. ||L|| = 3 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "snd">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "snd">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "snd"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. v4 : [[X2;snd(b1)]]
14. X3 : ?CubicalContext
15. b2 : varname() List × CttTerm
16. v6 : [[X3;snd(b2)]]
17. ||fst(bt)|| = 0 ∈ ℤ
18. ctt-kind(snd(bt)) = 1 ∈ ℤ
19. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
20. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
21. X = X1 ∈ ?CubicalContext
22. context-set(X) = context-set(X1) ∈ CubicalSet'''
23. t : Provisional''''(cttType(context-set(X)))
⊢ (||fst(b1)|| = 1 ∈ ℤ)
⇒ (ctt-kind(snd(b1)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1)))
⇒ (X2 = bind-provision(X;ctxt.ctxt; hd(fst(b1)):fst(t)) ∈ ?CubicalContext)
⇒ (||fst(b2)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b2)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2)))
⇒ (X3 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext)
⇒ (snd-meaning{i:l}(<X1, bt, t>; <X2, b1, v4>; <X3, b2, v6>) ∈ Provisional''''(cttTerm(context-set(X))))
19
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "glue">;L)
5. ||L|| = 4 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "glue">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "glue">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "glue"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext\000C)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. X3 : ?CubicalContext
14. b2 : varname() List × CttTerm
15. v6 : [[X3;snd(b2)]]
16. X4 : ?CubicalContext
17. b3 : varname() List × CttTerm
18. v8 : [[X4;snd(b3)]]
19. ||fst(bt)|| = 0 ∈ ℤ
20. ctt-kind(snd(bt)) = 0 ∈ ℤ
21. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
22. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
23. X = X1 ∈ ?CubicalContext
24. context-set(X) = context-set(X1) ∈ CubicalSet'''
25. t : Provisional''''(cttTerm(context-set(X)))
26. ||fst(b1)|| = 0 ∈ ℤ
27. ctt-kind(snd(b1)) = 0 ∈ ℤ
28. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1))
29. X2 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
30. X = X2 ∈ ?CubicalContext
31. context-set(X) = context-set(X2) ∈ CubicalSet'''
32. t1 : Provisional''''(cttTerm(context-set(X)))
⊢ (||fst(b2)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b2)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2)))
⇒ (X3 = bind-provision(X;ctxt.restrict-cubical-context{i:l}(ctxt;t)) ∈ ?CubicalContext)
⇒ (||fst(b3)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b3)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b3)))
⇒ (X4 = bind-provision(X;ctxt.restrict-cubical-context{i:l}(ctxt;t)) ∈ ?CubicalContext)
⇒ (glue-meaning{i:l}(<X1, bt, t>; <X2, b1, t1>; <X3, b2, v6>; <X4, b3, v8>) ∈ Provisional''''(cttTerm(context-set(X))))
20
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "unglue">;L)
5. ||L|| = 5 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "unglue">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "unglue">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "unglue"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalConte\000Cxt)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. X3 : ?CubicalContext
14. b2 : varname() List × CttTerm
15. v6 : [[X3;snd(b2)]]
16. X4 : ?CubicalContext
17. b3 : varname() List × CttTerm
18. v8 : [[X4;snd(b3)]]
19. X5 : ?CubicalContext
20. b4 : varname() List × CttTerm
21. v10 : [[X5;snd(b4)]]
22. ||fst(bt)|| = 0 ∈ ℤ
23. ctt-kind(snd(bt)) = 1 ∈ ℤ
24. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
25. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
26. X = X1 ∈ ?CubicalContext
27. context-set(X) = context-set(X1) ∈ CubicalSet'''
28. t : Provisional''''(cttType(context-set(X)))
29. ||fst(b1)|| = 0 ∈ ℤ
30. ctt-kind(snd(b1)) = 0 ∈ ℤ
31. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1))
32. X2 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
33. X = X2 ∈ ?CubicalContext
34. context-set(X) = context-set(X2) ∈ CubicalSet'''
35. t1 : Provisional''''(cttTerm(context-set(X)))
⊢ (||fst(b2)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b2)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2)))
⇒ (X3 = bind-provision(X;ctxt.restrict-cubical-context{i:l}(ctxt;t1)) ∈ ?CubicalContext)
⇒ (||fst(b3)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b3)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b3)))
⇒ (X4 = bind-provision(X;ctxt.restrict-cubical-context{i:l}(ctxt;t1)) ∈ ?CubicalContext)
⇒ (||fst(b4)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b4)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b4)))
⇒ (X5 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext)
⇒ (unglue-meaning{i:l}(<X1, bt, t>; <X2, b1, t1>; <X3, b2, v6>; <X4, b3, v8>; <X5, b4, v10>) ∈ Provisional''''(cttTerm(\000Ccontext-set(X))))
21
1. X : ?CubicalContext
2. vs : varname() List
3. L : CttMeaningTriple List
4. vdf-eq(?CubicalContext;ctt-binder-context X vs <"opid", "comp">;L)
5. ||L|| = 4 ∈ ℤ
6. ∀i:ℕ||L||
((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<"opid", "comp">)[i])) ∈ ℤ)
∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<"opid", "comp">)[i])) ∈ ℤ)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
7. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <"opid", "comp"> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext\000C)
8. context-ok(X)
9. X1 : ?CubicalContext
10. bt : varname() List × CttTerm
11. X2 : ?CubicalContext
12. b1 : varname() List × CttTerm
13. v4 : [[X2;snd(b1)]]
14. X3 : ?CubicalContext
15. b2 : varname() List × CttTerm
16. v6 : [[X3;snd(b2)]]
17. X4 : ?CubicalContext
18. b3 : varname() List × CttTerm
19. v8 : [[X4;snd(b3)]]
20. ||fst(bt)|| = 0 ∈ ℤ
21. ctt-kind(snd(bt)) = 0 ∈ ℤ
22. ↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(bt))
23. X1 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext
24. X = X1 ∈ ?CubicalContext
25. context-set(X) = context-set(X1) ∈ CubicalSet'''
26. t : Provisional''''(cttTerm(context-set(X)))
⊢ (||fst(b1)|| = 1 ∈ ℤ)
⇒ (ctt-kind(snd(b1)) = 1 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b1)))
⇒ (X2 = bind-provision(X;ctxt.ctxt; hd(fst(b1)):OK(<0, 𝕀>)) ∈ ?CubicalContext)
⇒ (||fst(b2)|| = 1 ∈ ℤ)
⇒ (ctt-kind(snd(b2)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b2)))
⇒ (X3 = bind-provision(X;ctxt.restrict-cubical-context{i:l}(ctxt;t),hd(fst(b2)):I) ∈ ?CubicalContext)
⇒ (||fst(b3)|| = 0 ∈ ℤ)
⇒ (ctt-kind(snd(b3)) = 0 ∈ ℤ)
⇒ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(b3)))
⇒ (X4 = bind-provision(X;ctxt.OK(ctxt)) ∈ ?CubicalContext)
⇒ (comp-meaning{i:l}(<X1, bt, t>; <X2, b1, v4>; <X3, b2, v6>; <X4, b3, v8>) ∈ Provisional''''(cttTerm(context-set(X))))
Latex:
Latex:
1. X : ?CubicalContext
2. vs : varname() List
3. k : \{k:Atom| (k \mmember{} ``opid nType nterm univ``)\}
4. f1 : \{f:Atom| (f \mmember{} 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. \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. k = "opid"
\mvdash{} ctt-op-meaning\{i:l\}(X; vs; <"opid", f1> L) \mmember{} [[X;mkterm(<"opid", f1>map(\mlambda{}x.(fst(snd(x)));L))]]
By
Latex:
(D 4
THEN Repeat ((GenListD 5 THEN D 5))
THEN Eliminate \mkleeneopen{}f1\mkleeneclose{}\mcdot{}
THEN Eliminate \mkleeneopen{}k\mkleeneclose{}\mcdot{}
THEN ThinVar `k'
THEN ThinVar `f1'
THEN RepUR ``ctt-arity ctt-opid-arity`` -3
THEN RepUR ``ctt-op-meaning ctt\_meaning ctt-meaning-type isvarterm mkterm term-opr ctt-op-sort`` 0
THEN Try (((Assert ||L|| = 0 BY Hypothesis) THEN Auto))
THEN Unfold `uimplies` 0
THEN (MemTypeCD THENW Auto)
THEN CttArityInst 6 \mkleeneopen{}L\mkleeneclose{}\mcdot{}
THEN Repeat (SimpleCttKindGen )
THEN Try ((...
THEN Reduce 0
THEN ProvisionCD
THEN Auto
THEN NthHypEqGen (-1)
THEN EqCDA
THEN Auto)))
Home
Index