Some programs make it hang/loop forever

[Boscop]

This program makes it hang forever:

def Z = λs λz (z)
def S = λn λs λz dup #s s1 s2 = s; (s1 (n s2 z))
def pow = λa λb (b a)
(pow (S (S Z)) (S (S Z)))

I added a println!("{}", from_net(&inet)); after the call to rewrite, then it prints:

dup #s e f = c; dup #s j k = h; dup #s p q = n; dup #s u v = s; (λa (a (λb λc λd (e ((b f) d)) (λg λh λi (j ((g k) i)) λ* λl l))) (λm λn λo (p ((m q) o)) (λr λs λt (u ((r v) t)) λ* λw w)))
dup #s d e = b; dup #s i j = g; dup #s o p = m; dup #s t u = r; ((λa λb λc (d ((a e) c)) (λf λg λh (i ((f j) h)) λ* λk k)) (λl λm λn (o ((l p) n)) (λq λr λs (t ((q u) s)) λ* λv v)))
dup #s c j = a; dup #s g h = e; dup #s n o = l; dup #s s t = q; (λa λb (c (((λd λe λf (g ((d h) f)) λ* λi i) j) b)) (λk λl λm (n ((k o) m)) (λp λq λr (s ((p t) r)) λ* λu u)))
dup #s m n = k; dup #s r s = p; dup #s b i = (λj λk λl (m ((j n) l)) (λo λp λq (r ((o s) q)) λ* λt t)); dup #s f g = d; λa (b (((λc λd λe (f ((c g) e)) λ* λh h) i) a))
dup #s l s = j; dup #s p q = n; dup #s b i = λj λk (l (((λm λn λo (p ((m q) o)) λ* λr r) s) k)); dup #s f g = d; λa (b (((λc λd λe (f ((c g) e)) λ* λh h) i) a))
dup #s m t = [b j#s]; dup #s q r = o; dup #s c k = λl (m (((λn λo λp (q ((n r) p)) λ* λs s) t) l)); dup #s g h = e; λa (λb c (((λd λe λf (g ((d h) f)) λ* λi i) λj k) a))
dup #s p q = n; dup #s d k = [(((λm λn λo (p ((m q) o)) λ* λr r) λs l) a) s#s]; dup #s h i = f; dup #s b l = λc (d (((λe λf λg (h ((e i) g)) λ* λj j) k) c)); λa b
dup #s q r = o; dup #s d k = [(((λn λo λp (q ((n r) p)) λ* λs s) λt λl m) a) t#s]; dup #s h i = f; dup #s c m = (d (((λe λf λg (h ((e i) g)) λ* λj j) k) [b l#s])); λa λb c
dup #s g h = e; dup #s p q = n; dup #s c l = ((((λd λe λf (g ((d h) f)) λ* λi i) λj λk l) a) (((λm λn λo (p ((m q) o)) λ* λr r) j) [b k#s])); λa λb c
dup #s f h = d; dup #s o p = m; dup #s c k = (((λd λe (f ((λ* λg g h) e)) λi λj k) a) (((λl λm λn (o ((l p) n)) λ* λq q) i) [b j#s])); λa λb c
dup #s e g = λn λo p; dup #s k l = i; dup #s c p = ((λd (e ((λ* λf f g) d)) a) (((λh λi λj (k ((h l) j)) λ* λm m) n) [b o#s])); λa λb c
dup #s d f = λm λn o; dup #s j k = h; dup #s c o = ((d ((λ* λe e f) a)) (((λg λh λi (j ((g k) i)) λ* λl l) m) [b n#s])); λa λb c
dup #s e h = λo p; dup #s l m = j; dup #s c p = ((λd e ((λ* λf f λg h) a)) (((λi λj λk (l ((i m) k)) λ* λn n) [d g#s]) [b o#s])); λa λb c
dup #s d m = λn o; dup #s h i = f; dup #s c o = (d (((λe λf λg (h ((e i) g)) λ* λj j) [((λ* λk k λl m) a) l#s]) [b n#s])); λa λb c
dup #s e o = p; dup #s i j = g; dup #s c p = (λd e (((λf λg λh (i ((f j) h)) λ* λk k) [((λ* λl l λm λn o) a) m#s]) [b [d n#s]#s])); λa λb c
dup #s d f = e; dup #s c e = d; λa λb c

For better readability I also ran it with lazy-REF nodes, then it prints:

(λa (a (S (S Z))) (S (S Z)))
((S (S Z)) (S (S Z)))
dup #s c d = a; (λa λb (c (((S Z) d) b)) (S (S Z)))
dup #s b c = (S (S Z)); λa (b (((S Z) c) a))
dup #s f g = d; dup #s b c = λd λe (f (((S Z) g) e)); λa (b (((S Z) c) a))
dup #s g h = [b d#s]; dup #s c e = λf (g (((S Z) h) f)); λa (λb c (((S Z) λd e) a))
dup #s d e = [(((S Z) λg f) a) g#s]; dup #s b f = λc (d (((S Z) e) c)); λa b
dup #s d e = [(((S Z) λh λf g) a) h#s]; dup #s c g = (d (((S Z) e) [b f#s])); λa λb c
dup #s c f = ((((S Z) λd λe f) a) (((S Z) d) [b e#s])); λa λb c
dup #s f g = d; dup #s c j = (((λd λe (f ((Z g) e)) λh λi j) a) (((S Z) h) [b i#s])); λa λb c
dup #s e f = λg λh i; dup #s c i = ((λd (e ((Z f) d)) a) (((S Z) g) [b h#s])); λa λb c
dup #s d e = λf λg h; dup #s c h = ((d ((Z e) a)) (((S Z) f) [b g#s])); λa λb c
dup #s e g = λh i; dup #s c i = ((λd e ((Z λf g) a)) (((S Z) [d f#s]) [b h#s])); λa λb c
dup #s d f = λg h; dup #s c h = (d (((S Z) [((Z λe f) a) e#s]) [b g#s])); λa λb c
dup #s e h = i; dup #s c i = (λd e (((S Z) [((Z λf λg h) a) f#s]) [b [d g#s]#s])); λa λb c
dup #s d f = e; dup #s c e = d; λa λb c

The dup label #s is reused between S calls but shouldn't be.

[Boscop]

def Two = 
  dup #s a b = s;
  λsλz(a (b z))

// Doesn't work
def Pow2a = (Two Two)

// Works, with different dup labels
def Pow2b =
  dup #s a b = s;
  dup #f c d = f;
(λsλz(a (b z)) λfλx(c (d x)))

[Boscop]

I think the fix for would be to generate fresh labels when inserting a DEF's body into a term.
(And in my repo with REF nodes, when substituting a REF by the DEF's net, we would have to remap the labels of DUP nodes occurring in that DEF's net, to fresh ones, right?)

But not generating unique fresh DUP labels blindly for a DEF's body, only for each original DUP label, right?
E.g. if we have a term that contains two occurrences to dup label #a, both occurrences should be mapped to the same fresh DUP label when inserting the DEF body into a term, right?
So if we have

def A = λa (dup #a a1 a2 = a; .... dup #a ....)
(A A) // stupid example, I know

then, when inserting A into another term twice, we should get:

((λa (dup #i a1 a2 = a; .... dup #i ....)) (λa (dup #j a1 a2 = a; .... dup #j ....)))

(To preserve the property that the same label occurs twice in each A, but multiple "copies" of A won't conflict.)
Right?