Untersuchungsergebnis.out Download desUnknown {[0] [0] [0]}zum Wurzelverzeichnis wechseln
0:-) 0
: nat
1 +_a 2
: nat
1 +_b 2
: nat
1 +_b 2
: nat
1 +_c 2
: nat
1 +_c 2
: nat
Scope nat_scope
Delimiting key is nat
Bound to class nat
"x >= y" := (ge x y)
"x > y" := (gt x y)
"x <= y <= z" := (and (le x y) (le y z))
"x <= y < z" := (and (le x y) (lt y z))
"n <= m" := (le n m)
"x < y <= z" := (and (lt x y) (le y z))
"x < y < z" := (and (lt x y) (lt y z))
"x < y" := (lt x y)
"x - y" := (Nat.sub x y)
"x +_c y" := (Nat.add x y) (only printing)
"x +_b y" := (Nat.add x y)
"x +_a y" := (Nat.add x y)
"x + y" := (Nat.add x y)
"x * y" := (Nat.mul x y)
1 +_b 2
: nat
1 +_a 2
: nat
1 + 2
: nat
1 +_c 2
: nat
[ 0.114Quellennavigators
]