-- File: prelimsOver -- hoort niet in cleaned up versie thuis. -- Wat feitjes over bisimulatie-relaties e.d. -- 1. De reflexieve, symmetrische en transitieve afsluiting is weer een -- bisimulatie-relatie. Path "../lol" Read "lambdaL" Load "logic2" def IsPER := \Y:*s. \R:Y->Y->*p. (@y1,y2:Y. R y1 y2 -> R y2 y1) /\ (@y1,y2,y3:Y. R y1 y2 -> R y2 y3 -> R y1 y3) implicit 1 IsPER def MakePER := \Y:*s. \R:Y->Y->*p. \y1,y2:Y. @E:Y->Y->*p. (@z1,z2:Y. R z1 z2 -> E z1 z2) -> IsPER E -> E y1 y2 : @Y:*s. (Y->Y->*p) -> (Y->Y->*p) implicit 1 MakePER prove MakePER_ext : @Y:*s. @R:Y->Y->*p. @y1,y2:Y. R y1 y2 -> MakePER R y1 y2 prove MakePER_sym : @Y:*s. @R:Y->Y->*p. @y1,y2:Y. MakePER R y1 y2 -> MakePER R y2 y1 prove MakePER_trans : @Y:*s. @R:Y->Y->*p. @y1,y2,y3:Y. MakePER R y1 y2 -> MakePER R y2 y3 -> MakePER R y1 y3 Prove MakePER_PER : @Y:*s.@R:Y->Y->*p. IsPER (MakePER R) Prove IsPER_closed_function : @A,B:*s.@f:A->B.@(~):B->B->*p. IsPER (~) -> IsPER (\a1,a2:A. f a1 ~ f a2) prove IsER__IsPER : @Y:*s. @R:Y->Y->*p. IsER R -> IsPER R prove IsER_is : @A:*s. IsER ((=) A) def MakeER := \Y:*s. \R:Y->Y->*p. \y1,y2:Y. @E:Y->Y->*p. (@z1,z2:Y. R z1 z2 -> E z1 z2) -> IsER E -> E y1 y2 : @Y:*s. (Y->Y->*p) -> (Y->Y->*p) implicit 1 MakeER prove MakeER_ext : @Y:*s. @R:Y->Y->*p. @y1,y2:Y. R y1 y2 -> MakeER R y1 y2 prove MakeER_refl : @Y:*s. @R:Y->Y->*p. @y:Y. MakeER R y y prove MakeER_sym : @Y:*s. @R:Y->Y->*p. @y1,y2:Y. MakeER R y1 y2 -> MakeER R y2 y1 prove MakeER_trans : @Y:*s. @R:Y->Y->*p. @y1,y2,y3:Y. MakeER R y1 y2 -> MakeER R y2 y3 -> MakeER R y1 y3 Prove rel_LeftC : @A,B:*s. @(~):A->B->*p. @a1,a2:A.@b:B. a1~b -> a2~b -> LeftC (~) a1 a2 prove LeftC_sym : @Y,Z:*s. @(~):Y->Z->*p. @y1,y2:Y. LeftC (~) y1 y2 -> LeftC (~) y2 y1 Prove LeftC_trans : @A,B:*s. @(~):A->B->*p. IsZclosed (~) -> @x,y,z:A. LeftC (~) x y -> LeftC (~) y z -> LeftC (~) x z prove LeftC_semirefl : @Y,Z:*s. @(~):Y->Z->*p. @y1,y2:Y. LeftC (~) y1 y2 -> LeftC (~) y1 y1 Prove rel_RightC : @A,B:*s. @(~):A->B->*p. @a:A.@b1,b2:B. a~b1 -> a~b2 -> RightC (~) b1 b2 prove IsZclosed__IsPER_LeftC : @Y,Z:*s. @R:Y->Z->*p. IsZclosed R -> IsPER (LeftC R) prove IsZclosed__IsPER_RightC : @Y,Z:*s. @R:Y->Z->*p. IsZclosed R -> IsPER (RightC R) def MakeZclosed := \Y,Z:*s. \R:Y->Z->*p. \y:Y.\z:Z. @sim:Y->Z->*p. (@y1:Y.@z1:Z. R y1 z1 -> sim y1 z1) -> IsZclosed sim -> sim y z : @Y,Z:*s. (Y->Z->*p) -> (Y->Z->*p) implicit 2 MakeZclosed prove MakeZclosed_ext : @Y,Z:*s. @R:Y->Z->*p. @y:Y.@z:Z. R y z -> MakeZclosed R y z prove MakeZclosed_Zclosed : @Y,Z:*s. @R:Y->Z->*p. IsZclosed (MakeZclosed R) Prove IsERon_is : @A:*s. @P:A->*p. IsERon ((=) A) P -- deelverzameling Def (==>) := \A:*s. \P,Q:A->*p. @x:A. P x -> Q x : @A:*s. (A->*p) -> (A->*p) -> *p Implicit 1 (==>) Prove Inverse_Inverse : @A,B:*s. @R:A->B->*p. Inverse (Inverse R) <===> R -- Deelrelatie Def (===>) := \A,B:*s. \P,Q:A->B->*p. @x:A.@y:B. P x y -> Q x y : @A,B:*s. (A->B->*p) -> (A->B->*p) -> *p Implicit 2 (===>) Def Range := \A,B:*s. \P:A->B->*p. \b:B. Ex a:A. P a b : @A,B:*s. (A->B->*p) -> B->*p Implicit 2 Range Prove IsER_fun_rel : @A,B : *s. @f : B->A. @(~):A->A->*p. IsERon (~) (Image f) -> IsER (\b1,b2:B. f b1 ~ f b2) Prove IsERon_Dom_restr : @A:*s. @(~):A->A->*p. @P:A->*p. IsERon (~) P -> IsERon (\y,z:A. P y /\ y~z /\ P z) P prove LeftC_Inverse : @A,B:*s.@(~):A->B->*p. LeftC (Inverse (~)) <===> RightC (~) prove RightC_Inverse : @A,B:*s.@(~):A->B->*p. RightC (Inverse (~)) <===> LeftC (~) prove IsZclosed_Inverse : @A,B:*s.@(~):A->B->*p. IsZclosed (~) -> IsZclosed (Inverse (~)) Prove IsERon_Dom : @A:*s. @(~):A->A->*p. IsPER (~) -> IsERon (~) (Dom (~))