1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
Axiom pair : nat -> nat -> nat -> Prop.
Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop).
Axiom plImp : forall k P Q,
pl P Q k -> forall (P':nat -> Prop),
(forall k', P k' -> P' k') -> forall (Q':nat -> Prop),
(forall k', Q k' -> Q' k') ->
pl P' Q' k.
Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
fun k' => exists k, P k k'.
Goal forall s k k' m,
(pl k' (nexists (fun w => (nexists (fun b => pl (pair w w)
(pl (pair s b)
(nexists (fun w0 => (nexists (fun a => pl (pair b w0)
(nexists (fun w1 => (nexists (fun c => pl
(pair a w1) (pl (pair a c) k))))))))))))))) m.
intros.
eapply plImp; [ | eauto | intros ].
2:econstructor.
2:econstructor.
2:eapply plImp; [ | eauto | intros ].
3:eapply plImp; [ | eauto | intros ].
4:econstructor.
4:econstructor.
4:eapply plImp; [ | eauto | intros ].
5:econstructor.
5:econstructor.
5:eauto.
4:eauto.
3:eauto.
2:eauto.
assert (X := 1).
clear X. (* very slow! *)
simpl. (* exception Not_found *)
Admitted.
|
