# Library Cantor.prelude.AccP

Section restricted_recursion.

Variables (A:Type)(P:AProp)(R:AAProp).

Definition restrict (a b:A):Prop :=
P a R a b P b.

Definition well_founded_P := (a:A), P a Acc restrict a.

Definition P_well_founded_induction_type :
well_founded_P
X : A Type,
( x : A, P x ( y : A,P y R y x X y) X x)
a : A, P a X a.
intros W X H a.
pattern a; eapply well_founded_induction_type with (R:=restrict).
unfold well_founded.
split.
unfold well_founded_P in W.
intros; apply W.
case H0.
auto.
intros; apply H.
auto.
intros; apply X0.
unfold restrict; auto.
auto.
Defined.

End restricted_recursion.

Theorem AccElim3 :
A B C:Type,
(RA:AAProp)
(RB:BBProp)
(RC:CCProp),
(P : A B C Prop),
( x y z,
( (t : A), RA t x
y' z', Acc RB y' Acc RC z'
P t y' z')
( (t : B), RB t y
z', Acc RC z' P x t z')
( (t : C), RC t z P x y t)
P x y z)
x y z, Acc RA x Acc RB y Acc RC z P x y z.
Proof.
intros A B C RA RB RC P H x y z Ax; generalize y z; clear y z.
elim Ax; clear Ax x; intros x _ Hrecx y z Ay; generalize z; clear z.
elim Ay; clear Ay y;
intros y _ Hrecy z Az; elim Az; clear Az z; auto.
Qed.

Theorem accElim3:
(A B C:Set)(RA : A A Prop) (RB : B B Prop)
(RC : C C Prop)(P : A B C Prop),
( x y z ,
( (t : A), RA t x P t y z)
( (t : B), RB t y P x t z)
( (t : C), RC t z P x y t) P x y z)
x y z, Acc RA x Acc RB y Acc RC z P x y z.

intros A B C RA RB RC P H x y z Ax Ay Az.
generalize Ax Ay Az.
pattern x, y, z;
eapply AccElim3 with (RA:=RA)(RB:=RB)(RC:=RC) ;eauto.
intros; apply H.

intros;apply H0; auto.
eapply Acc_inv;eauto.
intros;apply H1; auto.
eapply Acc_inv;eauto.
intros;apply H2; auto.
eapply Acc_inv;eauto.
Qed.