-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathcst_man.glob
4410 lines (4410 loc) · 246 KB
/
cst_man.glob
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
DIGEST a61622619ca1fc4fa79e4f62c3afc8b7
FDeepSpec.minic.tests.contracts.amm.cst_man
R181:185 Coq.Reals.Reals <> <> lib
R203:205 Coq.micromega.Lra <> <> lib
R223:225 Coq.micromega.Lia <> <> lib
R243:257 Interval.Tactic <> <> lib
R275:294 Interval.Real.Taylor <> <> lib
R312:334 Interval.Poly.Datatypes <> <> lib
R352:376 Interval.Poly.Taylor_poly <> <> lib
R394:425 Interval.Poly.Taylor_model_sharp <> <> lib
R443:474 Interval.Interval.Interval_compl <> <> lib
R492:515 DeepSpec.lib.Monad.Monad <> <> lib
R533:544 amm.LayerAMM <> <> lib
R562:567 Coq.PArith.BinPos <> <> lib
R585:600 DeepSpec.Runtime <> <> lib
R618:633 amm.EdsgerIdents <> <> lib
R651:663 amm.DataTypes <> <> lib
R681:695 amm.DataTypeOps <> <> lib
R713:730 amm.DataTypeProofs <> <> lib
R748:771 DeepSpec.lib.Monad.Monad <> <> lib
R789:817 DeepSpec.lib.Monad.MonadState <> <> lib
R835:863 DeepSpec.lib.Monad.StateMonad <> <> lib
R881:910 DeepSpec.lib.Monad.OptionMonad <> <> lib
R928:955 DeepSpec.lib.Monad.MonadZero <> <> lib
R973:999 DeepSpec.core.SynthesisStmt <> <> lib
R1017:1043 DeepSpec.core.SynthesisFunc <> <> lib
R1061:1080 DeepSpec.backend.MachineModel <> <> lib
R1163:1177 amm.LayerAMMLIB <> <> lib
R1211:1220 Coquelicot.Coquelicot <> <> lib
R1238:1264 Interval.Missing.Coquelicot <> <> lib
R1329:1338 Interval.Poly.Taylor_poly TaylorPoly <> modtype
R1340:1344 Interval.Poly.Datatypes FullR <> modtype
R1346:1349 Interval.Poly.Datatypes PolR <> modtype
mod 1323:1324 <> TR
R1368:1374 Interval.Poly.Datatypes SeqPoly <> modtype
R1376:1380 Interval.Poly.Datatypes FullR <> modtype
mod 1359:1363 <> SPoly
sec 1391:1395 <> C_man
R1446:1459 DeepSpec.core.MemoryModel <> MemoryModelOps class
R1461:1463 DeepSpec.backend.AbstractData <> mem def
def 1479:1483 <> state
R1488:1512 amm.DataTypeOps <> global_abstract_data_type rec
def 1527:1536 <> init_state
R1541:1565 amm.DataTypeOps <> init_global_abstract_data def
def 1580:1582 <> wei
R1587:1587 Coq.Numbers.BinNums <> Z ind
def 1602:1605 <> addr
R1610:1615 DeepSpec.cclib.Integers <> int256 syndef
def 1630:1640 <> blocknumber
R1645:1650 DeepSpec.cclib.Integers <> int256 syndef
R1716:1727 DeepSpec.Runtime <> GlobalAbData class
R1755:1780 amm.DataTypeOps <> global_low_level_invariant def
R1729:1753 amm.DataTypeOps <> init_global_abstract_data def
R1820:1841 DeepSpec.lib.Monad.RunStateTInv <> <> lib
R1859:1870 DeepSpec.lib.ArithInv <> <> lib
def 1885:1896 <> reserve_beta
R1903:1907 DeepSpec.minic.tests.contracts.amm.cst_man <> state def
R1912:1912 Coq.Numbers.BinNums <> Z ind
R1918:1959 amm.DataTypeOps <> AutomatedMarketMaker__reserve0 proj
R1961:1961 DeepSpec.minic.tests.contracts.amm.cst_man <> s var
def 1977:1989 <> reserve_alpha
R1996:2000 DeepSpec.minic.tests.contracts.amm.cst_man <> state def
R2005:2005 Coq.Numbers.BinNums <> Z ind
R2011:2052 amm.DataTypeOps <> AutomatedMarketMaker__reserve1 proj
R2054:2054 DeepSpec.minic.tests.contracts.amm.cst_man <> s var
def 2070:2081 <> get_balance0
R2087:2091 DeepSpec.minic.tests.contracts.amm.cst_man <> state def
R2098:2101 DeepSpec.minic.tests.contracts.amm.cst_man <> addr def
R2112:2133 DeepSpec.cclib.Maps Int256Tree get_default def
R2150:2174 amm.DataTypeOps <> FixedSupplyToken_balances proj
R2176:2176 DeepSpec.minic.tests.contracts.amm.cst_man <> s var
R2147:2147 DeepSpec.minic.tests.contracts.amm.cst_man <> a var
R2235:2238 DeepSpec.minic.tests.contracts.amm.cst_man <> addr def
R2263:2268 DeepSpec.cclib.Integers <> int256 syndef
R2294:2299 DeepSpec.cclib.Integers <> int256 syndef
R2322:2327 DeepSpec.cclib.Integers <> int256 syndef
R2357:2360 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2361:2366 DeepSpec.cclib.Integers <> int256 syndef
R2351:2356 DeepSpec.cclib.Integers <> int256 syndef
R2398:2401 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2402:2407 DeepSpec.cclib.Integers <> int256 syndef
R2392:2397 DeepSpec.cclib.Integers <> int256 syndef
R2443:2447 DeepSpec.minic.tests.contracts.amm.cst_man <> state def
def 2464:2479 <> make_machine_env
R2490:2493 DeepSpec.minic.tests.contracts.amm.cst_man <> addr def
R2528:2538 DeepSpec.backend.MachineModel <> machine_env rec
R2540:2544 DeepSpec.minic.tests.contracts.amm.cst_man <> state def
R2556:3119 DeepSpec.backend.MachineModel <> mkmachine constr
R3100:3118 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.prev_contract_state var
R3067:3071 Coq.Init.Logic <> False ind
R3003:3003 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3014:3015 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3017:3017 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3004:3013 DeepSpec.cclib.Integers Int256 one def
R3016:3016 DeepSpec.minic.tests.contracts.amm.cst_man <> d var
R2929:2937 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.blockhash var
R2894:2900 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.balance var
R2857:2867 DeepSpec.cclib.Integers Int256 zero def
R2816:2826 DeepSpec.cclib.Integers Int256 zero def
R2784:2789 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.number var
R2750:2758 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.timestamp var
R2713:2720 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.coinbase var
R2671:2681 DeepSpec.cclib.Integers Int256 repr def
R2637:2642 DeepSpec.minic.tests.contracts.amm.cst_man <> caller var
R2606:2611 DeepSpec.minic.tests.contracts.amm.cst_man <> caller var
R2570:2580 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.amm_address var
var 3167:3167 C_man s
var 3169:3170 C_man s'
R3173:3177 DeepSpec.minic.tests.contracts.amm.cst_man <> state def
var 3192:3192 C_man a
var 3194:3196 C_man toA
R3200:3203 DeepSpec.minic.tests.contracts.amm.cst_man <> addr def
var 3217:3217 C_man r
R3221:3223 DeepSpec.core.HyperTypeInst <> Z32 syndef
def 3239:3248 <> delta_beta
R3252:3252 Coq.Numbers.BinNums <> Z ind
R3257:3257 Coq.ZArith.BinInt <> ::Z_scope:x_'-'_x not
R3274:3278 Coq.ZArith.BinInt <> ::Z_scope:x_'-'_x not
R3293:3293 Coq.ZArith.BinInt <> ::Z_scope:x_'-'_x not
R3258:3269 DeepSpec.minic.tests.contracts.amm.cst_man <> get_balance0 def
R3273:3273 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.a var
R3271:3271 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.s var
R3279:3290 DeepSpec.minic.tests.contracts.amm.cst_man <> reserve_beta def
R3292:3292 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.s var
var 3307:3313 C_man del_alp
R3392:3394 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3317:3325 DeepSpec.lib.Monad.StateMonad <> runStateT proj
R3391:3391 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.s var
R3328:3363 amm.LayerAMM <> AutomatedMarketMaker_simpleSwap0_opt def
R3370:3385 DeepSpec.minic.tests.contracts.amm.cst_man <> make_machine_env def
R3387:3387 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.a var
R3365:3367 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.toA var
R3395:3398 Coq.Init.Datatypes <> Some constr
R3400:3400 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3402:3404 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3407:3407 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3401:3401 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.r var
R3405:3406 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.s' var
var 3421:3440 C_man non_neg_reserve_beta
R3464:3467 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R3444:3446 Coq.Reals.Rdefinitions <> IZR def
R3449:3460 DeepSpec.minic.tests.contracts.amm.cst_man <> reserve_beta def
R3462:3462 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.s var
def 3483:3493 <> delta_alpha
R3497:3497 Coq.Numbers.BinNums <> Z ind
R3502:3502 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.r var
def 3516:3527 <> market_price
R3531:3531 Coq.Reals.Rdefinitions <> R defax
R3536:3536 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3553:3555 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3573:3573 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3537:3539 Coq.Reals.Rdefinitions <> IZR def
R3542:3551 DeepSpec.minic.tests.contracts.amm.cst_man <> delta_beta def
R3556:3558 Coq.Reals.Rdefinitions <> IZR def
R3561:3571 DeepSpec.minic.tests.contracts.amm.cst_man <> delta_alpha def
def 3587:3589 <> eps
R3593:3593 Coq.Reals.Rdefinitions <> R defax
R3598:3598 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R3690:3694 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R3698:3698 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R3634:3636 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3689:3689 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3599:3601 Coq.Reals.Rdefinitions <> IZR def
R3604:3604 Coq.ZArith.BinInt <> ::Z_scope:x_'+'_x not
R3619:3622 Coq.ZArith.BinInt <> ::Z_scope:x_'+'_x not
R3605:3616 DeepSpec.minic.tests.contracts.amm.cst_man <> reserve_beta def
R3618:3618 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.s var
R3623:3632 DeepSpec.minic.tests.contracts.amm.cst_man <> delta_beta def
R3674:3676 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R3637:3639 Coq.Reals.Rdefinitions <> IZR def
R3642:3642 Coq.ZArith.BinInt <> ::Z_scope:x_'-'_x not
R3658:3661 Coq.ZArith.BinInt <> ::Z_scope:x_'-'_x not
R3643:3655 DeepSpec.minic.tests.contracts.amm.cst_man <> reserve_alpha def
R3657:3657 DeepSpec.minic.tests.contracts.amm.cst_man <> C_man.s var
R3662:3672 DeepSpec.minic.tests.contracts.amm.cst_man <> delta_alpha def
R3677:3688 DeepSpec.minic.tests.contracts.amm.cst_man <> market_price def
def 3713:3713 <> f
R3720:3720 Coq.Reals.Rdefinitions <> R defax
R3727:3730 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R3736:3736 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R3726:3726 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R3732:3734 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3735:3735 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
def 3751:3755 <> kappa
R3762:3762 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
def 3823:3827 <> T_f_1
R3834:3836 Coq.Init.Datatypes <> nat ind
R3849:3849 DeepSpec.minic.tests.contracts.amm.cst_man <> n var
R3887:3890 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R3905:3905 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R3878:3881 Coq.Reals.R_sqrt <> sqrt def
R3884:3884 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R3885:3885 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R3892:3892 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3893:3896 Coq.Reals.R_sqrt <> sqrt def
R3900:3902 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R3903:3903 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R3946:3949 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R3983:3983 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R3931:3932 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3945:3945 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3934:3935 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R3936:3939 Coq.Reals.R_sqrt <> sqrt def
R3942:3942 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R3943:3943 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R3951:3953 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3982:3982 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R3965:3968 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R3981:3981 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R3955:3958 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R3964:3964 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R3960:3962 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R3963:3963 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R3969:3972 Coq.Reals.R_sqrt <> sqrt def
R3976:3978 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R3979:3979 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R4008:4008 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4014:4017 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4046:4046 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4010:4012 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4013:4013 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R4033:4035 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4019:4022 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4032:4032 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4023:4023 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R4029:4030 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R4025:4027 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4028:4028 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R4036:4039 Coq.Reals.R_sqrt <> sqrt def
R4042:4043 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4044:4044 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
prf 4084:4092 <> lower_bnd
R4122:4125 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4174:4177 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R4126:4126 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4134:4138 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4173:4173 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4128:4130 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4131:4133 DeepSpec.minic.tests.contracts.amm.cst_man <> eta var
R4156:4158 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4140:4143 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4155:4155 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4144:4144 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R4152:4153 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R4146:4148 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4149:4151 DeepSpec.minic.tests.contracts.amm.cst_man <> eta var
R4159:4162 Coq.Reals.R_sqrt <> sqrt def
R4166:4168 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4169:4171 DeepSpec.minic.tests.contracts.amm.cst_man <> eta var
R4179:4181 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4110:4113 Coq.Reals.Rdefinitions <> ::R_scope:x_'<='_x_'<='_x not
R4117:4120 Coq.Reals.Rdefinitions <> ::R_scope:x_'<='_x_'<='_x not
R4114:4116 DeepSpec.minic.tests.contracts.amm.cst_man <> eta var
R4114:4116 DeepSpec.minic.tests.contracts.amm.cst_man <> eta var
R4223:4230 Interval.Tactic <> i_bisect constr
R4223:4230 Interval.Tactic <> i_bisect constr
prf 4250:4258 <> pos_deriv
R4272:4272 Coq.Reals.Rdefinitions <> R defax
R4281:4284 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4313:4316 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R4305:4307 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4286:4289 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4304:4304 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4291:4292 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4293:4296 Coq.Reals.R_sqrt <> sqrt def
R4299:4301 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4302:4302 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R4309:4309 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4276:4279 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R4275:4275 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
def 4369:4378 <> extended_f
R4385:4385 Coq.Reals.Rdefinitions <> R defax
R4390:4390 Coq.Reals.Rdefinitions <> R defax
R4415:4419 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4437:4437 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4396:4396 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R4412:4413 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R4408:4410 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4397:4400 Coq.Reals.R_sqrt <> sqrt def
R4403:4405 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4406:4406 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R4420:4420 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4426:4430 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4436:4436 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4422:4422 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4432:4434 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4435:4435 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
def 4453:4463 <> extended_f'
R4470:4470 Coq.Reals.Rdefinitions <> R defax
R4475:4475 Coq.Reals.Rdefinitions <> R defax
R4500:4502 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4481:4484 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4499:4499 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4486:4487 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4488:4491 Coq.Reals.R_sqrt <> sqrt def
R4494:4496 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4497:4497 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R4504:4504 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
def 4522:4527 <> P_gt_1
R4534:4534 Coq.Reals.Rdefinitions <> R defax
R4549:4551 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R4548:4548 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
prf 4565:4574 <> is_deriv_f
R4590:4590 Coq.Reals.Rdefinitions <> R defax
R4602:4605 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4606:4621 Coquelicot.Derive <> is_derive def
R4637:4647 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f' def
R4649:4649 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R4634:4634 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R4623:4632 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R4594:4599 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R4601:4601 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R4683:4692 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R4709:4719 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f' def
R4736:4750 Coquelicot.Derive <> is_derive_minus thm
R4860:4862 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4838:4840 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4842:4843 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4844:4847 Coq.Reals.R_sqrt <> sqrt def
R4851:4853 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4801:4801 Coq.Reals.Rdefinitions <> R defax
R4813:4816 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4823:4823 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4807:4809 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4818:4820 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4821:4822 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R4762:4762 Coq.Reals.Rdefinitions <> R defax
R4767:4767 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R4785:4786 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R4781:4783 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4768:4771 Coq.Reals.R_sqrt <> sqrt def
R4775:4777 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4778:4779 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R4736:4750 Coquelicot.Derive <> is_derive_minus thm
R4860:4862 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4838:4840 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4842:4843 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4844:4847 Coq.Reals.R_sqrt <> sqrt def
R4851:4853 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4801:4801 Coq.Reals.Rdefinitions <> R defax
R4813:4816 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4823:4823 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4807:4809 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4818:4820 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4821:4822 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R4762:4762 Coq.Reals.Rdefinitions <> R defax
R4767:4767 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R4785:4786 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R4781:4783 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4768:4771 Coq.Reals.R_sqrt <> sqrt def
R4775:4777 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4778:4779 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R4889:4891 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4893:4895 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4896:4899 Coq.Reals.R_sqrt <> sqrt def
R4903:4905 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4916:4919 Coquelicot.Hierarchy <> scal def
R4948:4951 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4968:4968 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4964:4966 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4952:4955 Coq.Reals.R_sqrt <> sqrt def
R4959:4961 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4923:4926 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4943:4943 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4928:4930 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4931:4934 Coq.Reals.R_sqrt <> sqrt def
R4938:4940 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4889:4891 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4893:4895 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4896:4899 Coq.Reals.R_sqrt <> sqrt def
R4903:4905 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4916:4919 Coquelicot.Hierarchy <> scal def
R4948:4951 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4968:4968 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4964:4966 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R4952:4955 Coq.Reals.R_sqrt <> sqrt def
R4959:4961 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4923:4926 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4943:4943 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R4928:4930 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R4931:4934 Coq.Reals.R_sqrt <> sqrt def
R4938:4940 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R4989:5002 Coquelicot.Derive <> is_derive_comp thm
R5087:5090 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5107:5107 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5092:5094 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5095:5098 Coq.Reals.R_sqrt <> sqrt def
R5102:5104 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5064:5067 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5082:5082 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5079:5080 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5068:5071 Coq.Reals.R_sqrt <> sqrt def
R5075:5076 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5037:5037 Coq.Reals.Rdefinitions <> R defax
R5055:5056 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5042:5045 Coq.Reals.R_sqrt <> sqrt def
R5049:5051 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5052:5053 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5014:5014 Coq.Reals.Rdefinitions <> R defax
R5021:5023 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R5019:5020 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R4989:5002 Coquelicot.Derive <> is_derive_comp thm
R5087:5090 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5107:5107 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5092:5094 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5095:5098 Coq.Reals.R_sqrt <> sqrt def
R5102:5104 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5064:5067 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5082:5082 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5079:5080 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5068:5071 Coq.Reals.R_sqrt <> sqrt def
R5075:5076 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5037:5037 Coq.Reals.Rdefinitions <> R defax
R5055:5056 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5042:5045 Coq.Reals.R_sqrt <> sqrt def
R5049:5051 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5052:5053 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5014:5014 Coq.Reals.Rdefinitions <> R defax
R5021:5023 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R5019:5020 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5145:5147 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5140:5142 Coq.Reals.Raxioms <> INR def
R5145:5147 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5140:5142 Coq.Reals.Raxioms <> INR def
R5185:5186 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5173:5176 Coq.Reals.R_sqrt <> sqrt def
R5180:5182 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5196:5196 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R5210:5213 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R5207:5208 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5197:5200 Coq.Reals.R_sqrt <> sqrt def
R5204:5204 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5214:5226 Coq.Init.Nat <> pred def
R5185:5186 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5173:5176 Coq.Reals.R_sqrt <> sqrt def
R5180:5182 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5196:5196 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R5210:5213 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R5207:5208 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5197:5200 Coq.Reals.R_sqrt <> sqrt def
R5204:5204 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5214:5226 Coq.Init.Nat <> pred def
R5256:5268 Coquelicot.Derive <> is_derive_pow thm
R5307:5307 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5296:5299 Coq.Reals.R_sqrt <> sqrt def
R5303:5304 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5280:5280 Coq.Reals.Rdefinitions <> R defax
R5285:5286 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5256:5268 Coquelicot.Derive <> is_derive_pow thm
R5307:5307 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5296:5299 Coq.Reals.R_sqrt <> sqrt def
R5303:5304 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5280:5280 Coq.Reals.Rdefinitions <> R defax
R5285:5286 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5344:5346 Coquelicot.Hierarchy <> one def
R5348:5353 Coquelicot.Hierarchy <> R_Ring canonstruc
R5344:5346 Coquelicot.Hierarchy <> one def
R5348:5353 Coquelicot.Hierarchy <> R_Ring canonstruc
R5382:5393 Coquelicot.Derive <> is_derive_id thm
R5395:5403 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R5382:5393 Coquelicot.Derive <> is_derive_id thm
R5395:5403 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R5426:5428 Coquelicot.Hierarchy <> one def
R5470:5482 Coq.Init.Nat <> pred def
R5517:5519 Coq.Reals.Raxioms <> INR def
R5517:5519 Coq.Reals.Raxioms <> INR def
R5559:5562 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5577:5577 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5564:5566 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5567:5570 Coq.Reals.R_sqrt <> sqrt def
R5574:5574 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5606:5608 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5587:5590 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5605:5605 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5592:5594 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5595:5598 Coq.Reals.R_sqrt <> sqrt def
R5602:5602 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5559:5562 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5577:5577 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5564:5566 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5567:5570 Coq.Reals.R_sqrt <> sqrt def
R5574:5574 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5606:5608 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R5587:5590 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5605:5605 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5592:5594 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5595:5598 Coq.Reals.R_sqrt <> sqrt def
R5602:5602 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5639:5653 Coquelicot.Derive <> is_derive_minus thm
R5709:5712 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5729:5729 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5714:5716 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5717:5720 Coq.Reals.R_sqrt <> sqrt def
R5724:5726 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5695:5695 Coq.Reals.Rdefinitions <> R defax
R5665:5665 Coq.Reals.Rdefinitions <> R defax
R5670:5673 Coq.Reals.R_sqrt <> sqrt def
R5677:5679 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5680:5681 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5639:5653 Coquelicot.Derive <> is_derive_minus thm
R5709:5712 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5729:5729 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5714:5716 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5717:5720 Coq.Reals.R_sqrt <> sqrt def
R5724:5726 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5695:5695 Coq.Reals.Rdefinitions <> R defax
R5665:5665 Coq.Reals.Rdefinitions <> R defax
R5670:5673 Coq.Reals.R_sqrt <> sqrt def
R5677:5679 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5680:5681 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5764:5767 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5784:5784 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5769:5771 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5772:5775 Coq.Reals.R_sqrt <> sqrt def
R5779:5781 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5793:5796 Coquelicot.Hierarchy <> scal def
R5802:5805 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5822:5822 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5807:5809 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5810:5813 Coq.Reals.R_sqrt <> sqrt def
R5817:5819 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5764:5767 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5784:5784 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5769:5771 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5772:5775 Coq.Reals.R_sqrt <> sqrt def
R5779:5781 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5793:5796 Coquelicot.Hierarchy <> scal def
R5802:5805 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5822:5822 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5807:5809 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5810:5813 Coq.Reals.R_sqrt <> sqrt def
R5817:5819 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5848:5861 Coquelicot.Derive <> is_derive_comp thm
R5914:5917 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5934:5934 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5919:5921 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5922:5925 Coq.Reals.R_sqrt <> sqrt def
R5929:5931 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5897:5897 Coq.Reals.Rdefinitions <> R defax
R5903:5905 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5906:5907 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5873:5873 Coq.Reals.Rdefinitions <> R defax
R5878:5881 Coq.Reals.R_sqrt <> sqrt def
R5883:5884 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5848:5861 Coquelicot.Derive <> is_derive_comp thm
R5914:5917 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5934:5934 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R5919:5921 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R5922:5925 Coq.Reals.R_sqrt <> sqrt def
R5929:5931 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5897:5897 Coq.Reals.Rdefinitions <> R defax
R5903:5905 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5906:5907 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5873:5873 Coq.Reals.Rdefinitions <> R defax
R5878:5881 Coq.Reals.R_sqrt <> sqrt def
R5883:5884 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5962:5975 Coquelicot.ElemFct <> is_derive_sqrt thm
R5998:5999 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5987:5987 Coq.Reals.Rdefinitions <> R defax
R5992:5993 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R5962:5975 Coquelicot.ElemFct <> is_derive_sqrt thm
R5998:5999 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R5987:5987 Coq.Reals.Rdefinitions <> R defax
R5992:5993 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R6038:6040 Coquelicot.Hierarchy <> one def
R6042:6047 Coquelicot.Hierarchy <> R_Ring canonstruc
R6038:6040 Coquelicot.Hierarchy <> one def
R6042:6047 Coquelicot.Hierarchy <> R_Ring canonstruc
R6078:6089 Coquelicot.Derive <> is_derive_id thm
R6091:6099 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R6078:6089 Coquelicot.Derive <> is_derive_id thm
R6091:6099 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R6124:6126 Coquelicot.Hierarchy <> one def
R6156:6161 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R6205:6207 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R6205:6207 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R6245:6258 Coquelicot.Derive <> is_derive_plus thm
R6290:6290 Coq.Reals.Rdefinitions <> R defax
R6295:6296 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R6270:6270 Coq.Reals.Rdefinitions <> R defax
R6245:6258 Coquelicot.Derive <> is_derive_plus thm
R6290:6290 Coq.Reals.Rdefinitions <> R defax
R6295:6296 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R6270:6270 Coq.Reals.Rdefinitions <> R defax
R6338:6341 Coquelicot.Hierarchy <> zero def
R6343:6348 Coquelicot.Hierarchy <> R_Ring canonstruc
R6338:6341 Coquelicot.Hierarchy <> zero def
R6343:6348 Coquelicot.Hierarchy <> R_Ring canonstruc
R6388:6402 Coquelicot.Derive <> is_derive_const thm
R6404:6412 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R6388:6402 Coquelicot.Derive <> is_derive_const thm
R6404:6412 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R6437:6440 Coquelicot.Hierarchy <> zero def
R6494:6496 Coquelicot.Hierarchy <> one def
R6498:6503 Coquelicot.Hierarchy <> R_Ring canonstruc
R6494:6496 Coquelicot.Hierarchy <> one def
R6498:6503 Coquelicot.Hierarchy <> R_Ring canonstruc
R6529:6540 Coquelicot.Derive <> is_derive_id thm
R6542:6550 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R6529:6540 Coquelicot.Derive <> is_derive_id thm
R6542:6550 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R6575:6577 Coquelicot.Hierarchy <> one def
R6621:6624 Coquelicot.Hierarchy <> scal def
R6641:6644 Coquelicot.Hierarchy <> mult def
R6690:6693 Coquelicot.Hierarchy <> zero def
R6695:6700 Coquelicot.Hierarchy <> R_Ring canonstruc
R6690:6693 Coquelicot.Hierarchy <> zero def
R6695:6700 Coquelicot.Hierarchy <> R_Ring canonstruc
R6740:6754 Coquelicot.Derive <> is_derive_const thm
R6756:6764 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R6740:6754 Coquelicot.Derive <> is_derive_const thm
R6756:6764 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R6789:6792 Coquelicot.Hierarchy <> zero def
R6836:6839 Coquelicot.Hierarchy <> scal def
R6856:6859 Coquelicot.Hierarchy <> mult def
R6896:6914 Coq.Reals.RIneq <> Rmult_minus_distr_l thm
R6896:6914 Coq.Reals.RIneq <> Rmult_minus_distr_l thm
R6896:6914 Coq.Reals.RIneq <> Rmult_minus_distr_l thm
R6896:6914 Coq.Reals.RIneq <> Rmult_minus_distr_l thm
R6896:6914 Coq.Reals.RIneq <> Rmult_minus_distr_l thm
R6930:6939 Coq.Init.Logic <> not_eq_sym thm
R6930:6939 Coq.Init.Logic <> not_eq_sym thm
R6948:6957 Coq.Reals.RIneq <> Rlt_not_eq thm
R6948:6957 Coq.Reals.RIneq <> Rlt_not_eq thm
R6981:6986 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R7022:7022 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R7039:7041 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R7035:7035 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R7022:7022 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R7039:7041 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R7035:7035 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R7073:7086 Coquelicot.Derive <> is_derive_scal thm
R7115:7115 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R7098:7098 Coq.Reals.Rdefinitions <> R defax
R7104:7106 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R7107:7108 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R7073:7086 Coquelicot.Derive <> is_derive_scal thm
R7115:7115 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R7098:7098 Coq.Reals.Rdefinitions <> R defax
R7104:7106 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R7107:7108 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R7150:7152 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R7150:7152 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R7184:7197 Coquelicot.Derive <> is_derive_plus thm
R7229:7229 Coq.Reals.Rdefinitions <> R defax
R7234:7235 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R7209:7209 Coq.Reals.Rdefinitions <> R defax
R7184:7197 Coquelicot.Derive <> is_derive_plus thm
R7229:7229 Coq.Reals.Rdefinitions <> R defax
R7234:7235 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R7209:7209 Coq.Reals.Rdefinitions <> R defax
R7271:7274 Coquelicot.Hierarchy <> zero def
R7276:7281 Coquelicot.Hierarchy <> R_Ring canonstruc
R7271:7274 Coquelicot.Hierarchy <> zero def
R7276:7281 Coquelicot.Hierarchy <> R_Ring canonstruc
R7301:7315 Coquelicot.Derive <> is_derive_const thm
R7317:7325 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R7301:7315 Coquelicot.Derive <> is_derive_const thm
R7317:7325 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R7344:7347 Coquelicot.Hierarchy <> zero def
R7395:7397 Coquelicot.Hierarchy <> one def
R7399:7404 Coquelicot.Hierarchy <> R_Ring canonstruc
R7395:7397 Coquelicot.Hierarchy <> one def
R7399:7404 Coquelicot.Hierarchy <> R_Ring canonstruc
R7424:7435 Coquelicot.Derive <> is_derive_id thm
R7437:7445 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R7424:7435 Coquelicot.Derive <> is_derive_id thm
R7437:7445 Coquelicot.Hierarchy <> R_AbsRing canonstruc
R7464:7466 Coquelicot.Hierarchy <> one def
prf 7501:7506 <> eps_sq
R7518:7521 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R7568:7571 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R7543:7547 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R7567:7567 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R7522:7522 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R7540:7541 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R7536:7538 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R7523:7526 Coq.Reals.R_sqrt <> sqrt def
R7529:7531 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R7532:7534 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R7548:7548 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R7554:7558 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R7566:7566 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R7550:7550 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R7560:7562 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R7563:7565 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R7513:7516 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R7510:7512 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R7612:7627 Interval.Missing.Stdlib <> connected def
R7629:7634 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R7612:7627 Interval.Missing.Stdlib <> connected def
R7629:7634 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R7655:7670 Interval.Missing.Stdlib <> connected def
R7688:7693 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R7703:7708 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R7747:7755 Coq.Reals.RIneq <> Rge_trans thm
R7747:7755 Coq.Reals.RIneq <> Rge_trans thm
R7771:7776 Coq.Reals.RIneq <> Rle_ge thm
R7771:7776 Coq.Reals.RIneq <> Rle_ge thm
R7825:7829 Interval.Interval.Interval_compl <> Rincr def
R7838:7847 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R7831:7836 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R7825:7829 Interval.Interval.Interval_compl <> Rincr def
R7838:7847 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R7831:7836 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R7869:7888 Interval.Interval.Interval_compl <> Rderive_pos_imp_incr thm
R7895:7904 DeepSpec.minic.tests.contracts.amm.cst_man <> is_deriv_f thm
R7869:7888 Interval.Interval.Interval_compl <> Rderive_pos_imp_incr thm
R7895:7904 DeepSpec.minic.tests.contracts.amm.cst_man <> is_deriv_f thm
R7925:7933 Interval.Interval.Interval_compl <> Rpos_over def
R7950:7955 Coq.Reals.RIneq <> Rge_le thm
R7950:7955 Coq.Reals.RIneq <> Rge_le thm
R7965:7975 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f' def
R7995:8003 DeepSpec.minic.tests.contracts.amm.cst_man <> pos_deriv thm
R7995:8003 DeepSpec.minic.tests.contracts.amm.cst_man <> pos_deriv thm
R8013:8018 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R8090:8093 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R8094:8094 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R8118:8137 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R8146:8149 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R8150:8150 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8197:8201 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8172:8176 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R8196:8196 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R8151:8151 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R8169:8170 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R8165:8167 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R8152:8155 Coq.Reals.R_sqrt <> sqrt def
R8158:8160 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R8161:8163 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8177:8177 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8183:8187 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8195:8195 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8179:8179 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R8189:8191 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R8192:8194 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8141:8144 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8138:8140 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8095:8099 Interval.Interval.Interval_compl <> Rincr def
R8108:8117 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8101:8106 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R8071:8071 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8084:8088 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8072:8081 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8090:8093 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R8094:8094 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R8118:8137 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R8146:8149 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R8150:8150 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8197:8201 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8172:8176 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R8196:8196 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R8151:8151 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R8169:8170 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R8165:8167 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R8152:8155 Coq.Reals.R_sqrt <> sqrt def
R8158:8160 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R8161:8163 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8177:8177 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8183:8187 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8195:8195 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8179:8179 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R8189:8191 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R8192:8194 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8141:8144 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8138:8140 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8095:8099 Interval.Interval.Interval_compl <> Rincr def
R8108:8117 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8101:8106 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R8071:8071 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8084:8088 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8072:8081 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8269:8271 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R8245:8245 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R8264:8267 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R8260:8262 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R8246:8249 Coq.Reals.R_sqrt <> sqrt def
R8253:8255 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R8256:8258 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8279:8282 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8290:8290 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8273:8275 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R8284:8286 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R8287:8289 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8299:8308 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8310:8312 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8269:8271 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R8245:8245 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R8264:8267 Coq.Reals.Rfunctions <> ::R_scope:x_'^'_x not
R8260:8262 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R8246:8249 Coq.Reals.R_sqrt <> sqrt def
R8253:8255 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R8256:8258 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8279:8282 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8290:8290 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8273:8275 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R8284:8286 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R8287:8289 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8299:8308 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8310:8312 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8353:8355 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8341:8350 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8353:8355 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8341:8350 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8380:8389 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8443:8446 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8429:8438 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8440:8442 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8447:8456 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8443:8446 Coq.Reals.Rdefinitions <> ::R_scope:x_'>='_x not
R8429:8438 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8440:8442 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8447:8456 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8483:8487 Interval.Interval.Interval_compl <> Rincr def
R8505:8510 Coq.Reals.RIneq <> Rle_ge thm
R8505:8510 Coq.Reals.RIneq <> Rle_ge thm
R8546:8551 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R8566:8571 DeepSpec.minic.tests.contracts.amm.cst_man <> P_gt_1 def
R8589:8594 Coq.Reals.RIneq <> Rge_le thm
R8589:8594 Coq.Reals.RIneq <> Rge_le thm
R8625:8633 Coq.Reals.RIneq <> Rge_trans thm
R8653:8662 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8636:8645 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8647:8649 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8625:8633 Coq.Reals.RIneq <> Rge_trans thm
R8653:8662 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8636:8645 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8647:8649 DeepSpec.minic.tests.contracts.amm.cst_man <> eps def
R8724:8733 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8804:8813 DeepSpec.minic.tests.contracts.amm.cst_man <> extended_f def
R8902:8922 Coq.Reals.Ranalysis1 <> derivable_pt_lim_comp thm
R8979:8982 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9001:9001 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R8984:8987 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9000:9000 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R8988:8991 Coq.Reals.R_sqrt <> sqrt def
R8995:8997 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R8957:8957 Coq.Reals.Rdefinitions <> R defax
R8962:8965 Coq.Reals.R_sqrt <> sqrt def
R8967:8968 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R8934:8934 Coq.Reals.Rdefinitions <> R defax
R8940:8942 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R8943:8944 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R9050:9052 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9103:9123 Coq.Reals.Ranalysis1 <> derivable_pt_lim_plus thm
R9143:9144 Coq.Reals.Ranalysis1 <> id def
R9135:9135 Coq.Reals.Rdefinitions <> R defax
R9185:9206 Coq.Reals.Ranalysis1 <> derivable_pt_lim_const thm
R9240:9258 Coq.Reals.Ranalysis1 <> derivable_pt_lim_id thm
R9296:9299 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9316:9316 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9301:9303 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9304:9307 Coq.Reals.R_sqrt <> sqrt def
R9311:9313 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9325:9327 Coq.Reals.Rdefinitions <> ::R_scope:'/'_x not
R9344:9344 Coq.Reals.Rdefinitions <> ::R_scope:'/'_x not
R9329:9331 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9332:9335 Coq.Reals.R_sqrt <> sqrt def
R9339:9341 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9386:9406 Coq.Reals.Sqrt_reg <> derivable_pt_lim_sqrt thm
R9440:9470 Coq.micromega.Fourier_util <> Rlt_zero_pos_plus1 thm
prf 9481:9493 <> deriv_lim_T_f
R9509:9511 Coq.Init.Datatypes <> nat ind
R9519:9519 Coq.Reals.Rdefinitions <> R defax
R9535:9538 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R9548:9551 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R9552:9567 Coq.Reals.Ranalysis1 <> derivable_pt_lim def
R9582:9586 DeepSpec.minic.tests.contracts.amm.cst_man <> T_f_1 def
R9594:9594 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R9589:9589 Coq.Init.Datatypes <> S constr
R9591:9591 DeepSpec.minic.tests.contracts.amm.cst_man <> k var
R9579:9579 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R9570:9574 DeepSpec.minic.tests.contracts.amm.cst_man <> T_f_1 def
R9576:9576 DeepSpec.minic.tests.contracts.amm.cst_man <> k var
R9540:9542 Coq.Reals.Rdefinitions <> ::R_scope:x_'<'_x_'<'_x not
R9544:9546 Coq.Reals.Rdefinitions <> ::R_scope:x_'<'_x_'<'_x not
R9543:9543 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R9543:9543 DeepSpec.minic.tests.contracts.amm.cst_man <> x var
R9525:9528 Coq.Init.Peano <> ::nat_scope:x_'<='_x not
R9524:9524 DeepSpec.minic.tests.contracts.amm.cst_man <> k var
R9643:9646 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R9635:9636 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9649:9651 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9643:9646 Coq.Init.Logic <> ::type_scope:x_'\/'_x not
R9635:9636 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9649:9651 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9759:9761 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R9738:9741 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9758:9758 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9743:9745 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9746:9749 Coq.Reals.R_sqrt <> sqrt def
R9753:9755 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9763:9766 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9793:9793 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9778:9780 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9768:9771 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9777:9777 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9773:9775 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9781:9784 Coq.Reals.R_sqrt <> sqrt def
R9788:9790 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9833:9835 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9812:9815 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9832:9832 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9817:9819 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9820:9823 Coq.Reals.R_sqrt <> sqrt def
R9827:9829 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9839:9842 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9869:9869 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9854:9856 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9844:9847 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9853:9853 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9849:9851 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9857:9860 Coq.Reals.R_sqrt <> sqrt def
R9864:9866 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9759:9761 Coq.Reals.Rdefinitions <> ::R_scope:x_'-'_x not
R9738:9741 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9758:9758 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9743:9745 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9746:9749 Coq.Reals.R_sqrt <> sqrt def
R9753:9755 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9763:9766 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9793:9793 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9778:9780 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9768:9771 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9777:9777 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9773:9775 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9781:9784 Coq.Reals.R_sqrt <> sqrt def
R9788:9790 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9833:9835 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9812:9815 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9832:9832 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9817:9819 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9820:9823 Coq.Reals.R_sqrt <> sqrt def
R9827:9829 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9839:9842 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9869:9869 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9854:9856 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9844:9847 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9853:9853 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9849:9851 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9857:9860 Coq.Reals.R_sqrt <> sqrt def
R9864:9866 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9896:9916 Coq.Reals.Ranalysis1 <> derivable_pt_lim_plus thm
R10023:10026 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R10053:10053 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R10038:10040 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R10028:10031 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R10037:10037 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R10033:10035 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R10041:10044 Coq.Reals.R_sqrt <> sqrt def
R10048:10050 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9986:9989 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R10006:10006 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9991:9993 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9994:9997 Coq.Reals.R_sqrt <> sqrt def
R10001:10003 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9958:9958 Coq.Reals.Rdefinitions <> R defax
R9964:9966 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9967:9970 Coq.Reals.R_sqrt <> sqrt def
R9974:9976 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9977:9978 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R9928:9928 Coq.Reals.Rdefinitions <> R defax
R9933:9936 Coq.Reals.R_sqrt <> sqrt def
R9940:9942 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9943:9944 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R9896:9916 Coq.Reals.Ranalysis1 <> derivable_pt_lim_plus thm
R10023:10026 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R10053:10053 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R10038:10040 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R10028:10031 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R10037:10037 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R10033:10035 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R10041:10044 Coq.Reals.R_sqrt <> sqrt def
R10048:10050 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9986:9989 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R10006:10006 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9991:9993 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R9994:9997 Coq.Reals.R_sqrt <> sqrt def
R10001:10003 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9958:9958 Coq.Reals.Rdefinitions <> R defax
R9964:9966 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R9967:9970 Coq.Reals.R_sqrt <> sqrt def
R9974:9976 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9977:9978 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R9928:9928 Coq.Reals.Rdefinitions <> R defax
R9933:9936 Coq.Reals.R_sqrt <> sqrt def
R9940:9942 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R9943:9944 DeepSpec.minic.tests.contracts.amm.cst_man <> x0 var
R10080:10083 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R10100:10100 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R10085:10087 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R10088:10091 Coq.Reals.R_sqrt <> sqrt def
R10095:10097 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R10131:10133 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R10110:10113 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R10130:10130 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not
R10115:10117 Coq.Reals.Rdefinitions <> ::R_scope:x_'*'_x not
R10118:10121 Coq.Reals.R_sqrt <> sqrt def
R10125:10127 Coq.Reals.Rdefinitions <> ::R_scope:x_'+'_x not
R10080:10083 Coq.Reals.Rdefinitions <> ::R_scope:x_'/'_x not