a transitive closure is transitive

parent 695b4f65
...@@ -93,6 +93,9 @@ theory TransClosure ...@@ -93,6 +93,9 @@ theory TransClosure
inductive relT t t = inductive relT t t =
| BaseTrans : forall x y:t. rel x y -> relT x y | BaseTrans : forall x y:t. rel x y -> relT x y
| StepTrans : forall x y z:t. relT x y -> rel y z -> relT x z | StepTrans : forall x y z:t. relT x y -> rel y z -> relT x z
lemma relT_transitive:
forall x y z: t. relT x y -> relT y z -> relT x z
end end
theory ReflTransClosure theory ReflTransClosure
...@@ -101,6 +104,9 @@ theory ReflTransClosure ...@@ -101,6 +104,9 @@ theory ReflTransClosure
inductive relTR t t = inductive relTR t t =
| BaseTransRefl : forall x:t. relTR x x | BaseTransRefl : forall x:t. relTR x x
| StepTransRefl : forall x y z:t. relTR x y -> rel y z -> relTR x z | StepTransRefl : forall x y z:t. relTR x y -> rel y z -> relTR x z
lemma relTR_transitive:
forall x y z: t. relTR x y -> relTR y z -> relTR x z
end end
(* (*
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment