Step * of Lemma first-member-iff

[T:Type]
  ∀L:T List. ∀P:T ⟶ 𝔹. ∀x:T.
    (first-member(T;x;L;P) ⇐⇒ ∃K,J:T List. ((L (K [x J]) ∈ (T List)) ∧ (↑(P x)) ∧ (∀y∈K.¬↑(P y))))
BY
(Auto THEN All(RepUR ``first-member``) THEN ExRepD) }

1
1. [T] Type
2. List
3. T ⟶ 𝔹
4. T
5. : ℕ||L||
6. L[i] ∈ T
7. ↑(P x)
8. ∀j:ℕi. (¬↑(P L[j]))
⊢ ∃K,J:T List. ((L (K [x J]) ∈ (T List)) ∧ (↑(P x)) ∧ (∀y∈K.¬↑(P y)))

2
1. [T] Type
2. List
3. T ⟶ 𝔹
4. T
5. List
6. List
7. (K [x J]) ∈ (T List)
8. ↑(P x)
9. (∀y∈K.¬↑(P y))
⊢ ∃i:ℕ||L||. ((x L[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P L[j]))))


Latex:


Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:T.
        (first-member(T;x;L;P)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}K,J:T  List.  ((L  =  (K  @  [x  /  J]))  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}y\mmember{}K.\mneg{}\muparrow{}(P  y))))


By


Latex:
(Auto  THEN  All(RepUR  ``first-member``)  THEN  ExRepD)




Home Index