Step * 2 of Lemma priority-select-ff


1. [T] : Type
2. as : T List
3. f : T āŸ¶ š”¹
4. g : T āŸ¶ š”¹
5. T āŠ†r ā„¤
6. āˆ€i:ā„•||as||. āˆ€j:ā„•i.  (as[j] ā‰¤ as[i])
7. (priority-select(f;g;as) = (inl ff) āˆˆ (š”¹?)) ā‡’ (āˆƒi:ā„•||as||. ((ā†‘(g as[i])) āˆ§ (āˆ€j:ā„•i + 1. (Ā¬ā†‘(f as[j])))))
8. (priority-select(f;g;as) = (inl ff) āˆˆ (š”¹?)) ā‡ āˆƒi:ā„•||as||. ((ā†‘(g as[i])) āˆ§ (āˆ€j:ā„•i + 1. (Ā¬ā†‘(f as[j]))))
9. (āˆƒaāˆˆas. (ā†‘(g a)) āˆ§ (āˆ€b:T. ((b āˆˆ as) ā‡’ Ā¬ā†‘(f b) supposing b ā‰¤ a)))
āŠ¢ āˆƒi:ā„•||as||. ((ā†‘(g as[i])) āˆ§ (āˆ€j:ā„•i + 1. (Ā¬ā†‘(f as[j]))))
BY
{ (D (-1) THEN With āŒœiāŒ (D 0)ā‹… THEN Auto THEN (BHyp (-3)) THEN Auto) }

1
1. T : Type
2. as : T List
3. f : T āŸ¶ š”¹
4. g : T āŸ¶ š”¹
5. T āŠ†r ā„¤
6. āˆ€i:ā„•||as||. āˆ€j:ā„•i.  (as[j] ā‰¤ as[i])
7. (priority-select(f;g;as) = (inl ff) āˆˆ (š”¹?)) ā‡’ (āˆƒi:ā„•||as||. ((ā†‘(g as[i])) āˆ§ (āˆ€j:ā„•i + 1. (Ā¬ā†‘(f as[j])))))
8. (priority-select(f;g;as) = (inl ff) āˆˆ (š”¹?)) ā‡ āˆƒi:ā„•||as||. ((ā†‘(g as[i])) āˆ§ (āˆ€j:ā„•i + 1. (Ā¬ā†‘(f as[j]))))
9. i : ā„•||as||
10. ā†‘(g as[i])
11. āˆ€b:T. ((b āˆˆ as) ā‡’ Ā¬ā†‘(f b) supposing b ā‰¤ as[i])
12. ā†‘(g as[i])
13. j : ā„•i + 1
āŠ¢ as[j] ā‰¤ as[i]

Latex:

Latex:

1.  [T]  :  Type
2.  as  :  T  List
3.  f  :  T  {}\mrightarrow{}  \mBbbB{}
4.  g  :  T  {}\mrightarrow{}  \mBbbB{}
5.  T  \msubseteq{}r  \mBbbZ{}
6.  \mforall{}i:\mBbbN{}||as||.  \mforall{}j:\mBbbN{}i.    (as[j]  \mleq{}  as[i])
7.  (priority-select(f;g;as)  =  (inl  ff))  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||as||.  ((\muparrow{}(g  as[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  as[j])))))
8.  (priority-select(f;g;as)  =  (inl  ff))  \mLeftarrow{}{}  \mexists{}i:\mBbbN{}||as||.  ((\muparrow{}(g  as[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  as[j]))))
9.  (\mexists{}a\mmember{}as.  (\muparrow{}(g  a))  \mwedge{}  (\mforall{}b:T.  ((b  \mmember{}  as)  {}\mRightarrow{}  \mneg{}\muparrow{}(f  b)  supposing  b  \mleq{}  a)))
\mvdash{}  \mexists{}i:\mBbbN{}||as||.  ((\muparrow{}(g  as[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  as[j]))))


By

Latex:
(D  (-1)  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  (BHyp  (-3))  THEN  Auto)



Home Index