| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: examples.summary Sprache: Unknown
|
Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[1072] Hlasm[2548] Haskell[2912]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] *** *** top (19:46:28 11/7/2014) *** Generated by proveit - ProofLite-6.0.9 (3/14/14) *** Trusted Oracles *** MetiTarski: MetiTarski Theorem Prover via PVS proof rule metit *** Proof summary for theory top Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory field_examples f1_TCC1...............................proved - complete [shostak](0.06 s) f1_TCC2...............................proved - complete [shostak](0.05 s) f1....................................proved - complete [shostak](0.20 s) f2_TCC1...............................proved - complete [shostak](0.03 s) f2_TCC2...............................proved - complete [shostak](0.03 s) f2....................................proved - complete [shostak](0.17 s) f3....................................proved - complete [shostak](0.21 s) f4....................................proved - complete [shostak](0.17 s) f5....................................proved - complete [shostak](0.35 s) f6_TCC1...............................proved - complete [shostak](0.26 s) f6_TCC2...............................proved - complete [shostak](0.04 s) f6....................................proved - complete [shostak](0.90 s) f7....................................proved - complete [shostak](0.96 s) f8....................................proved - complete [shostak](1.05 s) f9....................................proved - complete [shostak](1.02 s) f10...................................proved - complete [shostak](0.80 s) f11_TCC1..............................proved - complete [shostak](0.03 s) f11...................................proved - complete [shostak](0.51 s) cf1...................................proved - complete [shostak](0.40 s) cf2...................................proved - complete [shostak](0.50 s) cf3...................................proved - complete [shostak](0.54 s) cf4...................................proved - complete [shostak](-1.17 s) cf5...................................proved - complete [shostak](0.59 s) gr1_TCC1..............................proved - complete [shostak](0.05 s) gr1...................................proved - complete [shostak](0.19 s) gr2_TCC1..............................proved - complete [shostak](0.07 s) gr2_TCC2..............................proved - complete [shostak](0.08 s) gr2_TCC3..............................proved - complete [shostak](0.08 s) gr2...................................proved - complete [shostak](0.22 s) gr3_TCC1..............................proved - complete [shostak](0.07 s) gr3_TCC2..............................proved - complete [shostak](0.02 s) gr3...................................proved - complete [shostak](0.36 s) quadratic.............................proved - complete [shostak](1.51 s) kb3d_TCC1.............................proved - complete [shostak](0.18 s) kb3d_TCC2.............................proved - complete [shostak](0.11 s) kb3d_TCC3.............................proved - complete [shostak](0.37 s) kb3d_TCC4.............................proved - complete [shostak](0.40 s) kb3d..................................proved - complete [shostak](3.22 s) Theory totals: 38 formulas, 38 attempted, 38 succeeded (14.62 s) Proof summary for theory interval_examples sqrt23................................proved - incomplete [shostak](2.53 s) sin6sqrt2.............................proved - incomplete [shostak](1.64 s) sqrtx3_TCC1...........................proved - complete [shostak](0.05 s) sqrtx3................................proved - incomplete [shostak](1.64 s) tr_TCC1...............................proved - incomplete [shostak](0.10 s) tr_250_35_TCC1........................proved - incomplete [shostak](1.20 s) tr_250_35.............................proved - incomplete [shostak](2.33 s) tr_200_250_abs_35.....................proved - incomplete [shostak](2.61 s) G_TCC1................................proved - complete [shostak](0.04 s) A_and_S_TCC1..........................proved - complete [shostak](0.06 s) A_and_S_TCC2..........................proved - complete [shostak](0.07 s) A_and_S...............................proved - incomplete [shostak](1.08 s) common_point_TCC1.....................proved - complete [shostak](0.04 s) common_point_TCC2.....................proved - complete [shostak](0.05 s) common_point_TCC3.....................proved - incomplete [shostak](0.23 s) common_point_TCC4.....................proved - incomplete [shostak](0.23 s) common_point..........................proved - incomplete [shostak](4.85 s) r_TCC1................................proved - complete [shostak](0.05 s) r_TCC2................................proved - complete [shostak](0.04 s) atan_implementation...................proved - incomplete [shostak](1.94 s) ex1_ba_TCC1...........................proved - complete [shostak](0.04 s) ex1_ba_TCC2...........................proved - complete [shostak](0.08 s) ex1_ba................................proved - incomplete [shostak](1.21 s) ex2_ba_TCC1...........................proved - complete [shostak](0.06 s) ex2_ba................................proved - incomplete [shostak](1.18 s) ex3_ba_TCC1...........................proved - complete [shostak](0.06 s) ex3_ba................................proved - incomplete [shostak](1.30 s) ex4_ba................................proved - incomplete [shostak](1.31 s) ex5_ba_TCC1...........................proved - complete [shostak](0.10 s) ex5_ba................................proved - incomplete [shostak](1.39 s) ex6_ba................................proved - incomplete [shostak](1.30 s) ex7_ba................................proved - incomplete [shostak](1.34 s) Tunnel_3_IL...........................proved - incomplete [shostak](1.87 s) Tunnel_3_IL_LU........................proved - incomplete [shostak](2.05 s) Theory totals: 34 formulas, 34 attempted, 34 succeeded (34.07 s) Proof summary for theory interval_examples4Q zero_to_one_quarter...................proved - complete [shostak](0.44 s) Heart_TCC1............................proved - complete [shostak](0.03 s) Heart_TCC2............................proved - complete [shostak](0.03 s) hdp_mm_TCC1...........................proved - complete [shostak](0.04 s) hdp_mm_TCC2...........................proved - complete [shostak](0.04 s) hdp_mm_TCC3...........................proved - complete [shostak](0.04 s) hdp_mm_TCC4...........................proved - complete [shostak](0.04 s) hdp_mm_TCC5...........................proved - complete [shostak](0.04 s) hdp_mm_TCC6...........................proved - complete [shostak](0.04 s) hdp_mm................................proved - complete [shostak](4.75 s) hdp_minmax............................proved - complete [shostak](4.93 s) common_point_TCC1.....................proved - complete [shostak](0.04 s) common_point..........................proved - complete [shostak](0.55 s) simple_ite............................proved - complete [shostak](0.55 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (11.56 s) Proof summary for theory metit_examples simple................................proved - complete [shostak](0.02 s) simple_abs............................proved - complete [shostak](0.06 s) sqrtx3_TCC1...........................proved - complete [shostak](0.03 s) sqrtx3................................proved - complete [shostak](0.03 s) tr_35_TCC1............................proved - complete [shostak](0.03 s) tr_35.................................proved - complete [shostak](0.13 s) tr_35_le_TCC1.........................proved - complete [shostak](0.03 s) tr_35_le..............................proved - complete [shostak](0.03 s) sqrt23................................proved - complete [shostak](0.02 s) sin6sqrt2.............................proved - complete [shostak](0.03 s) G_TCC1................................proved - complete [shostak](0.02 s) A_and_S...............................proved - complete [shostak](0.03 s) r_TCC1................................proved - complete [shostak](0.02 s) r_TCC2................................proved - complete [shostak](0.02 s) atan_implementation...................proved - complete [shostak](0.03 s) ajn...................................proved - complete [shostak](0.04 s) ex1_ba_TCC1...........................proved - complete [shostak](0.02 s) ex1_ba_TCC2...........................proved - complete [shostak](0.05 s) ex1_ba................................proved - complete [shostak](0.02 s) ex2_ba_TCC1...........................proved - complete [shostak](0.04 s) ex2_ba................................proved - complete [shostak](0.03 s) ex3_ba_TCC1...........................proved - complete [shostak](0.04 s) ex3_ba................................proved - complete [shostak](0.03 s) ex4_ba................................proved - complete [shostak](0.03 s) ex5_ba_TCC1...........................proved - complete [shostak](0.07 s) ex5_ba................................proved - complete [shostak](0.03 s) ex6_ba................................proved - complete [shostak](0.03 s) ex7_ba................................proved - complete [shostak](0.03 s) quadratic.............................proved - complete [shostak](0.03 s) Tunnel_3_IL...........................proved - complete [shostak](0.03 s) Tunnel_3_IL_LU........................proved - complete [shostak](0.03 s) Ayad_Marche...........................proved - complete [shostak](0.03 s) Theory totals: 32 formulas, 32 attempted, 32 succeeded (1.11 s) Proof summary for theory sturm_examples example_1_TCC1........................proved - complete [shostak](0.04 s) example_1_TCC2........................proved - complete [shostak](0.03 s) example_1_TCC3........................proved - complete [shostak](0.02 s) example_1.............................proved - complete [shostak](2.53 s) example_2.............................proved - complete [shostak](1.07 s) example_3_TCC1........................proved - complete [shostak](0.02 s) example_3_TCC2........................proved - complete [shostak](0.02 s) example_3_TCC3........................proved - complete [shostak](0.03 s) example_3_TCC4........................proved - complete [shostak](0.02 s) example_3_TCC5........................proved - complete [shostak](0.02 s) example_3_TCC6........................proved - complete [shostak](0.03 s) example_3_TCC7........................proved - complete [shostak](0.02 s) example_3_TCC8........................proved - complete [shostak](0.02 s) example_3_TCC9........................proved - complete [shostak](0.03 s) example_3_TCC10.......................proved - complete [shostak](0.02 s) example_3_TCC11.......................proved - complete [shostak](0.02 s) example_3_TCC12.......................proved - complete [shostak](0.02 s) example_3_TCC13.......................proved - complete [shostak](0.03 s) example_3_TCC14.......................proved - complete [shostak](0.13 s) example_3.............................proved - complete [shostak](8.17 s) example_4_TCC1........................proved - complete [shostak](0.02 s) example_4.............................proved - complete [shostak](1.12 s) example_5.............................proved - complete [shostak](0.50 s) example_6_TCC1........................proved - complete [shostak](0.02 s) example_6.............................proved - complete [shostak](0.47 s) example_7.............................proved - complete [shostak](0.52 s) example_8.............................proved - complete [shostak](0.43 s) example_n8............................proved - complete [shostak](0.41 s) example_80............................proved - complete [shostak](0.41 s) example_n80...........................proved - complete [shostak](0.40 s) example_9.............................proved - complete [shostak](0.45 s) example_n9............................proved - complete [shostak](0.44 s) example_90............................proved - complete [shostak](0.32 s) example_n90...........................proved - complete [shostak](0.34 s) example_10............................proved - complete [shostak](0.35 s) example_11............................proved - complete [shostak](0.79 s) example_12_TCC1.......................proved - complete [shostak](0.02 s) example_12_TCC2.......................proved - complete [shostak](0.02 s) example_12............................proved - complete [shostak](1.23 s) legendre_TCC1.........................proved - complete [shostak](0.02 s) legendre_TCC2.........................proved - complete [shostak](0.03 s) legendre_TCC3.........................proved - complete [shostak](0.02 s) legendre..............................proved - complete [shostak](2.89 s) legendre3_TCC1........................proved - complete [shostak](0.10 s) legendre3.............................proved - complete [shostak](9.60 s) harrison_sos_TCC1.....................proved - complete [shostak](0.02 s) harrison_sos_TCC2.....................proved - complete [shostak](0.02 s) harrison_sos..........................proved - complete [shostak](1.24 s) example_13............................proved - complete [shostak](1.02 s) example_14............................proved - complete [shostak](0.40 s) example_15............................proved - complete [shostak](0.43 s) example_16............................proved - complete [shostak](0.59 s) example_17_TCC1.......................proved - complete [shostak](0.02 s) example_17_TCC2.......................proved - complete [shostak](0.03 s) example_17_TCC3.......................proved - complete [shostak](0.02 s) example_17_TCC4.......................proved - complete [shostak](0.03 s) example_17............................proved - complete [shostak](6.59 s) mono_example_1_TCC1...................proved - complete [shostak](0.02 s) mono_example_1........................proved - complete [shostak](1.24 s) mono_example_2_TCC1...................proved - complete [shostak](0.02 s) mono_example_2........................proved - complete [shostak](0.62 s) mono_example_3_TCC1...................proved - complete [shostak](0.02 s) mono_example_3_TCC2...................proved - complete [shostak](0.02 s) mono_example_3........................proved - complete [shostak](1.56 s) mono_example_4_TCC1...................proved - complete [shostak](0.02 s) mono_example_4........................proved - complete [shostak](0.57 s) mono_example_5........................proved - complete [shostak](0.58 s) mono_example_6_TCC1...................proved - complete [shostak](0.03 s) mono_example_6........................proved - complete [shostak](0.62 s) Theory totals: 69 formulas, 69 attempted, 69 succeeded (48.93 s) Proof summary for theory checker_example Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory is_prime is_prime?_TCC1........................proved - complete [shostak](0.02 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.02 s) Grand Totals: 188 proofs, 188 attempted, 188 succeeded (110.31 s) [ Dauer der Verarbeitung: 0.111 Sekunden ] |