sig str1. type p, q, r o.

module str1. r :- (p => q) => r. r :- q.

Click on a command or tactic to see a detailed view of its use.

Specification "str1". Define ctx : olist -> prop by ctx nil; ctx ((p => q) :: L) := ctx L. Theorem ctx_mem : forall L E, ctx L -> member E L -> E = (p => q). %% This lemma is NOT provable since r depends on q %% which in turn depends on p. Theorem indep : (forall L, ctx L -> {L, p |- p} -> {L |- p}) /\ (forall L, ctx L -> {L, p |- q} -> {L |- q}) /\ (forall L, ctx L -> {L, p |- r} -> {L |- r}).induction on 2 2 2. intros. split. % p is independent of p (which is NOT provable) intros. case H2. case H4. case H3. skip. % Cannot proceed apply ctx_mem to _ H5. case H3. % p is independent of q (again, not provable) intros. case H2. case H4. case H3. apply ctx_mem to _ H5. case H3. % application of IH which is not provable apply IH to _ H6. search. % p is independent of r (not provable) intros. case H2. apply IH2 to _ H3. search. % application of IH1 which is not provable apply IH1 to _ H3. search. case H4. case H3. apply ctx_mem to _ H5. case H3.