well-founded relation

parent 09305f76
...@@ -189,10 +189,22 @@ theory MinMax ...@@ -189,10 +189,22 @@ theory MinMax
end end
*) *)
theory WellFounded
type t
predicate r t t
inductive acc (x: t) =
| acc_x: forall x: t. (forall y: t. r y x -> acc y) -> acc x
axiom well_founded: forall x: t. acc x
end
(* (*
Local Variables: Local Variables:
compile-command: "make -C .. test" compile-command: "make -C .. theories/relations"
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