equal
deleted
inserted
replaced
19 "s -e>= t" == "(s,t) : eta^=" |
19 "s -e>= t" == "(s,t) : eta^=" |
20 "s ->= t" == "(s,t) : beta^=" |
20 "s ->= t" == "(s,t) : beta^=" |
21 |
21 |
22 primrec free Lambda.dB |
22 primrec free Lambda.dB |
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 (Suc i)" |
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" |
31 appR "s -e> t ==> u@s -e> u@t" |
31 appR "s -e> t ==> u$s -e> u$t" |
32 abs "s -e> t ==> Abs s -e> Abs t" |
32 abs "s -e> t ==> Abs s -e> Abs t" |
33 end |
33 end |
34 |
34 |