-void subst(char *ident, struct lambda *t1, struct lambda *t2, struct lambda *total)
+bool lambda_ident_eq(struct lambda *t1, struct lambda *t2)
+{
+ switch(t1->which){
+ case lambda_ident:
+ return strcmp(t1->data.identifier.ident, t2->data.identifier.ident) == 0
+ && t1->data.identifier.revision == t2->data.identifier.revision;
+ case lambda_abs:
+ return strcmp(t1->data.abstraction.ident, t2->data.abstraction.ident) == 0
+ && t1->data.abstraction.revision == t2->data.abstraction.revision;
+ default:
+ return false;
+ }
+}
+
+void lambda_alpha(struct lambda *expr, struct lambda *ident)
+{
+ switch(expr->which){
+ case lambda_ident:
+ if(lambda_ident_eq(expr, ident))
+ expr->data.identifier.revision++;
+ break;
+ case lambda_abs:
+ if(!lambda_ident_eq(expr, ident))
+ lambda_alpha(expr->data.abstraction.expr, ident);
+ break;
+ case lambda_app:
+ lambda_alpha(expr->data.application.expr1, ident);
+ lambda_alpha(expr->data.application.expr2, ident);
+ break;
+ }
+
+}
+
+void lambda_beta(struct lambda *ident, struct lambda *t1, struct lambda *t2, struct lambda *total)