1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
(* This example resulted in a code blow-up. The match compiler generates
thousands of cases. Now fixed by using a naive pattern-by-pattern
match. *)
structure Nbe =
struct
datatype Univ =
Const of string * Univ list
| Free of string * Univ list
| DFree of string
| BVar of int * Univ list
| Abs of (int * (Univ list -> Univ)) * Univ list;
end;
fun c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vp, v_vo, v_vn, v_vi, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.tr.const", [v_vm, v_vl, v_vk, v_vj, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vp, v_vo, v_vn, v_vi, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.tr.const", [v_vm, v_vl, v_vk, v_vj, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.tr.const", [v_vm, v_vl, v_vk, v_vj, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.tr.const", [v_vm, v_vl, v_vk, v_vj, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.tr.const", [v_vm, v_vl, v_vk, v_vj, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.tr.const", [v_vm, v_vl, v_vk, v_vj, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vl, v_vk, v_vj, v_vi, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.e.const", [])), v_v]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vl, v_vk, v_vj, v_vi, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.e.const", [])), v_v]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", []))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vl, v_vk, v_vj, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.tr.const", [v_vi, v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vl, v_vk, v_vj, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.tr.const", [v_vi, v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.tr.const", [v_vi, v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.tr.const", [v_vi, v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, (Nbe.Const ("RedBlackTree.tr.const", [v_vi, v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, (Nbe.Const ("RedBlackTree.tr.const", [v_vi, v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.e.const", [])), v_v]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.e.const", [])), v_v]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", []))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vm, v_vl, v_vk, v_vj, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.tr.const", [v_vp, v_vo, v_vn, v_vi, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vm, v_vl, v_vk, v_vj, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.tr.const", [v_vp, v_vo, v_vn, v_vi, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vm, v_vl, v_vk, v_vj, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vm, v_vl, v_vk, v_vj, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.tr.const", [v_vl, v_vk, v_vj, v_vi, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.tr.const", [v_vl, v_vk, v_vj, v_vi, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vg, v_vf, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vi, v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.tr.const", [v_vl, v_vk, v_vj, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", []))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vi, v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.tr.const", [v_vl, v_vk, v_vj, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vi, v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", []))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vi, v_vh, v_vg, v_vf, (Nbe.Const ("RedBlackTree.b.const", []))])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", []))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", []))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_vc, v_vb, (Nbe.Const ("RedBlackTree.e.const", [])), v_v])), v_t, v_s, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), v_z, v_y, (Nbe.Const ("RedBlackTree.tr.const", [v_c, v_t, v_s, v_b, (Nbe.Const ("RedBlackTree.r.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))])), v_x, v_w, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_z, v_y, (Nbe.Const ("RedBlackTree.tr.const", [v_c, v_t, v_s, v_b, (Nbe.Const ("RedBlackTree.r.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))])), v_x, v_w, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_z, v_y, (Nbe.Const ("RedBlackTree.tr.const", [v_c, v_t, v_s, v_b, (Nbe.Const ("RedBlackTree.r.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))])), v_x, v_w, (Nbe.Const ("RedBlackTree.e.const", []))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_z, v_y, (Nbe.Const ("RedBlackTree.tr.const", [v_c, v_t, v_s, v_b, (Nbe.Const ("RedBlackTree.r.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))])), v_x, v_w, (Nbe.Const ("RedBlackTree.e.const", []))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_d, v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.r.const", []))])), v_t, v_s, v_b, (Nbe.Const ("RedBlackTree.r.const", []))])), v_x, v_w, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_d, v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_d, v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.r.const", []))])), v_t, v_s, v_b, (Nbe.Const ("RedBlackTree.r.const", []))])), v_x, v_w, (Nbe.Const ("RedBlackTree.e.const", []))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_d, v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_z, v_y, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_c, v_t, v_s, v_b, (Nbe.Const ("RedBlackTree.r.const", []))])), v_x, v_w, (Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, (Nbe.Const ("RedBlackTree.tr.const", [v_vh, v_vg, v_vf, v_ve, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_z, v_y, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_c, v_t, v_s, v_b, (Nbe.Const ("RedBlackTree.r.const", []))])), v_x, v_w, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.r.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_z, v_y, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_c, v_t, v_s, v_b, (Nbe.Const ("RedBlackTree.r.const", []))])), v_x, v_w, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, (Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_z, v_y, (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_c, v_t, v_s, v_b, (Nbe.Const ("RedBlackTree.r.const", []))])), v_x, v_w, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.r.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, (Nbe.Const ("RedBlackTree.e.const", [])), (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_z, v_y, (Nbe.Const ("RedBlackTree.tr.const", [v_c, v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, v_a, (Nbe.Const ("RedBlackTree.r.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_vd, v_vc, v_vb, v_va, (Nbe.Const ("RedBlackTree.b.const", []))])), v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, v_a, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.e.const", [])), v_z, v_y, (Nbe.Const ("RedBlackTree.tr.const", [v_c, v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, v_a, (Nbe.Const ("RedBlackTree.r.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.e.const", [])), v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, v_a, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [(Nbe.Const ("RedBlackTree.tr.const", [v_d, v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.r.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, v_a, (Nbe.Const ("RedBlackTree.r.const", []))]))] = (Nbe.Const ("RedBlackTree.tr.const", [(Nbe.Const ("RedBlackTree.tr.const", [v_d, v_z, v_y, v_c, (Nbe.Const ("RedBlackTree.b.const", []))])), v_t, v_s, (Nbe.Const ("RedBlackTree.tr.const", [v_b, v_x, v_w, v_a, (Nbe.Const ("RedBlackTree.b.const", []))])), (Nbe.Const ("RedBlackTree.r.const", []))]))
| c_RedBlackTree_balance_const [v_a, v_b, v_c, v_d] = (Nbe.Const ("RedBlackTree.balance.const", [v_a, v_b, v_c, v_d]));
|
