Set Implicit Arguments.
From Undecidability.HOU Require Import std.ars.basic.

Set Default Proof Using "Type".

Section StrongNormalisation.

  Variables (X A: Type).
  Variables (R: X X Prop) (S: A A Prop).


  Inductive SN {X} (R: X X Prop) : X Prop :=
  | SNC x : ( y, R x y SN R y) SN R x.

  Lemma SN_ext Q x :
    ( x y, R x y Q x y)
    SN R x SN Q x.
  Proof.
    split; induction 1; econstructor; firstorder.
  Qed.


  Fact SN_unfold x :
    SN R x y, R x y SN R y.
  Proof.
    split.
    - destruct 1 as [x H]. exact H.
    - intros H. constructor. exact H.
  Qed.


  Fact Normal_SN x :
    Normal R x SN R x.
  Proof.
    intros H. constructor. intros y .
    exfalso. eapply H; eauto.
  Qed.


  Fact Normal_star_stops x:
    Normal R x y, star R x y x = y.
  Proof.
    destruct 2; firstorder.
  Qed.


  Fact SN_multiple x :
    SN R x SN (multiple R) x.
  Proof.
    split.
    - induction 1 as [x _ IH].
      constructor. induction 1; eauto.
      apply IHmultiple. intros z % multiple_exp.
      destruct (IH x' H) as [].
      apply . eauto.
    - induction 1 as [x _ IH].
      constructor. intros y . apply IH. eauto.
  Qed.


  Definition morphism (f: X A) :=
     x y, R x y S (f x) (f y).

  Fact SN_morphism f x :
    morphism f SN S (f x) SN R x.
  Proof.
    intros H .
    remember (f x) as a eqn:. revert x .
    induction as [a _ IH]. intros x .
    constructor. intros y % H.
    apply (IH _ ). reflexivity.
  Qed.


  Fact SN_finite_steps:
     ( x, ( y, R x y) Normal R x) x, SN R x y, star R x y & Normal R y.
  Proof.
    intros H; induction 1 as [x IH]. destruct (H x) as [[y ]|].
    + edestruct IH as [z ]; eauto.
    + eexists; eauto.
  Qed.


End StrongNormalisation.