ada/SPARKlib
0
0
Fork 0
mirror of https://github.com/AdaCore/SPARKlib.git synced 2026-02-12 13:11:36 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
SPARKlib/proof/Coq
History
Yannick Moy 09e546bdeb Fix Coq scripts for proof of modular arithmetic lemmas 
Following a change in Why3, there is a renaming of generated axioms.
Update session files.
2024-02-01 11:59:36 +01:00
..
common
Fix Coq scripts for proof of modular arithmetic lemmas
2024-02-01 11:59:36 +01:00
Ada___ada___spark__lemmas__float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_protect__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_scale__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_protect__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_scale__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__tests__array_lemmas__test_ufloat__lemma_transitive_order__pragargs__forall.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00
Ada___ada___spark__tests__array_lemmas__test_uint__lemma_transitive_order__pragargs__forall.ctx
V913-014, W224-046 Copy SPARKlib source files
2023-04-07 11:29:15 +02:00