Ticket #453: bug.v

File bug.v, 5.9 KB (added by coquser, 12 years ago)

A long inductive defintion.

Line 
1Inductive test : bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
2  | Con01 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
3              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
4           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
5  | Con02 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
6              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
7           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
8  | Con03 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
9              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
10           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
11  | Con04 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
12              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
13           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
14  | Con05 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
15              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
16           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
17  | Con06 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
18              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
19           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
20  | Con07 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
21              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
22           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
23  | Con08 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
24              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
25           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
26  | Con09 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
27              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
28           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
29  | Con10 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
30              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
31           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
32  | Con11 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
33              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
34           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
35  | Con12 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
36              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
37           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
38  | Con13 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
39              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
40           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
41  | Con14 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
42              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
43           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
44  | Con15 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
45              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
46           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
47  | Con16 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
48              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
49           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
50  | Con17 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
51              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
52           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
53  | Con18 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
54              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
55           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
56  | Con19 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
57              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
58           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
59  | Con20 : forall variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8,
60              test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
61           -> test variable1 variable2 variable3 variable4 variable5 variable6 variable7 variable8
62  .