109 |
109 |
110 consts |
110 consts |
111 Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool" |
111 Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool" |
112 |
112 |
113 definition |
113 definition |
114 is_f :: "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool" |
114 is_f :: "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool" where |
115 "is_f f = (!i1 i2 o1 o2. f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))" |
115 "is_f f = (!i1 i2 o1 o2. f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))" |
116 |
116 |
|
117 definition |
117 is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => |
118 is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => |
118 'b stream => 'c stream => bool" |
119 'b stream => 'c stream => bool" where |
119 "is_net_g f x y == (? z. |
120 "is_net_g f x y == (? z. |
120 <y,z> = f$<x,z> & |
121 <y,z> = f$<x,z> & |
121 (!oy hz. <oy,hz> = f$<x,hz> --> z << hz))" |
122 (!oy hz. <oy,hz> = f$<x,hz> --> z << hz))" |
122 |
123 |
123 is_g :: "('b stream -> 'c stream) => bool" |
124 definition |
|
125 is_g :: "('b stream -> 'c stream) => bool" where |
124 "is_g g == (? f. is_f f & (!x y. g$x = y --> is_net_g f x y))" |
126 "is_g g == (? f. is_f f & (!x y. g$x = y --> is_net_g f x y))" |
125 |
127 |
126 def_g :: "('b stream -> 'c stream) => bool" |
128 definition |
|
129 def_g :: "('b stream -> 'c stream) => bool" where |
127 "def_g g == (? f. is_f f & g = (LAM x. cfst$(f$<x,fix$(LAM k. csnd$(f$<x,k>))>)))" |
130 "def_g g == (? f. is_f f & g = (LAM x. cfst$(f$<x,fix$(LAM k. csnd$(f$<x,k>))>)))" |
128 |
131 |
129 |
132 |
130 (* first some logical trading *) |
133 (* first some logical trading *) |
131 |
134 |