equal
deleted
inserted
replaced
30 |
30 |
31 translations |
31 translations |
32 "x -1-> y" == "(x,y) : contract" |
32 "x -1-> y" == "(x,y) : contract" |
33 "x ---> y" == "(x,y) : contract^*" |
33 "x ---> y" == "(x,y) : contract^*" |
34 |
34 |
35 inductive "contract" |
35 inductive contract |
36 intrs |
36 intrs |
37 K "K#x#y -1-> x" |
37 K "K#x#y -1-> x" |
38 S "S#x#y#z -1-> (x#z)#(y#z)" |
38 S "S#x#y#z -1-> (x#z)#(y#z)" |
39 Ap1 "x-1->y ==> x#z -1-> y#z" |
39 Ap1 "x-1->y ==> x#z -1-> y#z" |
40 Ap2 "x-1->y ==> z#x -1-> z#y" |
40 Ap2 "x-1->y ==> z#x -1-> z#y" |
50 |
50 |
51 translations |
51 translations |
52 "x =1=> y" == "(x,y) : parcontract" |
52 "x =1=> y" == "(x,y) : parcontract" |
53 "x ===> y" == "(x,y) : parcontract^*" |
53 "x ===> y" == "(x,y) : parcontract^*" |
54 |
54 |
55 inductive "parcontract" |
55 inductive parcontract |
56 intrs |
56 intrs |
57 refl "x =1=> x" |
57 refl "x =1=> x" |
58 K "K#x#y =1=> x" |
58 K "K#x#y =1=> x" |
59 S "S#x#y#z =1=> (x#z)#(y#z)" |
59 S "S#x#y#z =1=> (x#z)#(y#z)" |
60 Ap "[| x=1=>y; z=1=>w |] ==> x#z =1=> y#w" |
60 Ap "[| x=1=>y; z=1=>w |] ==> x#z =1=> y#w" |