Step
*
1
of Lemma
provisional-subterm-context_wf
.....subterm..... T:t
2:n
1. X : Provisional''''(CubicalContext)
2. f : CttOp
3. vs : varname() List
4. L : (a:Provisional''''(CubicalContext) × bt:varname() List × CttTerm × [[a;snd(bt)]]) List
5. ||L|| < ||ctt-arity(f)||
6. ||vs|| = (fst(ctt-arity(f)[||L||])) ∈ ℤ
7. ∀i:ℕ||L||. (ctt-kind(snd(fst(snd(L[i])))) = (snd(ctt-arity(f)[i])) ∈ ℤ)
8. (||L|| = 1 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"pi"))
∨ (↑ctt-opr-is(f;"sigma"))
∨ (↑ctt-opr-is(f;"lambda"))
∨ (↑ctt-opr-is(f;"apply"))
∨ (↑ctt-opr-is(f;"pair"))
∨ (↑ctt-opr-is(f;"fst"))
∨ (↑ctt-opr-is(f;"snd")))
⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
9. (||L|| = 2 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue"))
∨ (↑ctt-opr-is(f;"case"))
∨ (↑ctt-opr-is(f;"comp"))
∨ (↑ctt-opr-is(f;"unglue"))
∨ (↑ctt-opr-is(f;"glue")))
⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
10. (||L|| = 2 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue")) ∨ (↑ctt-opr-is(f;"unglue")))
⇒ ((fst(L[1])) = X ∈ Provisional''''(CubicalContext))
11. (||L|| = 3 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue")) ∨ (↑ctt-opr-is(f;"case")) ∨ (↑ctt-opr-is(f;"unglue")))
⇒ ((fst(L[1])) = X ∈ Provisional''''(CubicalContext))
12. (||L|| = 3 ∈ ℤ) ⇒ (↑ctt-opr-is(f;"glue")) ⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
13. (||L|| = 4 ∈ ℤ) ⇒ (↑ctt-opr-is(f;"glue")) ⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
14. CubicalContext ∈ 𝕌{i'''''}
15. ctxt : {t:CubicalContext| allowed(X) ∧ (t = allow(X) ∈ CubicalContext)}
⊢ ctt-subterm-context{i:l}(ctxt;f;||L||;vs;if (ctt-opr-is(f;"Glue") ∧b ((||L|| =z 2) ∨b(||L|| =z 3)))
∨b(ctt-opr-is(f;"case") ∧b (||L|| =z 3))
∨b(ctt-opr-is(f;"unglue") ∧b ((||L|| =z 2) ∨b(||L|| =z 3)))
then snd(snd(L[1]))
else snd(snd(L[0]))
fi ) ∈ provisional-type{i 4:l}(CubicalContext)
BY
{ (DSetVars THEN ExRepD THEN MemCD THEN Try (Trivial)) }
1
.....wf.....
1. X : Provisional''''(CubicalContext)
2. f : CttOp
3. vs : varname() List
4. L : (a:Provisional''''(CubicalContext) × bt:varname() List × CttTerm × [[a;snd(bt)]]) List
5. ||L|| < ||ctt-arity(f)||
6. ||vs|| = (fst(ctt-arity(f)[||L||])) ∈ ℤ
7. ∀i:ℕ||L||. (ctt-kind(snd(fst(snd(L[i])))) = (snd(ctt-arity(f)[i])) ∈ ℤ)
8. (||L|| = 1 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"pi"))
∨ (↑ctt-opr-is(f;"sigma"))
∨ (↑ctt-opr-is(f;"lambda"))
∨ (↑ctt-opr-is(f;"apply"))
∨ (↑ctt-opr-is(f;"pair"))
∨ (↑ctt-opr-is(f;"fst"))
∨ (↑ctt-opr-is(f;"snd")))
⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
9. (||L|| = 2 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue"))
∨ (↑ctt-opr-is(f;"case"))
∨ (↑ctt-opr-is(f;"comp"))
∨ (↑ctt-opr-is(f;"unglue"))
∨ (↑ctt-opr-is(f;"glue")))
⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
10. (||L|| = 2 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue")) ∨ (↑ctt-opr-is(f;"unglue")))
⇒ ((fst(L[1])) = X ∈ Provisional''''(CubicalContext))
11. (||L|| = 3 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue")) ∨ (↑ctt-opr-is(f;"case")) ∨ (↑ctt-opr-is(f;"unglue")))
⇒ ((fst(L[1])) = X ∈ Provisional''''(CubicalContext))
12. (||L|| = 3 ∈ ℤ) ⇒ (↑ctt-opr-is(f;"glue")) ⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
13. (||L|| = 4 ∈ ℤ) ⇒ (↑ctt-opr-is(f;"glue")) ⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
14. CubicalContext ∈ 𝕌{i'''''}
15. ctxt : CubicalContext
16. allowed(X)
17. ctxt = allow(X) ∈ CubicalContext
⊢ ||L|| ∈ ℕ
2
.....wf.....
1. X : Provisional''''(CubicalContext)
2. f : CttOp
3. vs : varname() List
4. L : (a:Provisional''''(CubicalContext) × bt:varname() List × CttTerm × [[a;snd(bt)]]) List
5. ||L|| < ||ctt-arity(f)||
6. ||vs|| = (fst(ctt-arity(f)[||L||])) ∈ ℤ
7. ∀i:ℕ||L||. (ctt-kind(snd(fst(snd(L[i])))) = (snd(ctt-arity(f)[i])) ∈ ℤ)
8. (||L|| = 1 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"pi"))
∨ (↑ctt-opr-is(f;"sigma"))
∨ (↑ctt-opr-is(f;"lambda"))
∨ (↑ctt-opr-is(f;"apply"))
∨ (↑ctt-opr-is(f;"pair"))
∨ (↑ctt-opr-is(f;"fst"))
∨ (↑ctt-opr-is(f;"snd")))
⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
9. (||L|| = 2 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue"))
∨ (↑ctt-opr-is(f;"case"))
∨ (↑ctt-opr-is(f;"comp"))
∨ (↑ctt-opr-is(f;"unglue"))
∨ (↑ctt-opr-is(f;"glue")))
⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
10. (||L|| = 2 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue")) ∨ (↑ctt-opr-is(f;"unglue")))
⇒ ((fst(L[1])) = X ∈ Provisional''''(CubicalContext))
11. (||L|| = 3 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue")) ∨ (↑ctt-opr-is(f;"case")) ∨ (↑ctt-opr-is(f;"unglue")))
⇒ ((fst(L[1])) = X ∈ Provisional''''(CubicalContext))
12. (||L|| = 3 ∈ ℤ) ⇒ (↑ctt-opr-is(f;"glue")) ⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
13. (||L|| = 4 ∈ ℤ) ⇒ (↑ctt-opr-is(f;"glue")) ⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
14. CubicalContext ∈ 𝕌{i'''''}
15. ctxt : CubicalContext
16. allowed(X)
17. ctxt = allow(X) ∈ CubicalContext
⊢ if (ctt-opr-is(f;"Glue") ∧b ((||L|| =z 2) ∨b(||L|| =z 3)))
∨b(ctt-opr-is(f;"case") ∧b (||L|| =z 3))
∨b(ctt-opr-is(f;"unglue") ∧b ((||L|| =z 2) ∨b(||L|| =z 3)))
then snd(snd(L[1]))
else snd(snd(L[0]))
fi ∈ Provisional''''(cttTerm(fst(ctxt)))
supposing ↑(((ctt-opr-is(f;"Glue") ∨bctt-opr-is(f;"case") ∨bctt-opr-is(f;"unglue"))
∧b ((||L|| =z 2) ∨b(||L|| =z 3)))
∨b(ctt-opr-is(f;"comp") ∧b (||L|| =z 2))
∨b(ctt-opr-is(f;"glue")
∧b ((||L|| =z 2) ∨b(||L|| =z 3) ∨b(||L|| =z 4)))) ⋂ Provisional''''(ctt-type-meaning1{i:l}(fst(ctxt)))
supposing ↑((ctt-opr-is(f;"pi")
∨bctt-opr-is(f;"sigma")
∨bctt-opr-is(f;"lambda")
∨bctt-opr-is(f;"apply")
∨bctt-opr-is(f;"pair")
∨bctt-opr-is(f;"fst")
∨bctt-opr-is(f;"snd"))
∧b (||L|| =z 1))
3
1. X : Provisional''''(CubicalContext)
2. f : CttOp
3. vs : varname() List
4. L : (a:Provisional''''(CubicalContext) × bt:varname() List × CttTerm × [[a;snd(bt)]]) List
5. ||L|| < ||ctt-arity(f)||
6. ||vs|| = (fst(ctt-arity(f)[||L||])) ∈ ℤ
7. ∀i:ℕ||L||. (ctt-kind(snd(fst(snd(L[i])))) = (snd(ctt-arity(f)[i])) ∈ ℤ)
8. (||L|| = 1 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"pi"))
∨ (↑ctt-opr-is(f;"sigma"))
∨ (↑ctt-opr-is(f;"lambda"))
∨ (↑ctt-opr-is(f;"apply"))
∨ (↑ctt-opr-is(f;"pair"))
∨ (↑ctt-opr-is(f;"fst"))
∨ (↑ctt-opr-is(f;"snd")))
⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
9. (||L|| = 2 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue"))
∨ (↑ctt-opr-is(f;"case"))
∨ (↑ctt-opr-is(f;"comp"))
∨ (↑ctt-opr-is(f;"unglue"))
∨ (↑ctt-opr-is(f;"glue")))
⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
10. (||L|| = 2 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue")) ∨ (↑ctt-opr-is(f;"unglue")))
⇒ ((fst(L[1])) = X ∈ Provisional''''(CubicalContext))
11. (||L|| = 3 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue")) ∨ (↑ctt-opr-is(f;"case")) ∨ (↑ctt-opr-is(f;"unglue")))
⇒ ((fst(L[1])) = X ∈ Provisional''''(CubicalContext))
12. (||L|| = 3 ∈ ℤ) ⇒ (↑ctt-opr-is(f;"glue")) ⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
13. (||L|| = 4 ∈ ℤ) ⇒ (↑ctt-opr-is(f;"glue")) ⇒ ((fst(L[0])) = X ∈ Provisional''''(CubicalContext))
14. CubicalContext ∈ 𝕌{i'''''}
15. ctxt : CubicalContext
16. allowed(X)
17. ctxt = allow(X) ∈ CubicalContext
⊢ (↑(((ctt-opr-is(f;"pi")
∨bctt-opr-is(f;"sigma")
∨bctt-opr-is(f;"lambda")
∨bctt-opr-is(f;"apply")
∨bctt-opr-is(f;"pair")
∨bctt-opr-is(f;"fst")
∨bctt-opr-is(f;"snd")
∨bctt-opr-is(f;"pathabs")
∨bctt-opr-is(f;"comp"))
∧b (||L|| =z 1))
∨b(ctt-opr-is(f;"comp") ∧b (||L|| =z 2))))
⇒ 0 < ||vs||
Latex:
Latex:
.....subterm..... T:t
2:n
1. X : Provisional''''(CubicalContext)
2. f : CttOp
3. vs : varname() List
4. L : (a:Provisional''''(CubicalContext) \mtimes{} bt:varname() List \mtimes{} CttTerm \mtimes{} [[a;snd(bt)]]) List
5. ||L|| < ||ctt-arity(f)||
6. ||vs|| = (fst(ctt-arity(f)[||L||]))
7. \mforall{}i:\mBbbN{}||L||. (ctt-kind(snd(fst(snd(L[i])))) = (snd(ctt-arity(f)[i])))
8. (||L|| = 1)
{}\mRightarrow{} ((\muparrow{}ctt-opr-is(f;"pi"))
\mvee{} (\muparrow{}ctt-opr-is(f;"sigma"))
\mvee{} (\muparrow{}ctt-opr-is(f;"lambda"))
\mvee{} (\muparrow{}ctt-opr-is(f;"apply"))
\mvee{} (\muparrow{}ctt-opr-is(f;"pair"))
\mvee{} (\muparrow{}ctt-opr-is(f;"fst"))
\mvee{} (\muparrow{}ctt-opr-is(f;"snd")))
{}\mRightarrow{} ((fst(L[0])) = X)
9. (||L|| = 2)
{}\mRightarrow{} ((\muparrow{}ctt-opr-is(f;"Glue"))
\mvee{} (\muparrow{}ctt-opr-is(f;"case"))
\mvee{} (\muparrow{}ctt-opr-is(f;"comp"))
\mvee{} (\muparrow{}ctt-opr-is(f;"unglue"))
\mvee{} (\muparrow{}ctt-opr-is(f;"glue")))
{}\mRightarrow{} ((fst(L[0])) = X)
10. (||L|| = 2) {}\mRightarrow{} ((\muparrow{}ctt-opr-is(f;"Glue")) \mvee{} (\muparrow{}ctt-opr-is(f;"unglue"))) {}\mRightarrow{} ((fst(L[1])) = X)
11. (||L|| = 3)
{}\mRightarrow{} ((\muparrow{}ctt-opr-is(f;"Glue")) \mvee{} (\muparrow{}ctt-opr-is(f;"case")) \mvee{} (\muparrow{}ctt-opr-is(f;"unglue")))
{}\mRightarrow{} ((fst(L[1])) = X)
12. (||L|| = 3) {}\mRightarrow{} (\muparrow{}ctt-opr-is(f;"glue")) {}\mRightarrow{} ((fst(L[0])) = X)
13. (||L|| = 4) {}\mRightarrow{} (\muparrow{}ctt-opr-is(f;"glue")) {}\mRightarrow{} ((fst(L[0])) = X)
14. CubicalContext \mmember{} \mBbbU{}\{i'''''\}
15. ctxt : \{t:CubicalContext| allowed(X) \mwedge{} (t = allow(X))\}
\mvdash{} ctt-subterm-context\{i:l\}(ctxt;f;||L||;vs;if (ctt-opr-is(f;"Glue")
\mwedge{}\msubb{} ((||L|| =\msubz{} 2) \mvee{}\msubb{}(||L|| =\msubz{} 3)))
\mvee{}\msubb{}(ctt-opr-is(f;"case") \mwedge{}\msubb{} (||L|| =\msubz{} 3))
\mvee{}\msubb{}(ctt-opr-is(f;"unglue")
\mwedge{}\msubb{} ((||L|| =\msubz{} 2) \mvee{}\msubb{}(||L|| =\msubz{} 3)))
then snd(snd(L[1]))
else snd(snd(L[0]))
fi ) \mmember{} provisional-type\{i 4:l\}(CubicalContext)
By
Latex:
(DSetVars THEN ExRepD THEN MemCD THEN Try (Trivial))
Home
Index