equal
deleted
inserted
replaced
20 "s ->= t" == "(s,t) : beta^=" |
20 "s ->= t" == "(s,t) : beta^=" |
21 |
21 |
22 primrec |
22 primrec |
23 "free (Var j) i = (j=i)" |
23 "free (Var j) i = (j=i)" |
24 "free (s $ t) i = (free s i | free t i)" |
24 "free (s $ t) i = (free s i | free t i)" |
25 "free (Abs s) i = free s (Suc i)" |
25 "free (Abs s) i = free s (i+1)" |
26 |
26 |
27 inductive eta |
27 inductive eta |
28 intrs |
28 intrs |
29 eta "~free s 0 ==> Abs(s $ Var 0) -e> s[dummy/0]" |
29 eta "~free s 0 ==> Abs(s $ Var 0) -e> s[dummy/0]" |
30 appL "s -e> t ==> s$u -e> t$u" |
30 appL "s -e> t ==> s$u -e> t$u" |