spechub/Hets — pull request #1324 by cmaeder (2014-08-08 17:01:30+00:00)
Title: reconstruct missing pattern term

fixes #1137.

```
the definition of __<__ is not complete
the defining formula group is:
1. forall x : Nat . 0 < suc(x)
2. forall x, y : Nat . x < y => suc(x) < suc(y)
missing pattern for: __<__(0, op 0 : Nat)
missing pattern for: __<__(suc((var x : Nat)), op 0 : Nat)

the definition of f is not complete
the defining formula group is:
1. forall x, y : Nat . f(x, suc(y)) = 0
2. forall x, y : Nat . f(suc(x), y) = suc(0)
3. forall x : Nat . f(suc(suc(x)), 0) = x
missing pattern for: f(0, op 0 : Nat)

the definition of f is not complete
the defining formula group is:
1. forall x, y : Nat . f(x, suc(y), 0) = 0
2. forall x, y, z : Nat . f(suc(x), suc(y), suc(z)) = suc(0)
missing pattern for: f(0, op 0 : Nat, _)
missing pattern for: f(0, suc((var y : Nat)), op suc : Nat -> Nat)
missing pattern for: f(suc((var _ : Nat)), op 0 : Nat, _)
```