2. r1: Term List
3. as: (Label
Term) List4.
x:Label. unprime(apply_alist(as;x;x)) = x5. i:
6. i < ||r1||
map(
t.unprime(t);map(t.term_subst(as;t);r1))[i] = map(t.unprime(t);r1)[i] r:rel(), as:(LabelTerm) List.
(x:Label. unprime(apply_alist(as;x;x)) = x) 
rel_unprime(rel_subst(as;r)) = rel_unprime(r)a,b:T List.
||a|| = ||b|| 
(i:. i < ||a|| a[i] = b[i]) a = b
| 1 | 1. name: relname() 2. r1: Term List 3. as: (Label Term) List4. x:Label. unprime(apply_alist(as;x;x)) = x5. i: 6. i < ||r1|| map(t.unprime(t);map(t.term_subst(as;t);r1))[i] = map(t.unprime(t);r1)[i] |
About:
 |  |  |  |  |  |