---

Step * of Lemma ctt-subterm-context_wf

No Annotations
∀[ctxt:CubicalContext]. ∀[f:CttOp]. ∀[n:ℕ]. ∀[vs:varname() List].
∀[m:Provisional''''(cttTerm(fst(ctxt))) 
    supposing ↑(((ctt-opr-is(f;"Glue") ∨bctt-opr-is(f;"case") ∨bctt-opr-is(f;"unglue")) ∧b ((n =z 2) ∨b(n =z 3)))
    ∨b(ctt-opr-is(f;"comp") ∧b (n =z 2))
    ∨b(ctt-opr-is(f;"glue") ∧b ((n =z 2) ∨b(n =z 3) ∨b(n =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 (n =z 1))].
  ctt-subterm-context{i:l}(ctxt;f;n;vs;m) ∈ ?CubicalContext 
  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")
  ∨bctt-opr-is(f;"pathabs")
  ∨bctt-opr-is(f;"comp"))
  ∧b (n =z 1))
  ∨b(ctt-opr-is(f;"comp") ∧b (n =z 2))))
  ⇒ 0 < ||vs||
BY
{ (Intros
   THEN ((Unhide THEN (Assert fst(ctxt) ⊢''' BY (D 1 THEN Auto))) ORELSE (D 1 THEN Reduce 0 THEN Auto))
   THEN RepeatFor 2 (D 2)
   THEN Repeat ((GenListD 3
                 THEN ((D 3 THENL [(Eliminate ⌜k⌝⋅ THEN Reduce 4); Id]) ORELSE (Eliminate ⌜k⌝⋅ THEN Reduce 4))
                 ))
   THEN Try ((RepUR ``ctt-subterm-context ctt-opr-is cubical-context`` 0
              THEN MemCD
              THEN ((Unfold `uimplies` 0 THEN MemTypeCD) ORELSE MemCD)
              THEN (Declaration ORELSE D 0)))
   THEN (Assert OK(ctxt) ∈ Provisional''''(CubicalContext) BY
               Auto)
   THEN D 4
   THEN Repeat ((GenListD 5
                 THEN ((D 5 THENL [(Eliminate ⌜f1⌝⋅ THEN Reduce 4); Id]) ORELSE (Eliminate ⌜f1⌝⋅ THEN Reduce 4))
                 ))
   THEN (RepUR ``ctt-opr-is`` -2 THEN RepUR ``ctt-opr-is`` -1)
   THEN RepUR ``ctt-subterm-context ctt-opr-is cubical-context`` 0
   THEN Try (Trivial)
   THEN Repeat (((SplitOnConclITE THENA Auto) THEN Try (Trivial)))
   THEN Try (DOr (-1))
   THEN Eliminate ⌜n⌝⋅
   THEN (RepUR ``ctt-opr-is`` 9 THEN Reduce 9)
   THEN RepUR ``ctt-opr-is`` 8
   THEN Reduce 8
   THEN Isect2HD 8
   THEN Auto
   THEN RepUR ``ctt-level-type`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[ctxt:CubicalContext].  \mforall{}[f:CttOp].  \mforall{}[n:\mBbbN{}].  \mforall{}[vs:varname()  List].
\mforall{}[m:Provisional''''(cttTerm(fst(ctxt))) 
        supposing  \muparrow{}(((ctt-opr-is(f;"Glue")  \mvee{}\msubb{}ctt-opr-is(f;"case")  \mvee{}\msubb{}ctt-opr-is(f;"unglue"))
                                \mwedge{}\msubb{}  ((n  =\msubz{}  2)  \mvee{}\msubb{}(n  =\msubz{}  3)))
        \mvee{}\msubb{}(ctt-opr-is(f;"comp")  \mwedge{}\msubb{}  (n  =\msubz{}  2))
        \mvee{}\msubb{}(ctt-opr-is(f;"glue")
            \mwedge{}\msubb{}  ((n  =\msubz{}  2)  \mvee{}\msubb{}(n  =\msubz{}  3)  \mvee{}\msubb{}(n  =\msubz{}  4))))  \mcap{}  Provisional''''(ctt-type-meaning1\{i:l\}(fst(ctxt))) 
                                                                                            supposing  \muparrow{}((ctt-opr-is(f;"pi")
                                                                                            \mvee{}\msubb{}ctt-opr-is(f;"sigma")
                                                                                            \mvee{}\msubb{}ctt-opr-is(f;"lambda")
                                                                                            \mvee{}\msubb{}ctt-opr-is(f;"apply")
                                                                                            \mvee{}\msubb{}ctt-opr-is(f;"pair")
                                                                                            \mvee{}\msubb{}ctt-opr-is(f;"fst")
                                                                                            \mvee{}\msubb{}ctt-opr-is(f;"snd"))
                                                                                            \mwedge{}\msubb{}  (n  =\msubz{}  1))].
    ctt-subterm-context\{i:l\}(ctxt;f;n;vs;m)  \mmember{}  ?CubicalContext 
    supposing  (\muparrow{}(((ctt-opr-is(f;"pi")
    \mvee{}\msubb{}ctt-opr-is(f;"sigma")
    \mvee{}\msubb{}ctt-opr-is(f;"lambda")
    \mvee{}\msubb{}ctt-opr-is(f;"apply")
    \mvee{}\msubb{}ctt-opr-is(f;"pair")
    \mvee{}\msubb{}ctt-opr-is(f;"fst")
    \mvee{}\msubb{}ctt-opr-is(f;"snd")
    \mvee{}\msubb{}ctt-opr-is(f;"pathabs")
    \mvee{}\msubb{}ctt-opr-is(f;"comp"))
    \mwedge{}\msubb{}  (n  =\msubz{}  1))
    \mvee{}\msubb{}(ctt-opr-is(f;"comp")  \mwedge{}\msubb{}  (n  =\msubz{}  2))))
    {}\mRightarrow{}  0  <  ||vs||


By

---

Latex:
(Intros
  THEN  ((Unhide  THEN  (Assert  fst(ctxt)  \mvdash{}'''  BY  (D  1  THEN  Auto)))
  ORELSE  (D  1  THEN  Reduce  0  THEN  Auto)
  )
  THEN  RepeatFor  2  (D  2)
  THEN  Repeat  ((GenListD  3
                              THEN  ((D  3  THENL  [(Eliminate  \mkleeneopen{}k\mkleeneclose{}\mcdot{}  THEN  Reduce  4);  Id])
                                        ORELSE  (Eliminate  \mkleeneopen{}k\mkleeneclose{}\mcdot{}  THEN  Reduce  4)
                                        )
                              ))
  THEN  Try  ((RepUR  ``ctt-subterm-context  ctt-opr-is  cubical-context``  0
                        THEN  MemCD
                        THEN  ((Unfold  `uimplies`  0  THEN  MemTypeCD)  ORELSE  MemCD)
                        THEN  (Declaration  ORELSE  D  0)))
  THEN  (Assert  OK(ctxt)  \mmember{}  Provisional''''(CubicalContext)  BY
                          Auto)
  THEN  D  4
  THEN  Repeat  ((GenListD  5
                              THEN  ((D  5  THENL  [(Eliminate  \mkleeneopen{}f1\mkleeneclose{}\mcdot{}  THEN  Reduce  4);  Id])
                                        ORELSE  (Eliminate  \mkleeneopen{}f1\mkleeneclose{}\mcdot{}  THEN  Reduce  4)
                                        )
                              ))
  THEN  (RepUR  ``ctt-opr-is``  -2  THEN  RepUR  ``ctt-opr-is``  -1)
  THEN  RepUR  ``ctt-subterm-context  ctt-opr-is  cubical-context``  0
  THEN  Try  (Trivial)
  THEN  Repeat  (((SplitOnConclITE  THENA  Auto)  THEN  Try  (Trivial)))
  THEN  Try  (DOr  (-1))
  THEN  Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
  THEN  (RepUR  ``ctt-opr-is``  9  THEN  Reduce  9)
  THEN  RepUR  ``ctt-opr-is``  8
  THEN  Reduce  8
  THEN  Isect2HD  8
  THEN  Auto
  THEN  RepUR  ``ctt-level-type``  0
  THEN  Auto)

---

Home Index