---

Step * of Lemma W-elimination-facts

∀A:Type. ∀B:A ⟶ Type. ∀w:W(A;a.B[a]).
  ((cw-step(A;a.B[a]) ∈ Type)
  ∧ (W-rel(A;a.B[a];w) ∈ n:ℕ ⟶ (ℕn ⟶ cw-step(A;a.B[a])) ⟶ cw-step(A;a.B[a]) ⟶ ℙ)
  ∧ (W(A;a.B[a]) ∈ Type)
  ∧ (W(A;a.B[a]) ⊆r (pco-W ⋅))
  ∧ (∀n:ℕ. ∀s:ℕn ⟶ cw-step(A;a.B[a]).  (Barred(<n, s>) ∨ (¬Barred(<n, s>))))
  ∧ (∀alpha:ℕ ⟶ cw-step(A;a.B[a]). ((∀n:ℕ. (W-rel(A;a.B[a];w) n alpha (alpha n))) ⇒ (alpha ∈ Path)))
  ∧ (∀[pp:n:ℕ × (ℕn ⟶ cw-step(A;a.B[a]))]. (Barred(pp) ∈ ℙ))
  ∧ (∀alpha:ℕ ⟶ cw-step(A;a.B[a]). ((∀n:ℕ. (W-rel(A;a.B[a];w) n alpha (alpha n))) ⇒ (↓∃n:ℕ. Barred(<n, alpha>))))
  ∧ (∀a:A. ∀x1:B[a] ⟶ W(A;a.B[a]). ∀n:ℕ+. ∀s:ℕn ⟶ cw-step(A;a.B[a]). ∀a1:A. ∀w1:b:B[a1] ⟶ (pco-W ⋅). ∀x:B[a1]. ∀a2:A.
     ∀z1:b:B[a2] ⟶ (pco-W ⋅).
       ((∀k:ℕn. (W-rel(A;a.B[a];<a, x1>) k s (s k)))
       ⇒ ((s (n - 1)) = <⋅, <a1, w1>, inl x> ∈ cw-step(A;a.B[a]))
       ⇒ ((w1 x) = <a2, z1> ∈ (pco-W ⋅))
       ⇒ (z1 ∈ B[a2] ⟶ W(A;a.B[a])))))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN BetterSplitAndConcl
          THEN Try ((BLemma `cw-step_wf` THEN Auto))
          THEN Try ((BLemma `W_wf` THEN Auto))
          THEN Try ((BLemma `W-rel_wf` THEN Auto))
          THEN Try (((InstLemma `W-path-lemma` [⌜A⌝;⌜B⌝;⌜w⌝]⋅ THENM Trivial) THENA Auto))
          THEN Try (((InstLemma `pcw-pp-barred-W` [⌜A⌝;⌜B⌝]⋅ THENM Trivial) THEN Auto))
          THEN Try ((RepUR ``W param-W`` 0 THEN Complete (Auto)))
          THEN Try (((InstLemma `W-path-lemma2` [⌜A⌝;⌜B⌝]⋅ THENA Auto) THEN Trivial))
          THEN Try ((Auto
                     THEN Seq [ Assert ⌜0 ∈ ℕ⌝ THENA Auto
                                 ; (OnVar `w' (RepUR ``W param-W``) THEN OnVar `w' D THEN Unhide THEN Auto)
                                 ; Fold `pcw-partial` 0 THEN BackThruSomeHyp
                                 ; Try (InstHyp [⌜0⌝] (-2) THENA Trivial
                                       THEN MoveToConcl (-1)
                                       THEN RepUR ``W-rel param-W-rel`` 0
                                       THEN (D 0 THENM NthHyp (-1))
                                       THEN Auto
                                       )
                                 ]⋅
                     ))) }

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}w:W(A;a.B[a]).
    ((cw-step(A;a.B[a])  \mmember{}  Type)
    \mwedge{}  (W-rel(A;a.B[a];w)  \mmember{}  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  cw-step(A;a.B[a]))  {}\mrightarrow{}  cw-step(A;a.B[a])  {}\mrightarrow{}  \mBbbP{})
    \mwedge{}  (W(A;a.B[a])  \mmember{}  Type)
    \mwedge{}  (W(A;a.B[a])  \msubseteq{}r  (pco-W  \mcdot{}))
    \mwedge{}  (\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  cw-step(A;a.B[a]).    (Barred(<n,  s>)  \mvee{}  (\mneg{}Barred(<n,  s>))))
    \mwedge{}  (\mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  cw-step(A;a.B[a])
              ((\mforall{}n:\mBbbN{}.  (W-rel(A;a.B[a];w)  n  alpha  (alpha  n)))  {}\mRightarrow{}  (alpha  \mmember{}  Path)))
    \mwedge{}  (\mforall{}[pp:n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  cw-step(A;a.B[a]))].  (Barred(pp)  \mmember{}  \mBbbP{}))
    \mwedge{}  (\mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  cw-step(A;a.B[a])
              ((\mforall{}n:\mBbbN{}.  (W-rel(A;a.B[a];w)  n  alpha  (alpha  n)))  {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(<n,  alpha>))))
    \mwedge{}  (\mforall{}a:A.  \mforall{}x1:B[a]  {}\mrightarrow{}  W(A;a.B[a]).  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  cw-step(A;a.B[a]).  \mforall{}a1:A.  \mforall{}w1:b:B[a1]  {}\mrightarrow{}  (pco-W 
                                                                                                                                                                                            \mcdot{}).
          \mforall{}x:B[a1].  \mforall{}a2:A.  \mforall{}z1:b:B[a2]  {}\mrightarrow{}  (pco-W  \mcdot{}).
              ((\mforall{}k:\mBbbN{}n.  (W-rel(A;a.B[a];<a,  x1>)  k  s  (s  k)))
              {}\mRightarrow{}  ((s  (n  -  1))  =  <\mcdot{},  <a1,  w1>,  inl  x>)
              {}\mRightarrow{}  ((w1  x)  =  <a2,  z1>)
              {}\mRightarrow{}  (z1  \mmember{}  B[a2]  {}\mrightarrow{}  W(A;a.B[a])))))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  BetterSplitAndConcl
                THEN  Try  ((BLemma  `cw-step\_wf`  THEN  Auto))
                THEN  Try  ((BLemma  `W\_wf`  THEN  Auto))
                THEN  Try  ((BLemma  `W-rel\_wf`  THEN  Auto))
                THEN  Try  (((InstLemma  `W-path-lemma`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}  THENM  Trivial)  THENA  Auto))
                THEN  Try  (((InstLemma  `pcw-pp-barred-W`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENM  Trivial)  THEN  Auto))
                THEN  Try  ((RepUR  ``W  param-W``  0  THEN  Complete  (Auto)))
                THEN  Try  (((InstLemma  `W-path-lemma2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Trivial))
                THEN  Try  ((Auto
                                      THEN  Seq  [  Assert  \mkleeneopen{}0  \mmember{}  \mBbbN{}\mkleeneclose{}  THENA  Auto
                                                              ;  (OnVar  `w'  (RepUR  ``W  param-W``)
                                                                    THEN  OnVar  `w'  D
                                                                    THEN  Unhide
                                                                    THEN  Auto)
                                                              ;  Fold  `pcw-partial`  0  THEN  BackThruSomeHyp
                                                              ;  Try  (InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-2)  THENA  Trivial
                                                                          THEN  MoveToConcl  (-1)
                                                                          THEN  RepUR  ``W-rel  param-W-rel``  0
                                                                          THEN  (D  0  THENM  NthHyp  (-1))
                                                                          THEN  Auto
                                                                          )
                                                              ]\mcdot{}
                                      )))

---

Home Index