16 lines
331 B
Text
16 lines
331 B
Text
|
import logic
|
||
|
|
|
||
|
|
inductive acc1 (A : Type) (R : A → A → Prop) (a : A) : Prop :=
|
||
|
|
intro : ∀ (x : A), (∀ (y : A), R y x → acc1 A R y) → acc1 A R x
|
||
|
|
|
||
|
|
section
|
||
|
|
|
||
|
|
variables (A : Type) (R : A → A → Prop)
|
||
|
|
|
||
|
|
inductive acc2 (a : A) : Prop :=
|
||
|
|
intro : ∀ (x : A), (∀ (y : A), R y x → acc2 y) → acc2 x
|
||
|
|
|
||
|
|
end
|
||
|
|
|
||
|
|
print "done"
|