Step * of Lemma filter_interleaving_occurence

No Annotations
[T:Type]
  ∀P:T ⟶ 𝔹. ∀L:T List.
    ∃f1:ℕ||filter(λx.(¬b(P x));L)|| ⟶ ℕ||L||
     ∃f2:ℕ||filter(P;L)|| ⟶ ℕ||L||
      (interleaving_occurence(T;filter(λx.(¬b(P x));L);filter(P;L);L;f1;f2)
      ∧ ((∀i:ℕ||L||. ∃k:ℕ||filter(P;L)||. ((i (f2 k) ∈ ℤ) ∧ (L[i] filter(P;L)[k] ∈ T)) supposing ↑(P L[i]))
        ∧ (∀i:ℕ||L||
             ∃k:ℕ||filter(λx.(¬b(P x));L)||. ((i (f1 k) ∈ ℤ) ∧ (L[i] filter(λx.(¬b(P x));L)[k] ∈ T)) 
             supposing ¬↑(P L[i])))
      ∧ (∀i:ℕ||filter(λx.(¬b(P x));L)||. (¬↑(P L[f1 i])))
      ∧ (∀i:ℕ||filter(P;L)||. (↑(P L[f2 i]))))
BY
(Auto
   THEN Assert ∃f1:ℕ||filter(λx.(¬b(P x));L)|| ⟶ ℕ||L||
                ∃f2:ℕ||filter(P;L)|| ⟶ ℕ||L||. interleaving_occurence(T;filter(λx.(¬b(P x));L);filter(P;L);L;f1;f2)
   }

1
.....assertion..... 
1. [T] Type
2. T ⟶ 𝔹@i
3. List@i
⊢ ∃f1:ℕ||filter(λx.(¬b(P x));L)|| ⟶ ℕ||L||
   ∃f2:ℕ||filter(P;L)|| ⟶ ℕ||L||. interleaving_occurence(T;filter(λx.(¬b(P x));L);filter(P;L);L;f1;f2)

2
1. [T] Type
2. T ⟶ 𝔹@i
3. List@i
4. ∃f1:ℕ||filter(λx.(¬b(P x));L)|| ⟶ ℕ||L||
    ∃f2:ℕ||filter(P;L)|| ⟶ ℕ||L||. interleaving_occurence(T;filter(λx.(¬b(P x));L);filter(P;L);L;f1;f2)
⊢ ∃f1:ℕ||filter(λx.(¬b(P x));L)|| ⟶ ℕ||L||
   ∃f2:ℕ||filter(P;L)|| ⟶ ℕ||L||
    (interleaving_occurence(T;filter(λx.(¬b(P x));L);filter(P;L);L;f1;f2)
    ∧ ((∀i:ℕ||L||. ∃k:ℕ||filter(P;L)||. ((i (f2 k) ∈ ℤ) ∧ (L[i] filter(P;L)[k] ∈ T)) supposing ↑(P L[i]))
      ∧ (∀i:ℕ||L||
           ∃k:ℕ||filter(λx.(¬b(P x));L)||. ((i (f1 k) ∈ ℤ) ∧ (L[i] filter(λx.(¬b(P x));L)[k] ∈ T)) 
           supposing ¬↑(P L[i])))
    ∧ (∀i:ℕ||filter(λx.(¬b(P x));L)||. (¬↑(P L[f1 i])))
    ∧ (∀i:ℕ||filter(P;L)||. (↑(P L[f2 i]))))


Latex:


Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.
        \mexists{}f1:\mBbbN{}||filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L)||  {}\mrightarrow{}  \mBbbN{}||L||
          \mexists{}f2:\mBbbN{}||filter(P;L)||  {}\mrightarrow{}  \mBbbN{}||L||
            (interleaving\_occurence(T;filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L);filter(P;L);L;f1;f2)
            \mwedge{}  ((\mforall{}i:\mBbbN{}||L||
                        \mexists{}k:\mBbbN{}||filter(P;L)||.  ((i  =  (f2  k))  \mwedge{}  (L[i]  =  filter(P;L)[k]))  supposing  \muparrow{}(P  L[i]))
                \mwedge{}  (\mforall{}i:\mBbbN{}||L||
                          \mexists{}k:\mBbbN{}||filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L)||.  ((i  =  (f1  k))  \mwedge{}  (L[i]  =  filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L)[k])) 
                          supposing  \mneg{}\muparrow{}(P  L[i])))
            \mwedge{}  (\mforall{}i:\mBbbN{}||filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L)||.  (\mneg{}\muparrow{}(P  L[f1  i])))
            \mwedge{}  (\mforall{}i:\mBbbN{}||filter(P;L)||.  (\muparrow{}(P  L[f2  i]))))


By


Latex:
(Auto
  THEN  Assert  \mexists{}f1:\mBbbN{}||filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L)||  {}\mrightarrow{}  \mBbbN{}||L||
                            \mexists{}f2:\mBbbN{}||filter(P;L)||  {}\mrightarrow{}  \mBbbN{}||L||
                              interleaving\_occurence(T;filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L);filter(P;L);L;f1;f2)
  )




Home Index