| Parents |
| wf_relp |
| Constants |
|
$respects
|
(('a  'b) 'a 'b) ('a 'a BOOL) BOOL
|
|
fixed_below
|
(('a 'b) 'a 'b)  ('a 'a BOOL) ('a 'b) 'a BOOL
|
|
fixed_at
|
(('a 'b) 'a 'b) ('a 'a BOOL) ('a 'b) 'a BOOL
|
|
fix
|
(('a 'b) 'a 'b) 'a 'b
|
|
relmap
|
('a 'a BOOL) ('a 'b) 'a 'a 'b BOOL
|
| Fixity |
| Right Infix 240: |
respects |
| Definitions |
|
respects
|
  f r  f respects r  ( g h x ( y tc r y x  g y = h y) f g x = f h x)
|
|
fixed_below
|
f r g x fixed_below f r g x ( y tc r y x f g y = g y)
|
|
fixed_at
|
f r g x fixed_at f r g x fixed_below f r g x  f g x = g x
|
|
fix
|
f r well_founded r f respects r f (fix f) = fix f
|
|
relmap
|
r f relmap r f = ( x y z r y x z = f y)
|
| Theorems |
|
fixed_below_lemma1
|
f r
well_founded r f respects r ( x g y fixed_below f r g x tc r y x fixed_below f r g y)
|
|
fixed_at_lemma1
|
f r
well_founded r f respects r ( x g fixed_below f r g x fixed_at f r (f g) x)
|
|
fixed_at_lemma2
|
f r
well_founded r f respects r ( x g fixed_below f r g x ( y tc r y x fixed_at f r g y))
|
|
fixed_at_lemma3
|
f r
well_founded r f respects r ( x g ( y tc r y x fixed_at f r g y) fixed_below f r g x)
|
|
fixed_below_lemma2
|
f r
well_founded r f respects r ( x g h fixed_below f r g x fixed_below f r h x ( z tc r z x h z = g z))
|
|
fixed_at_lemma4
|
f r
well_founded r f respects r ( g x fixed_at f r g x ( y tc r y x fixed_at f r g y))
|
|
fixed_at_lemma5
|
f r
well_founded r f respects r ( g h x fixed_at f r g x fixed_at f r h x g x = h x)
|
|
fixed_below_lemma3
|
f r
well_founded r f respects r ( x ( y tc r y x ( g fixed_at f r g y)) ( g fixed_below f r g x))
|
|
fixed_below_lemma4
|
r f
well_founded r f respects r ( x g fixed_below f r g x)
|
|
fixed_at_lemma6
|
f r
well_founded r f respects r ( x g fixed_at f r g x)
|
|
fixed_lemma1
|
f r well_founded r f respects r ( x fixed_at f r ( x ( h fixed_at f r h x) x) x)
|
|
fixp_thm1
|
f r well_founded r f respects r ( g f g = g)
|
|
relmap_respect_thm
|
r g ( f g o relmap r f) respects r
|
