Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
profile_ltac.ml
Sprache: SML
Untersuchungsergebnis.out Download desHaskell {Haskell[80] Ada[347] Abap[474]}zum Wurzelverzeichnis wechseln
1 subgoal
x3 : nat
============================
forall x x1 x4 x0 : nat,
(forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
1 subgoal
x3, x, x1, x4, x0 : nat
H : forall x x3 : nat, x + x1 = x4 + x3
============================
x + x1 = x4 + x0
1 subgoal
x3 : nat
============================
forall x x1 x4 x0 : nat,
(forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
x + x1 = x4 + x0 -> foo (S x)
1 subgoal
x3 : nat
============================
forall x x1 x4 x0 : nat,
(forall x2 x5 : nat,
x2 + x1 = x4 + x5 ->
forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
x + x1 = x4 + x0 ->
forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, x, x1, x4, x0 : nat
============================
(forall x2 x5 : nat,
x2 + x1 = x4 + x5 ->
forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
x + x1 = x4 + x0 ->
forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, x, x1, x4, x0 : nat
H : forall x x3 : nat,
x + x1 = x4 + x3 ->
forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
H0 : x + x1 = x4 + x0
============================
forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, x, x1, x4, x0 : nat
H : forall x x3 : nat,
x + x1 = x4 + x3 ->
forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (Datatypes.S x + x1)
H0 : x + x1 = x4 + x0
x5, x6, x7, S : nat
============================
x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, a : nat
H : a = 0 -> forall a : nat, a = 0
============================
a = 0
[ zur Elbe Produktseite wechseln0.109Quellennavigators
]
|
|
