[YICES-HELP] unbounded loop
Jean-Francois Couchot
Jean-Francois.Couchot at lri.fr
Fri Feb 9 06:48:00 PST 2007
Hi.
I've some difficulties to understand why Yices does not discharge the
proof obligation joined in attachement in smtlib formalism.
More precisely, the command
$yices -smt -v 10 sstrat.smt
returns
Yices (version 1.0.2). Copyright 2005, 2006 SRI International.
GMP (version 4.1.4). Copyright Free Software Foundation, Inc.
Build date: Mon Nov 13 09:58:33 PST 2006
simplifying...
hash consing...
eliminating term ite...
searching...
ssiIssssiI.s...........s...........s...r.........s.......s
.......s........s.........s.......s......s.......s....r....s
......s...........s............s..........s.............s......s
............s........s......s........s.......s.....................
.........s........s.......s.............s..........s..............s.
Well, it seems that the case spliting rule of the SAT solver is widely
activated.
However, in the proof obligation, when I comment the two quantified axioms
;; Why axiom ite_true
:assumption
(forall (?t_5_200_144 c_type)
(forall (?x_75_145 c_unique)
(forall (?y_74_146 c_unique)
(= (smtlib__ite c_Boolean_true (c_sort ?t_5_200_144 ?x_75_145)
(c_sort ?t_5_200_144 ?y_74_146))
?x_75_145))))
;; Why axiom ite_false
:assumption
(forall (?t_6_201_147 c_type)
(forall (?x_77_148 c_unique)
(forall (?y_76_149 c_unique)
(= (smtlib__ite c_Boolean_false (c_sort ?t_6_201_147 ?x_77_148)
(c_sort ?t_6_201_147 ?y_76_149))
?y_76_149))))
the proof is discharged. It makes me think that the instantiation
process which diverges.
Where is the really origin ?
Thanks
--
Jean-Francois Couchot
Post Doctorant
INRIA Futurs - PROVAL
Parc club Orsay Université, Zac des Vignes
4, rue Jacques Monod, 91893 Orsay cedex
tel : (+33) (0)1 72 92 59 70 fax : (+33) (0)1 60 19 69 63
-------------- next part --------------
(benchmark gwhydbf892
:status unknown
:extrasorts (Unit)
:extrasorts (c_unique)
:extrasorts (c_ssorted)
:extrasorts (c_type)
:extrasorts (c_Boolean)
;;;; Why logic c_sort
:extrafuns ((c_sort c_type c_unique c_ssorted))
;;;; Why logic c_Boolean_true
:extrafuns ((c_Boolean_true c_Boolean))
;;;; Why logic c_Boolean_false
:extrafuns ((c_Boolean_false c_Boolean))
;; Why axiom either true_or_false_c_to_either true_or_false_c
:assumption
(forall (?b_22_110 c_Boolean)
(or (= c_Boolean_true ?b_22_110) (= c_Boolean_false ?b_22_110)))
;; Why axiom true_neq_false_c_to_true_neq_false_c
:assumption (not (= c_Boolean_true c_Boolean_false))
;;;; Why logic int2U
:extrafuns ((int2U Int c_unique))
;;;; Why logic ss2Int
:extrafuns ((ss2Int c_ssorted Int))
;;;; Why logic real2U
:extrafuns ((real2U Real c_unique))
;;;; Why logic ss2Real
:extrafuns ((ss2Real c_ssorted Real))
;;;; Why logic bool2U
:extrafuns ((bool2U c_Boolean c_unique))
;;;; Why logic ss2Bool
:extrafuns ((ss2Bool c_ssorted c_Boolean))
;;;; Why logic c_int
:extrafuns ((c_int c_type))
;;;; Why logic c_bool
:extrafuns ((c_bool c_type))
;;;; Why logic c_real
:extrafuns ((c_real c_type))
;;;; Why logic c_unit
:extrafuns ((c_unit c_type))
;;;; Why logic c_ref
:extrafuns ((c_ref c_unique c_unique))
;; Why axiom c__c_to_c__csort_is_injective
:assumption
(forall (?t_21_111 c_type)
(forall (?x_20_112 c_unique)
(forall (?y_19_113 c_unique)
(implies (= (c_sort ?t_21_111 ?x_20_112) (c_sort ?t_21_111 ?y_19_113))
(= ?x_20_112 ?y_19_113)))))
;; Why axiom eq__c_to_eq__css2Int_int2U
:assumption
(forall (?x_18_114 Int)
(= (ss2Int (c_sort c_int (int2U ?x_18_114))) ?x_18_114))
;; Why axiom int2U_c_to_int2U_c_is_injective
:assumption
(forall (?x_17_115 Int)
(forall (?y_16_116 Int)
(implies (= (int2U ?x_17_115) (int2U ?y_16_116)) (= ?x_17_115 ?y_16_116))))
;; Why axiom real2U_c_to_real2U_c_is_injective
:assumption
(forall (?x_15_117 Real)
(forall (?y_14_118 Real)
(implies (= (real2U ?x_15_117) (real2U ?y_14_118))
(= ?x_15_117 ?y_14_118))))
;; Why axiom bool2U_c_to_bool2U_c_is_injective
:assumption
(forall (?x_13_119 c_Boolean)
(forall (?y_12_120 c_Boolean)
(implies (= (bool2U ?x_13_119) (bool2U ?y_12_120))
(= ?x_13_119 ?y_12_120))))
;; Why axiom ss2Int_c_to_ss2Int_c_is_injective
:assumption
(forall (?x_11_121 c_ssorted)
(forall (?y_10_122 c_ssorted)
(implies (= (ss2Int ?x_11_121) (ss2Int ?y_10_122))
(= ?x_11_121 ?y_10_122))))
;; Why axiom ss2Real_c_to_ss2Real_c_is_injective
:assumption
(forall (?x_9_123 c_ssorted)
(forall (?y_8_124 c_ssorted)
(implies (= (ss2Real ?x_9_123) (ss2Real ?y_8_124)) (= ?x_9_123 ?y_8_124))))
;; Why axiom ss2Bool_c_to_ss2Bool_c_is_injective
:assumption
(forall (?x_7_125 c_ssorted)
(forall (?y_6_126 c_ssorted)
(implies (= (ss2Bool ?x_7_125) (ss2Bool ?y_6_126)) (= ?x_7_125 ?y_6_126))))
;; Why axiom eq__c_to_eq__css2Real_real2U
:assumption
(forall (?x_5_127 Real)
(= (ss2Real (c_sort c_real (real2U ?x_5_127))) ?x_5_127))
;; Why axiom eq__c_to_eq__css2Bool_bool2U
:assumption
(forall (?x_4_128 c_Boolean)
(= (ss2Bool (c_sort c_bool (bool2U ?x_4_128))) ?x_4_128))
;; Why axiom eq__c_to_eq__cint2U_ss2Int
:assumption
(forall (?x_3_129 c_unique)
(= (int2U (ss2Int (c_sort c_int ?x_3_129))) ?x_3_129))
;; Why axiom eq__c_to_eq__creal2U_ss2Real
:assumption
(forall (?x_2_130 c_unique)
(= (real2U (ss2Real (c_sort c_real ?x_2_130))) ?x_2_130))
;; Why axiom eq__c_to_eq__cbool2U_ss2Bool
:assumption
(forall (?x_1_131 c_unique)
(= (bool2U (ss2Bool (c_sort c_bool ?x_1_131))) ?x_1_131))
;;;; Why logic eq_int
:extrapreds ((eq_int Int Int))
;;;; Why logic neq_int
:extrapreds ((neq_int Int Int))
;;;; Why logic lt_int_bool
:extrafuns ((lt_int_bool Int Int c_Boolean))
;;;; Why logic le_int_bool
:extrafuns ((le_int_bool Int Int c_Boolean))
;;;; Why logic gt_int_bool
:extrafuns ((gt_int_bool Int Int c_Boolean))
;;;; Why logic ge_int_bool
:extrafuns ((ge_int_bool Int Int c_Boolean))
;;;; Why logic eq_int_bool
:extrafuns ((eq_int_bool Int Int c_Boolean))
;;;; Why logic neq_int_bool
:extrafuns ((neq_int_bool Int Int c_Boolean))
;; Why axiom lt_int_bool_axiom
:assumption
(forall (?x_40_132 Int)
(forall (?y_39_133 Int)
(iff (= (lt_int_bool ?x_40_132 ?y_39_133) c_Boolean_true)
(< ?x_40_132 ?y_39_133))))
;; Why axiom le_int_bool_axiom
:assumption
(forall (?x_42_134 Int)
(forall (?y_41_135 Int)
(iff (= (le_int_bool ?x_42_134 ?y_41_135) c_Boolean_true)
(<= ?x_42_134 ?y_41_135))))
;; Why axiom gt_int_bool_axiom
:assumption
(forall (?x_44_136 Int)
(forall (?y_43_137 Int)
(iff (= (gt_int_bool ?x_44_136 ?y_43_137) c_Boolean_true)
(> ?x_44_136 ?y_43_137))))
;; Why axiom ge_int_bool_axiom
:assumption
(forall (?x_46_138 Int)
(forall (?y_45_139 Int)
(iff (= (ge_int_bool ?x_46_138 ?y_45_139) c_Boolean_true)
(>= ?x_46_138 ?y_45_139))))
;; Why axiom eq_int_bool_axiom
:assumption
(forall (?x_48_140 Int)
(forall (?y_47_141 Int)
(iff (= (eq_int_bool ?x_48_140 ?y_47_141) c_Boolean_true)
(= ?x_48_140 ?y_47_141))))
;; Why axiom neq_int_bool_axiom
:assumption
(forall (?x_50_142 Int)
(forall (?y_49_143 Int)
(iff (= (neq_int_bool ?x_50_142 ?y_49_143) c_Boolean_true)
(not (= ?x_50_142 ?y_49_143)))))
;;;; Why logic add_real
:extrafuns ((add_real Real Real Real))
;;;; Why logic sub_real
:extrafuns ((sub_real Real Real Real))
;;;; Why logic mul_real
:extrafuns ((mul_real Real Real Real))
;;;; Why logic div_real
:extrafuns ((div_real Real Real Real))
;;;; Why logic pow_real
:extrafuns ((pow_real Real Real Real))
;;;; Why logic neg_real
:extrafuns ((neg_real Real Real))
;;;; Why logic abs_real
:extrafuns ((abs_real Real Real))
;;;; Why logic sqrt_real
:extrafuns ((sqrt_real Real Real))
;;;; Why logic real_of_int
:extrafuns ((real_of_int Int Real))
;;;; Why logic int_of_real
:extrafuns ((int_of_real Real Int))
;;;; Why logic lt_real
:extrapreds ((lt_real Real Real))
;;;; Why logic le_real
:extrapreds ((le_real Real Real))
;;;; Why logic gt_real
:extrapreds ((gt_real Real Real))
;;;; Why logic ge_real
:extrapreds ((ge_real Real Real))
;;;; Why logic eq_real
:extrapreds ((eq_real Real Real))
;;;; Why logic neq_real
:extrapreds ((neq_real Real Real))
;;;; Why logic eq_bool
:extrapreds ((eq_bool c_Boolean c_Boolean))
;;;; Why logic neq_bool
:extrapreds ((neq_bool c_Boolean c_Boolean))
;;;; Why logic eq_unit
:extrapreds ((eq_unit c_ssorted c_ssorted))
;;;; Why logic neq_unit
:extrapreds ((neq_unit c_ssorted c_ssorted))
;;;;;;;;;;;;;;;; comment all lines from here
;;;; Why logic ite
:extrafuns ((smtlib__ite c_Boolean c_ssorted c_ssorted c_unique))
;; Why axiom ite_true
:assumption
(forall (?t_5_200_144 c_type)
(forall (?x_75_145 c_unique)
(forall (?y_74_146 c_unique)
(= (smtlib__ite c_Boolean_true (c_sort ?t_5_200_144 ?x_75_145)
(c_sort ?t_5_200_144 ?y_74_146))
?x_75_145))))
;; Why axiom ite_false
:assumption
(forall (?t_6_201_147 c_type)
(forall (?x_77_148 c_unique)
(forall (?y_76_149 c_unique)
(= (smtlib__ite c_Boolean_false (c_sort ?t_6_201_147 ?x_77_148)
(c_sort ?t_6_201_147 ?y_76_149))
?y_76_149))))
;;;;;;;;;;;;;;;;;;;;;;; until here
;;;; Why logic type_farray
:extrafuns ((type_farray c_type c_type))
;;;; Why logic array_length
:extrafuns ((array_length c_ssorted Int))
;;;; Why logic access
:extrafuns ((access c_ssorted Int c_unique))
;;;; Why logic update
:extrafuns ((update c_ssorted Int c_ssorted c_unique))
;; Why axiom access_update
:assumption
(forall (?t_7_202_150 c_type)
(forall (?t_86_151 c_unique)
(forall (?i_85_152 Int)
(forall (?v_84_153 c_unique)
(= (access
(c_sort (type_farray ?t_7_202_150)
(update (c_sort (type_farray ?t_7_202_150) ?t_86_151) ?i_85_152
(c_sort ?t_7_202_150 ?v_84_153))) ?i_85_152)
?v_84_153)))))
;; Why axiom access_update_neq
:assumption
(forall (?t_8_203_154 c_type)
(forall (?t_90_155 c_unique)
(forall (?i_89_156 Int)
(forall (?j_88_157 Int)
(forall (?v_87_158 c_unique)
(implies (not (= ?i_89_156 ?j_88_157))
(= (access
(c_sort (type_farray ?t_8_203_154)
(update (c_sort (type_farray ?t_8_203_154) ?t_90_155) ?i_89_156
(c_sort ?t_8_203_154 ?v_87_158))) ?j_88_157)
(access (c_sort (type_farray ?t_8_203_154) ?t_90_155) ?j_88_157))))))))
;;;; Why logic sorted_array
:extrapreds ((sorted_array c_ssorted Int Int))
;; Why axiom def_sorted_array
:assumption
(forall (?t_206_159 c_unique)
(forall (?i_205_160 Int)
(forall (?j_204_161 Int)
(iff
(sorted_array (c_sort (type_farray c_int) ?t_206_159) ?i_205_160
?j_204_161)
(forall (?k_96_162 Int)
(implies (and (<= ?i_205_160 ?k_96_162) (< ?k_96_162 ?j_204_161))
(<= (ss2Int
(c_sort c_int
(access (c_sort (type_farray c_int) ?t_206_159) ?k_96_162)))
(ss2Int
(c_sort c_int
(access (c_sort (type_farray c_int) ?t_206_159) (+ ?k_96_162 1)))))))))))
;;;; Why logic array_le
:extrapreds ((array_le c_ssorted Int Int Int))
;;;; Why logic array_ge
:extrapreds ((array_ge c_ssorted Int Int Int))
;;;; Why logic exchange
:extrapreds ((exchange c_ssorted c_ssorted Int Int))
;; Why axiom def_exchange
:assumption
(forall (?t1_210_163 c_unique)
(forall (?t2_209_164 c_unique)
(forall (?i_208_165 Int)
(forall (?j_207_166 Int)
(iff
(exchange (c_sort (type_farray c_int) ?t1_210_163)
(c_sort (type_farray c_int) ?t2_209_164) ?i_208_165 ?j_207_166)
(and
(= (array_length (c_sort (type_farray c_int) ?t1_210_163))
(array_length (c_sort (type_farray c_int) ?t2_209_164)))
(and
(= (access (c_sort (type_farray c_int) ?t1_210_163) ?i_208_165)
(access (c_sort (type_farray c_int) ?t2_209_164) ?j_207_166))
(and
(= (access (c_sort (type_farray c_int) ?t2_209_164) ?i_208_165)
(access (c_sort (type_farray c_int) ?t1_210_163) ?j_207_166))
(forall (?k_97_167 Int)
(implies
(and (not (= ?k_97_167 ?i_208_165)) (not (= ?k_97_167 ?j_207_166)))
(= (access (c_sort (type_farray c_int) ?t1_210_163) ?k_97_167)
(access (c_sort (type_farray c_int) ?t2_209_164) ?k_97_167))))))))))))
;;;; Why logic permut
:extrapreds ((permut c_ssorted c_ssorted))
;; Why axiom permut_refl
:assumption
(forall (?t_98_168 c_unique)
(permut (c_sort (type_farray c_int) ?t_98_168)
(c_sort (type_farray c_int) ?t_98_168)))
;; Why axiom permut_sym
:assumption
(forall (?t1_100_169 c_unique)
(forall (?t2_99_170 c_unique)
(implies
(permut (c_sort (type_farray c_int) ?t1_100_169)
(c_sort (type_farray c_int) ?t2_99_170))
(permut (c_sort (type_farray c_int) ?t2_99_170)
(c_sort (type_farray c_int) ?t1_100_169)))))
;; Why axiom permut_trans
:assumption
(forall (?t1_103_171 c_unique)
(forall (?t2_102_172 c_unique)
(forall (?t3_101_173 c_unique)
(implies
(and
(permut (c_sort (type_farray c_int) ?t1_103_171)
(c_sort (type_farray c_int) ?t2_102_172))
(permut (c_sort (type_farray c_int) ?t2_102_172)
(c_sort (type_farray c_int) ?t3_101_173)))
(permut (c_sort (type_farray c_int) ?t1_103_171)
(c_sort (type_farray c_int) ?t3_101_173))))))
;; Why axiom permut_exchange
:assumption
(forall (?t_106_174 c_unique)
(forall (?i_105_175 Int)
(forall (?j_104_176 Int)
(permut (c_sort (type_farray c_int) ?t_106_174)
(c_sort (type_farray c_int)
(update
(c_sort (type_farray c_int)
(update (c_sort (type_farray c_int) ?t_106_174) ?i_105_175
(c_sort c_int (access (c_sort (type_farray c_int) ?t_106_174) ?j_104_176))))
?j_104_176
(c_sort c_int (access (c_sort (type_farray c_int) ?t_106_174) ?i_105_175))))))))
;;;; Why logic sub_permut
:extrapreds ((sub_permut Int Int c_ssorted c_ssorted))
;; Why axiom sub_permut_refl
:assumption
(forall (?t_109_177 c_unique)
(forall (?g_108_178 Int)
(forall (?d_107_179 Int)
(sub_permut ?g_108_178 ?d_107_179 (c_sort (type_farray c_int) ?t_109_177)
(c_sort (type_farray c_int) ?t_109_177)))))
;; Why axiom sub_permut_sym
:assumption
(forall (?t1_113_180 c_unique)
(forall (?t2_112_181 c_unique)
(forall (?g_111_182 Int)
(forall (?d_110_183 Int)
(implies
(sub_permut ?g_111_182 ?d_110_183 (c_sort (type_farray c_int) ?t1_113_180)
(c_sort (type_farray c_int) ?t2_112_181))
(sub_permut ?g_111_182 ?d_110_183 (c_sort (type_farray c_int) ?t2_112_181)
(c_sort (type_farray c_int) ?t1_113_180)))))))
;; Why axiom sub_permut_trans
:assumption
(forall (?t1_118_184 c_unique)
(forall (?t2_117_185 c_unique)
(forall (?t3_116_186 c_unique)
(forall (?g_115_187 Int)
(forall (?d_114_188 Int)
(implies
(sub_permut ?g_115_187 ?d_114_188 (c_sort (type_farray c_int) ?t1_118_184)
(c_sort (type_farray c_int) ?t2_117_185))
(implies
(sub_permut ?g_115_187 ?d_114_188 (c_sort (type_farray c_int) ?t2_117_185)
(c_sort (type_farray c_int) ?t3_116_186))
(sub_permut ?g_115_187 ?d_114_188 (c_sort (type_farray c_int) ?t1_118_184)
(c_sort (type_farray c_int) ?t3_116_186)))))))))
;; Why axiom sub_permut_exchange_1
:assumption
(forall (?t_123_189 c_unique)
(forall (?g_122_190 Int)
(forall (?d_121_191 Int)
(forall (?i_120_192 Int)
(forall (?j_119_193 Int)
(implies
(and (<= ?g_122_190 ?i_120_192)
(and (<= ?i_120_192 ?d_121_191)
(and (<= ?g_122_190 ?j_119_193) (<= ?j_119_193 ?d_121_191))))
(sub_permut ?g_122_190 ?d_121_191 (c_sort (type_farray c_int) ?t_123_189)
(c_sort (type_farray c_int)
(update
(c_sort (type_farray c_int)
(update (c_sort (type_farray c_int) ?t_123_189) ?i_120_192
(c_sort c_int (access (c_sort (type_farray c_int) ?t_123_189) ?j_119_193))))
?j_119_193
(c_sort c_int (access (c_sort (type_farray c_int) ?t_123_189) ?i_120_192)))))))))))
;; Why axiom sub_permut_exchange_2
:assumption
(forall (?t1_129_194 c_unique)
(forall (?t2_128_195 c_unique)
(forall (?g_127_196 Int)
(forall (?d_126_197 Int)
(forall (?i_125_198 Int)
(forall (?j_124_199 Int)
(implies
(and (<= ?g_127_196 ?i_125_198)
(and (<= ?i_125_198 ?d_126_197)
(and (<= ?g_127_196 ?j_124_199)
(and (<= ?j_124_199 ?d_126_197)
(exchange (c_sort (type_farray c_int) ?t1_129_194)
(c_sort (type_farray c_int) ?t2_128_195) ?i_125_198 ?j_124_199)))))
(sub_permut ?g_127_196 ?d_126_197 (c_sort (type_farray c_int) ?t1_129_194)
(c_sort (type_farray c_int) ?t2_128_195)))))))))
;; Why axiom sub_permut_permut
:assumption
(forall (?t1_133_200 c_unique)
(forall (?t2_132_201 c_unique)
(forall (?g_131_202 Int)
(forall (?d_130_203 Int)
(implies
(sub_permut ?g_131_202 ?d_130_203 (c_sort (type_farray c_int) ?t1_133_200)
(c_sort (type_farray c_int) ?t2_132_201))
(permut (c_sort (type_farray c_int) ?t1_133_200)
(c_sort (type_farray c_int) ?t2_132_201)))))))
;; Why axiom array_length_update
:assumption
(forall (?t_136_204 c_unique)
(forall (?i_135_205 Int)
(forall (?v_134_206 Int)
(= (array_length
(c_sort (type_farray c_int)
(update (c_sort (type_farray c_int) ?t_136_204) ?i_135_205
(c_sort c_int (int2U ?v_134_206)))))
(array_length (c_sort (type_farray c_int) ?t_136_204))))))
;; Why axiom sub_permut_array_length
:assumption
(forall (?t1_140_207 c_unique)
(forall (?t2_139_208 c_unique)
(forall (?g_138_209 Int)
(forall (?d_137_210 Int)
(implies
(sub_permut ?g_138_209 ?d_137_210 (c_sort (type_farray c_int) ?t1_140_207)
(c_sort (type_farray c_int) ?t2_139_208))
(= (array_length (c_sort (type_farray c_int) ?t1_140_207))
(array_length (c_sort (type_farray c_int) ?t2_139_208))))))))
;; Why axiom permut_array_length
:assumption
(forall (?t1_142_211 c_unique)
(forall (?t2_141_212 c_unique)
(implies
(permut (c_sort (type_farray c_int) ?t1_142_211)
(c_sort (type_farray c_int) ?t2_141_212))
(= (array_length (c_sort (type_farray c_int) ?t1_142_211))
(array_length (c_sort (type_farray c_int) ?t2_141_212))))))
:formula
;; Why obligation from file "", line 0, characters 0-0:
(not
(forall (?l Int)
(forall (?r Int)
(forall (?t c_unique)
(implies
(and (<= 0 ?l) (< ?r (array_length (c_sort (type_farray c_int) ?t))))
(implies (< ?l ?r)
(implies
(and (<= 0 ?l) (< ?l (array_length (c_sort (type_farray c_int) ?t))))
(forall (?result c_unique)
(implies (= ?result (access (c_sort (type_farray c_int) ?t) ?l))
(implies
(and
(forall (?j_167_213 Int)
(implies (and (< ?l ?j_167_213) (<= ?j_167_213 ?l))
(< (ss2Int
(c_sort c_int (access (c_sort (type_farray c_int) ?t) ?j_167_213)))
(ss2Int (c_sort c_int ?result)))))
(and
(forall (?j_166_214 Int)
(implies (and (< ?l ?j_166_214) (< ?j_166_214 (+ ?l 1)))
(>= (ss2Int
(c_sort c_int (access (c_sort (type_farray c_int) ?t) ?j_166_214)))
(ss2Int (c_sort c_int ?result)))))
(and
(sub_permut ?l ?r (c_sort (type_farray c_int) ?t)
(c_sort (type_farray c_int) ?t))
(and (= (access (c_sort (type_farray c_int) ?t) ?l) ?result)
(and (and (<= ?l ?l) (< ?l (+ ?l 1))) (<= (+ ?l 1) (+ ?r 1)))))))
(forall (?i Int)
(forall (?m Int)
(forall (?t0 c_unique)
(implies
(and
(forall (?j_167_215 Int)
(implies (and (< ?l ?j_167_215) (<= ?j_167_215 ?m))
(< (ss2Int
(c_sort c_int (access (c_sort (type_farray c_int) ?t0) ?j_167_215)))
(ss2Int (c_sort c_int ?result)))))
(and
(forall (?j_166_216 Int)
(implies (and (< ?m ?j_166_216) (< ?j_166_216 ?i))
(>= (ss2Int
(c_sort c_int (access (c_sort (type_farray c_int) ?t0) ?j_166_216)))
(ss2Int (c_sort c_int ?result)))))
(and
(sub_permut ?l ?r (c_sort (type_farray c_int) ?t0)
(c_sort (type_farray c_int) ?t))
(and (= (access (c_sort (type_farray c_int) ?t0) ?l) ?result)
(and (and (<= ?l ?m) (< ?m ?i)) (<= ?i (+ ?r 1)))))))
(implies (<= ?i ?r)
(implies
(and (<= 0 ?i) (< ?i (array_length (c_sort (type_farray c_int) ?t0))))
(forall (?result0 c_unique)
(implies (= ?result0 (access (c_sort (type_farray c_int) ?t0) ?i))
(implies
(< (ss2Int (c_sort c_int ?result0)) (ss2Int (c_sort c_int ?result)))
(forall (?m0 Int)
(implies (= ?m0 (+ ?m 1))
(implies
(and (and (<= 0 ?i) (< ?i (array_length (c_sort (type_farray c_int) ?t0))))
(and (<= 0 ?m0) (< ?m0 (array_length (c_sort (type_farray c_int) ?t0)))))
(forall (?t1 c_unique)
(implies
(exchange (c_sort (type_farray c_int) ?t1) (c_sort (type_farray c_int) ?t0)
?i ?m0)
(forall (?i0 Int)
(implies (= ?i0 (+ ?i 1))
(and
(and
(forall (?j_167_217 Int)
(implies (and (< ?l ?j_167_217) (< ?j_167_217 ?m0))
(< (ss2Int
(c_sort c_int (access (c_sort (type_farray c_int) ?t1) ?j_167_217)))
(ss2Int (c_sort c_int ?result)))))
))))))))))))))))))))))))))))
)
More information about the YICES-HELP
mailing list