Hello. I want to perform a substitution with `copy`

, where the clause added to the context has a body to compute stuff. Up to management of the scope of variables, it would look like this:

```
(copy X Y :- p1 X Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 Y) => copy T T'
```

What do I need to add? (quantifiers / which variables / what order)

Until now I have only used single line `copy`

instances added to the context, where the output is directly linked to the input, without further computations.

Intuitively, for the more complex case, I did the following but it doesn't seem to work:

```
(pi x y\ sigma Tmp1 Tmp2\ copy x y :- p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'
```

(`sigma`

for all variables local to the body, `pi`

so that the clause behaves like a top-level clause)

Did I make a mistake somewhere else, or is this code incorrect?

```
(pi x y\ copy x y :- sigma Tmp1 Tmp2\ p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'
```

or

```
(pi x y Tmp1 Tmp2\ copy x y :- p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'
```

(the latter is faster)

The order of abstractions does not matter

Thanks a lot! :smile:

Last updated: Jun 06 2023 at 23:01 UTC