Step
*
2
2
1
2
of Lemma
priority-select-property
1. [T] : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
     ((priority-select(f;g;v) = (inl tt) ∈ (𝔹?) 
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
     ∧ (priority-select(f;g;v) = (inl ff) ∈ (𝔹?) 
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
     ∧ (priority-select(f;g;v) = (inr ⋅ ) ∈ (𝔹?) 
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ↑(g u)
⊢ ((inl ff) = (inl tt) ∈ (𝔹?) 
⇐⇒ ∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j])))))
∧ ((inl ff) = (inl ff) ∈ (𝔹?) 
⇐⇒ ∃i:ℕ||v|| + 1. ((↑(g [u / v][i])) ∧ (∀j:ℕi + 1. (¬↑(f [u / v][j])))))
∧ ((inl ff) = (inr ⋅ ) ∈ (𝔹?) 
⇐⇒ ∀i:ℕ||v|| + 1. ((¬↑(f [u / v][i])) ∧ (¬↑(g [u / v][i]))))
BY
{ TACTIC:Auto }
1
.....subterm..... T:t
1:n
1. T : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
     ((priority-select(f;g;v) = (inl tt) ∈ (𝔹?) 
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
     ∧ (priority-select(f;g;v) = (inl ff) ∈ (𝔹?) 
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
     ∧ (priority-select(f;g;v) = (inr ⋅ ) ∈ (𝔹?) 
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ↑(g u)
9. ∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j]))))
⊢ ff = tt
2
1. [T] : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
     ((priority-select(f;g;v) = (inl tt) ∈ (𝔹?) 
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
     ∧ (priority-select(f;g;v) = (inl ff) ∈ (𝔹?) 
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
     ∧ (priority-select(f;g;v) = (inr ⋅ ) ∈ (𝔹?) 
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ↑(g u)
9. ((inl ff) = (inl tt) ∈ (𝔹?)) 
⇒ (∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j])))))
10. ((inl ff) = (inl tt) ∈ (𝔹?)) 
⇐ ∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j]))))
11. ff = ff
⊢ ∃i:ℕ||v|| + 1. ((↑(g [u / v][i])) ∧ (∀j:ℕi + 1. (¬↑(f [u / v][j]))))
3
1. T : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
     ((priority-select(f;g;v) = (inl tt) ∈ (𝔹?) 
⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
     ∧ (priority-select(f;g;v) = (inl ff) ∈ (𝔹?) 
⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
     ∧ (priority-select(f;g;v) = (inr ⋅ ) ∈ (𝔹?) 
⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ↑(g u)
9. ((inl ff) = (inl tt) ∈ (𝔹?)) 
⇒ (∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j])))))
10. ((inl ff) = (inl tt) ∈ (𝔹?)) 
⇐ ∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j]))))
11. ((inl ff) = (inl ff) ∈ (𝔹?)) 
⇒ (∃i:ℕ||v|| + 1. ((↑(g [u / v][i])) ∧ (∀j:ℕi + 1. (¬↑(f [u / v][j])))))
12. ((inl ff) = (inl ff) ∈ (𝔹?)) 
⇐ ∃i:ℕ||v|| + 1. ((↑(g [u / v][i])) ∧ (∀j:ℕi + 1. (¬↑(f [u / v][j]))))
13. ∀i:ℕ||v|| + 1. ((¬↑(f [u / v][i])) ∧ (¬↑(g [u / v][i])))
⊢ (inl ff) = (inr ⋅ ) ∈ (𝔹?)
Latex:
Latex:
1.  [T]  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}f,g:T  {}\mrightarrow{}  \mBbbB{}.
          ((priority-select(f;g;v)  =  (inl  tt)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(f  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(g  v[j])))))
          \mwedge{}  (priority-select(f;g;v)  =  (inl  ff)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(g  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  v[j])))))
          \mwedge{}  (priority-select(f;g;v)  =  (inr  \mcdot{}  )  \mLeftarrow{}{}\mRightarrow{}  \mforall{}i:\mBbbN{}||v||.  ((\mneg{}\muparrow{}(f  v[i]))  \mwedge{}  (\mneg{}\muparrow{}(g  v[i])))))
5.  f  :  T  {}\mrightarrow{}  \mBbbB{}
6.  g  :  T  {}\mrightarrow{}  \mBbbB{}
7.  \mneg{}\muparrow{}(f  u)
8.  \muparrow{}(g  u)
\mvdash{}  ((inl  ff)  =  (inl  tt)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||  +  1.  ((\muparrow{}(f  [u  /  v][i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(g  [u  /  v][j])))))
\mwedge{}  ((inl  ff)  =  (inl  ff)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||  +  1.  ((\muparrow{}(g  [u  /  v][i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  [u  /  v][j])))))
\mwedge{}  ((inl  ff)  =  (inr  \mcdot{}  )  \mLeftarrow{}{}\mRightarrow{}  \mforall{}i:\mBbbN{}||v||  +  1.  ((\mneg{}\muparrow{}(f  [u  /  v][i]))  \mwedge{}  (\mneg{}\muparrow{}(g  [u  /  v][i]))))
By
Latex:
TACTIC:Auto
Home
Index