---

Step * of Lemma non-null-list-tactic-test

∀T:Type. ∀L:T List. ∀x:T.
  (((((((((0 < ||L|| ∨ (1 ≤ ||L||)) ∨ null(L) = ff) ∨ null(L) = ff) ∨ (¬↑null(L))) ∨ (¬(L = [] ∈ (T List))))
    ∨ (¬([] = L ∈ (T List))))
    ∨ (¬null(L) = tt))
  ∨ (∃x:T. (x ∈ L))
  ∨ (x ∈ L)
  ∨ (L = [x / L] ∈ (T List)))
  ⇒ (((((((1 ≤ ||L||) ∧ null(L) = ff) ∧ (null(L) ~ ff)) ∧ (¬↑null(L))) ∧ (¬(L = [] ∈ (T List)))) ∧ (∃x:T. (x ∈ L)))
     ∧ (0 ≤ ||L||)))
BY
{ ((UnivCD THENA Auto) THEN SplitOrHyps THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}L:T  List.  \mforall{}x:T.
    (((((((((0  <  ||L||  \mvee{}  (1  \mleq{}  ||L||))  \mvee{}  null(L)  =  ff)  \mvee{}  null(L)  =  ff)  \mvee{}  (\mneg{}\muparrow{}null(L)))  \mvee{}  (\mneg{}(L  =  [])))
        \mvee{}  (\mneg{}([]  =  L)))
        \mvee{}  (\mneg{}null(L)  =  tt))
    \mvee{}  (\mexists{}x:T.  (x  \mmember{}  L))
    \mvee{}  (x  \mmember{}  L)
    \mvee{}  (L  =  [x  /  L]))
    {}\mRightarrow{}  (((((((1  \mleq{}  ||L||)  \mwedge{}  null(L)  =  ff)  \mwedge{}  (null(L)  \msim{}  ff))  \mwedge{}  (\mneg{}\muparrow{}null(L)))  \mwedge{}  (\mneg{}(L  =  [])))
          \mwedge{}  (\mexists{}x:T.  (x  \mmember{}  L)))
          \mwedge{}  (0  \mleq{}  ||L||)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  SplitOrHyps  THEN  Auto)

---

Home Index