//
// Generated by the Resolve Verifier, November 2007 version
// from file:  Sort_Realiz.rb
// on:         Mon May 19 21:25:30 EDT 2008
//

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



(((((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 (Max_Length > 0)) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q))
_____________________________
IsPreceding(<??min>, empty_string)

((((((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(((?NewQ o ??Q) o <?min>), Q) and IsPreceding(<?min>, ?NewQ)) and (|??Q| /= 0 and (??Q = (<?E> o ?Q) and LEQV(?E, ?min)))))
_____________________________
(|?NewQ| < Max_Length)

((((((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(((?NewQ o ??Q) o <?min>), Q) and IsPreceding(<?min>, ?NewQ)) and (|??Q| /= 0 and (??Q = (<?E> o ?Q) and LEQV(?E, ?min)))))
_____________________________
IsPermutation((((?NewQ o <?min>) o ?Q) o <?E>), Q)

((((((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(((?NewQ o ??Q) o <?min>), Q) and IsPreceding(<?min>, ?NewQ)) and (|??Q| /= 0 and (??Q = (<?E> o ?Q) and LEQV(?E, ?min)))))
_____________________________
IsPreceding(<?E>, (?NewQ o <?min>))

((((((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(((?NewQ o ??Q) o <?min>), Q) and IsPreceding(<?min>, ?NewQ)) and (|??Q| /= 0 and (??Q = (<?E> o ?Q) and LEQV(?E, ?min)))))
_____________________________
(|?Q| < |??Q|)




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



(((((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 (Max_Length > 0)) and (Entry.is_initial(min) and ((|Q| <= Max_Length) and |Q| /= 0))) and Q = (<??min> o ???Q))
_____________________________
IsPreceding(<??min>, empty_string)

((((((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(((?NewQ o ??Q) o <?min>), Q) and IsPreceding(<?min>, ?NewQ)) and (|??Q| /= 0 and (??Q = (<?E> o ?Q) and not(LEQV(?E, ?min))))))
_____________________________
(|?NewQ| < Max_Length)

((((((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(((?NewQ o ??Q) o <?min>), Q) and IsPreceding(<?min>, ?NewQ)) and (|??Q| /= 0 and (??Q = (<?E> o ?Q) and not(LEQV(?E, ?min))))))
_____________________________
IsPermutation((((?NewQ o <?E>) o ?Q) o <?min>), Q)

((((((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(((?NewQ o ??Q) o <?min>), Q) and IsPreceding(<?min>, ?NewQ)) and (|??Q| /= 0 and (??Q = (<?E> o ?Q) and not(LEQV(?E, ?min))))))
_____________________________
IsPreceding(<?min>, (?NewQ o <?E>))

((((((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(((?NewQ o ??Q) o <?min>), Q) and IsPreceding(<?min>, ?NewQ)) and (|??Q| /= 0 and (??Q = (<?E> o ?Q) and not(LEQV(?E, ?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), E:*Entry, NewQ:*Str(*Entry)



(((((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(((?NewQ o ?Q) o <?min>), Q) and IsPreceding(<?min>, ?NewQ)) and |?Q| = 0)))
_____________________________
IsPermutation((?NewQ o <?min>), Q)




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 (Max_Length > 0)) and (|Q| <= Max_Length))
_____________________________
IsPermutation((Q o empty_string), Q)

((((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 (Max_Length > 0)) and (|Q| <= Max_Length))
_____________________________
IsPreceding(empty_string, Q)

(((((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 IsPreceding(?sorted, ??Q)) and (|??Q| /= 0 and (IsPermutation((?Q o <?min>), ??Q) and IsPreceding(<?min>, ?Q)))))
_____________________________
(|?sorted| < Max_Length)

(((((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 IsPreceding(?sorted, ??Q)) and (|??Q| /= 0 and (IsPermutation((?Q o <?min>), ??Q) and IsPreceding(<?min>, ?Q)))))
_____________________________
IsPermutation((?Q o (?sorted o <?min>)), Q)

(((((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 IsPreceding(?sorted, ??Q)) and (|??Q| /= 0 and (IsPermutation((?Q o <?min>), ??Q) and IsPreceding(<?min>, ?Q)))))
_____________________________
IsNonDecreasing((?sorted o <?min>))

(((((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 IsPreceding(?sorted, ??Q)) and (|??Q| /= 0 and (IsPermutation((?Q o <?min>), ??Q) and IsPreceding(<?min>, ?Q)))))
_____________________________
IsPreceding((?sorted o <?min>), ?Q)

(((((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 IsPreceding(?sorted, ??Q)) and (|??Q| /= 0 and (IsPermutation((?Q o <?min>), ??Q) and IsPreceding(<?min>, ?Q)))))
_____________________________
(|?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 (Max_Length > 0)) and ((|Q| <= Max_Length) and (((IsPermutation((?Q o ?sorted), Q) and IsNonDecreasing(?sorted)) and IsPreceding(?sorted, ?Q)) and |?Q| = 0)))
_____________________________
IsPermutation(Q, ?sorted)