//
// Generated by the Resolve Verifier, November 2007 version
// from file:  Isabelle_Selection_Sort_Realiz.rb
// on:         Wed Feb 27 11:46:18 EST 2008
//

Free Variables: Max_Length:*Z, min_int:*Z, max_int:*Z, Q:*Str(*Entry), min:*Entry, ?x:*Entry, ?temp:*Str(*Entry), ?Q:*Str(*Entry), ??min:*Entry, ???Q:*Str(*Entry), x:*Entry, temp:*Str(*Entry)



(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q))
_____________________________
IsPermutation(((empty_string o ???Q) o <??min>), Q)

(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q))
_____________________________
IsASmallest((empty_string o <??min>), ??min)

((((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q)) and ((IsPermutation(((?temp o ??Q) o <?min>), Q) and IsASmallest((?temp o <?min>), ?min)) and (|??Q| /= 0 and (??Q = (<?x> o ?Q) and LEQV(?x, ?min)))))
_____________________________
(|?temp| < Max_Length)

((((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q)) and ((IsPermutation(((?temp o ??Q) o <?min>), Q) and IsASmallest((?temp o <?min>), ?min)) and (|??Q| /= 0 and (??Q = (<?x> o ?Q) and LEQV(?x, ?min)))))
_____________________________
IsPermutation((((?temp o <?min>) o ?Q) o <?x>), Q)

((((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q)) and ((IsPermutation(((?temp o ??Q) o <?min>), Q) and IsASmallest((?temp o <?min>), ?min)) and (|??Q| /= 0 and (??Q = (<?x> o ?Q) and LEQV(?x, ?min)))))
_____________________________
IsASmallest(((?temp o <?min>) o <?x>), ?x)

((((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q)) and ((IsPermutation(((?temp o ??Q) o <?min>), Q) and IsASmallest((?temp o <?min>), ?min)) and (|??Q| /= 0 and (??Q = (<?x> o ?Q) and LEQV(?x, ?min)))))
_____________________________
(|?Q| < |??Q|)




Free Variables: Max_Length:*Z, min_int:*Z, max_int:*Z, Q:*Str(*Entry), min:*Entry, ?x:*Entry, ?temp:*Str(*Entry), ?Q:*Str(*Entry), ??min:*Entry, ???Q:*Str(*Entry), x:*Entry, temp:*Str(*Entry)



(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q))
_____________________________
IsPermutation(((empty_string o ???Q) o <??min>), Q)

(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q))
_____________________________
IsASmallest((empty_string o <??min>), ??min)

((((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q)) and ((IsPermutation(((?temp o ??Q) o <?min>), Q) and IsASmallest((?temp o <?min>), ?min)) and (|??Q| /= 0 and (??Q = (<?x> o ?Q) and not(LEQV(?x, ?min))))))
_____________________________
(|?temp| < Max_Length)

((((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q)) and ((IsPermutation(((?temp o ??Q) o <?min>), Q) and IsASmallest((?temp o <?min>), ?min)) and (|??Q| /= 0 and (??Q = (<?x> o ?Q) and not(LEQV(?x, ?min))))))
_____________________________
IsPermutation((((?temp o <?x>) o ?Q) o <?min>), Q)

((((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q)) and ((IsPermutation(((?temp o ??Q) o <?min>), Q) and IsASmallest((?temp o <?min>), ?min)) and (|??Q| /= 0 and (??Q = (<?x> o ?Q) and not(LEQV(?x, ?min))))))
_____________________________
IsASmallest(((?temp o <?x>) o <?min>), ?min)

((((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q)) and ((IsPermutation(((?temp o ??Q) o <?min>), Q) and IsASmallest((?temp o <?min>), ?min)) and (|??Q| /= 0 and (??Q = (<?x> o ?Q) and not(LEQV(?x, ?min))))))
_____________________________
(|?Q| < |??Q|)




Free Variables: Max_Length:*Z, min_int:*Z, max_int:*Z, Q:*Str(*Entry), min:*Entry, ?P_val:*N, ??min:*Entry, ??Q:*Str(*Entry), x:*Entry, temp:*Str(*Entry)



(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and (Q = (<??min> o ??Q) and ((IsPermutation(((?temp o ?Q) o <?min>), Q) and IsASmallest((?temp o <?min>), ?min)) and |?Q| = 0)))
_____________________________
IsPermutation((?temp o <?min>), Q)

(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and (Q = (<??min> o ??Q) and ((IsPermutation(((?temp o ?Q) o <?min>), Q) and IsASmallest((?temp o <?min>), ?min)) and |?Q| = 0)))
_____________________________
IsASmallest(Q, ?min)




Free Variables: Max_Length:*Z, min_int:*Z, max_int:*Z, Q:*Str(*Entry), ?min:*Entry, ?sorted:*Str(*Entry), ?Q:*Str(*Entry), min:*Entry, sorted:*Str(*Entry)



((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (|Q| <= Max_Length))
_____________________________
IsPermutation((Q o empty_string), Q)

((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (|Q| <= Max_Length))
_____________________________
IsNondecreasing(empty_string)

((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (|Q| <= Max_Length))
_____________________________
for all y:Entry, If IsSubstring(<y>, Q) then (IsNondecreasing((empty_string o <y>)))

(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (|Q| <= Max_Length)) and (((IsPermutation((??Q o ?sorted), Q) and IsNondecreasing(?sorted)) and for all y:Entry, If IsSubstring(<y>, ??Q) then (IsNondecreasing((?sorted o <y>)))) and (|??Q| /= 0 and (IsPermutation((?Q o <?min>), ??Q) and IsASmallest(??Q, ?min)))))
_____________________________
(|?sorted| < Max_Length)

(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (|Q| <= Max_Length)) and (((IsPermutation((??Q o ?sorted), Q) and IsNondecreasing(?sorted)) and for all y:Entry, If IsSubstring(<y>, ??Q) then (IsNondecreasing((?sorted o <y>)))) and (|??Q| /= 0 and (IsPermutation((?Q o <?min>), ??Q) and IsASmallest(??Q, ?min)))))
_____________________________
IsPermutation((?Q o (?sorted o <?min>)), Q)

(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (|Q| <= Max_Length)) and (((IsPermutation((??Q o ?sorted), Q) and IsNondecreasing(?sorted)) and for all y:Entry, If IsSubstring(<y>, ??Q) then (IsNondecreasing((?sorted o <y>)))) and (|??Q| /= 0 and (IsPermutation((?Q o <?min>), ??Q) and IsASmallest(??Q, ?min)))))
_____________________________
IsNondecreasing((?sorted o <?min>))

(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (|Q| <= Max_Length)) and (((IsPermutation((??Q o ?sorted), Q) and IsNondecreasing(?sorted)) and for all y:Entry, If IsSubstring(<y>, ??Q) then (IsNondecreasing((?sorted o <y>)))) and (|??Q| /= 0 and (IsPermutation((?Q o <?min>), ??Q) and IsASmallest(??Q, ?min)))))
_____________________________
for all y:Entry, If IsSubstring(<y>, ?Q) then (IsNondecreasing(((?sorted o <?min>) o <y>)))

(((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and (|Q| <= Max_Length)) and (((IsPermutation((??Q o ?sorted), Q) and IsNondecreasing(?sorted)) and for all y:Entry, If IsSubstring(<y>, ??Q) then (IsNondecreasing((?sorted o <y>)))) and (|??Q| /= 0 and (IsPermutation((?Q o <?min>), ??Q) and IsASmallest(??Q, ?min)))))
_____________________________
(|?Q| < |??Q|)




Free Variables: Max_Length:*Z, min_int:*Z, max_int:*Z, Q:*Str(*Entry), ?P_val:*N, min:*Entry, sorted:*Str(*Entry)



((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and ((|Q| <= Max_Length) and (((IsPermutation((?Q o ?sorted), Q) and IsNondecreasing(?sorted)) and for all y:Entry, If IsSubstring(<y>, ?Q) then (IsNondecreasing((?sorted o <y>)))) and |?Q| = 0)))
_____________________________
IsNondecerasing(?sorted)

((((min_int <= 0) and (0 < max_int)) and ((min_int <= 0) and (0 < max_int) and (Max_Length > 0))) and ((|Q| <= Max_Length) and (((IsPermutation((?Q o ?sorted), Q) and IsNondecreasing(?sorted)) and for all y:Entry, If IsSubstring(<y>, ?Q) then (IsNondecreasing((?sorted o <y>)))) and |?Q| = 0)))
_____________________________
IsPermutation(Q, ?sorted)