(fun (z) fun (t) fun (f) (z t) f) (fun (x) fun (y) x) |
|
1 2
® |
|
((fun (t) fun (f) (z t) f) {z ¬ fun (x) fun (y) x}) 1 2
º |
(fun (t) fun (f) (fun (x) fun (y) x) t f) |
|
1 2
® |
|
((fun (f) ((fun (x) fun (y) x) t) f) {t ¬ 1}) 2
º |
(fun (f) (fun (x) fun (y) x) 1 f) 2 |
|
® |
|
(((fun (x) fun (y) x) 1) f) {f ¬ 2} º |
|
((fun (y) x) {x ¬ 1}) 2) º |
|
|