From Undecidability.L Require Export LTactics LTerm Functions.Encoding Tactics.Lbeta_nonrefl.
Import L_Notations.
Theorem FirstFixedPoint (s : term) : closed s -> exists t, closed t /\ s t == t.
Proof.
intros cls_s.
pose (A := lam (s (#0 #0))).
pose (t := A A).
exists t. split;[subst t A;Lproc|].
symmetry. cbv. now redStep.
Qed.
Theorem SecondFixedPoint (s : term) : closed s -> exists t, closed t /\ s (enc t) == t.
Proof.
intros cls_s.
pose (A := lam(s ((ext app) #0 ((ext term_enc) #0)))).
pose (t := A (ext A)).
exists t. split;[subst t A;Lproc|].
symmetry. change (enc t) with (ext t).
unfold t. unfold A at 1.
redSteps. now Lsimpl.
Qed.
Goal exists t, closed t /\ t == (enc t).
Proof.
destruct (SecondFixedPoint) with ( s := I) as [t [cls_t A]]. Lproc.
exists t.
split. Lproc. rewrite <- A at 1. clear A. unfold I. now Lsimpl.
Qed.
Import L_Notations.
Theorem FirstFixedPoint (s : term) : closed s -> exists t, closed t /\ s t == t.
Proof.
intros cls_s.
pose (A := lam (s (#0 #0))).
pose (t := A A).
exists t. split;[subst t A;Lproc|].
symmetry. cbv. now redStep.
Qed.
Theorem SecondFixedPoint (s : term) : closed s -> exists t, closed t /\ s (enc t) == t.
Proof.
intros cls_s.
pose (A := lam(s ((ext app) #0 ((ext term_enc) #0)))).
pose (t := A (ext A)).
exists t. split;[subst t A;Lproc|].
symmetry. change (enc t) with (ext t).
unfold t. unfold A at 1.
redSteps. now Lsimpl.
Qed.
Goal exists t, closed t /\ t == (enc t).
Proof.
destruct (SecondFixedPoint) with ( s := I) as [t [cls_t A]]. Lproc.
exists t.
split. Lproc. rewrite <- A at 1. clear A. unfold I. now Lsimpl.
Qed.