Proof of Nuprl Lemma : provisional-subterm-context

Step * of Lemma provisional-subterm-context_wf

No Annotations
∀[X:?CubicalContext]. ∀[f:CttOp]. ∀[vs:varname() List]. ∀[L:{L:(a:?CubicalContext

                                                             × bt:varname() List × CttTerm

                                                             × [[a;snd(bt)]]) List|

                                                             ||L|| < ||ctt-arity(f)||

                                                             ∧ (||vs|| = (fst(ctt-arity(f)[||L||])) ∈ ℤ)

                                                             ∧ (∀i:ℕ||L||

                                                                  (ctt-kind(snd(fst(snd(L[i]))))

                                                                  = (snd(ctt-arity(f)[i]))

                                                                  ∈ ℤ))

                                                             ∧ ((||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 ∈ ?CubicalContext))

                                                             ∧ ((||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 ∈ ?CubicalContext))

                                                             ∧ ((||L|| = 2 ∈ ℤ)

⇒ ((↑ctt-opr-is(f;"Glue")) ∨ (↑ctt-opr-is(f;"unglue")))

⇒ ((fst(L[1])) = X ∈ ?CubicalContext))

                                                             ∧ ((||L|| = 3 ∈ ℤ)

⇒ ((↑ctt-opr-is(f;"Glue"))

                                                                  ∨ (↑ctt-opr-is(f;"case"))

                                                                  ∨ (↑ctt-opr-is(f;"unglue")))

⇒ ((fst(L[1])) = X ∈ ?CubicalContext))

                                                             ∧ ((||L|| = 3 ∈ ℤ)

⇒ (↑ctt-opr-is(f;"glue"))

⇒ ((fst(L[0])) = X ∈ ?CubicalContext))

                                                             ∧ ((||L|| = 4 ∈ ℤ)

⇒ (↑ctt-opr-is(f;"glue"))

⇒ ((fst(L[0])) = X ∈ ?CubicalContext))} ].
  (provisional-subterm-context{i:l}(X;f;vs;L) ∈ ?CubicalContext)
BY
{ (Unfold `cubical-context` 0
   THEN Intros
   THEN Unhide
   THEN Unfold `provisional-subterm-context` 0
   THEN (Assert CubicalContext ∈ 𝕌{i'''''} BY
               Auto)
   THEN DSetVars
   THEN ExRepD
   THEN ((MemCD THEN Try (Trivial)) THENW Auto)) }

1
.....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)

Latex:

Latex:
No Annotations \mforall{}[X:?CubicalContext]. \mforall{}[f:CttOp]. \mforall{}[vs:varname() List]. \mforall{}[L:\{L:(a:?CubicalContext \mtimes{} bt:varname() List \mtimes{} CttTerm \mtimes{} [[a;snd(bt)]]) List| ||L|| < ||ctt-arity(f)|| \mwedge{} (||vs|| = (fst(ctt-arity(f)[||L||]))) \mwedge{} (\mforall{}i:\mBbbN{}||L|| (ctt-kind(snd(fst(snd(L[i])))) = (snd(ctt-arity(f)[i])))) \mwedge{} ((||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)) \mwedge{} ((||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)) \mwedge{} ((||L|| = 2) {}\mRightarrow{} ((\muparrow{}ctt-opr-is(f;"Glue")) \mvee{} (\muparrow{}ctt-opr-is(f;"unglue"))) {}\mRightarrow{} ((fst(L[1])) = X)) \mwedge{} ((||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)) \mwedge{} ((||L|| = 3) {}\mRightarrow{} (\muparrow{}ctt-opr-is(f;"glue")) {}\mRightarrow{} ((fst(L[0])) = X)) \mwedge{} ((||L|| = 4) {}\mRightarrow{} (\muparrow{}ctt-opr-is(f;"glue")) {}\mRightarrow{} ((fst(L[0])) = X))\} ]. (provisional-subterm-context\{i:l\}(X;f;vs;L) \mmember{} ?CubicalContext) By Latex: (Unfold `cubical-context` 0 THEN Intros THEN Unhide THEN Unfold `provisional-subterm-context` 0 THEN (Assert CubicalContext \mmember{} \mBbbU{}\{i'''''\} BY Auto) THEN DSetVars THEN ExRepD THEN ((MemCD THEN Try (Trivial)) THENW Auto)) Home Index