(*T* \uchapter{Compositionality via Intensionality}\label{sect-comp} *T*)

(*BEGIN-H*)
Load WfTinf_nat.
(*END-H*)

(*T* Although we have simple compositionality theorems for most
temporal operators, there is no counterpart of a similar
form for |leads_to|. In particular, we cannot just replace |ensures| by |leads_to| in
the theorem |ensures_unless_| \linebreak |union|. Let us take a closer
look at this issue: Assume we have components |E| and |E'| and state
predicates |p| and |q| such that |(leads_to E p q)| and |(leads_to E'|\linebreak|p q)| 
holds. Then we cannot infer in general that |(leads_to (Union act E E')| \linebreak
|p q)| holds, since the component |E| may interfere with
|E'| on the execution path from |p| to |q|, e.g. by modifying variables
which the progress of |E'| relies on. Obviously, such an
interference can lead to new possibilities of execution that do not
lead to |q|. The issue of interference in parallel programs is a
well-known problem and the solution proposed in \cite{OrGr76} (see
also the textbook presentation \cite{AptOlderog97}) is based on a notion of {\em interference-free
proof schemes}. This notion is rich of details and syntactic in
nature. It involves a concept of programs annotated with proofs that
seems to be hard to formalize in a rigorous way. 
In this section we propose to use the abstract notion of proof 
offered by the type theory itself according
to the propositions-as-types/proofs-as-objects interpretation to obtain a fully satisfactory
formalization of interference freeness in the general context 
of labeled transition systems. *T*)

(*T* Recall that we are using the logical universe |Prop| of CIC in a
classical way. We have assumed classical axioms such as the law of the
excluded middle, logical extensionality and proof-irrelevance, which
are satisfied under an appropriate classical interpretation.  Since,
we are also interested in treating proofs as informative objects for
the |leads_to| fragment of the temporal logic rather than assuming
proof irrelevance, we move the relevant parts to the universe |Type|
and we exploit the duality of views offered by the
propositions-as-types interpretation, i.e. we use both, the
conventional view of types as data types and the logical view of types
as formulae. In other words, we will now work with {\em two different
logics} simultaneously: (1) the impredicative logic which resides in
the standard propositional universe |Prop| and is axiomatized as a
classical extensional logic with proof irrelevance; and (2) the
predicative logic provided by the |Type| universe hierarchy which is
intuitionistic, intensional and takes proofs seriously. *T*)

(*T* The first step is to migrate from uninformative |leads_to|
assertions to informative |inf_leads_to| assertions by replacing
|Prop| by |Type|. We obtain the following definition: 

\begin{verbatim}
Inductive inf_leads_to [E:view] : s_prop->s_prop->Type :=
  inf_leads_to_basis : (p,q:s_prop)
  (ensures E p q) -> (inf_leads_to E p q)
| inf_leads_to_transitivity : (p,q,r:s_prop)
  (inf_leads_to E p q) -> (inf_leads_to E q r) -> 
  (inf_leads_to E p r)
| inf_leads_to_disjunction : (T:Type)(P:T->s_prop)(q:s_prop)
  ((i:T)(inf_leads_to E (P i) q)) -> 
  (inf_leads_to E (s_ex T P) q).
\end{verbatim}

*T*)

(*BEGIN-H*)

Inductive inf_leads_to [E:view] : s_prop->s_prop->Type :=
  inf_leads_to_basis : (p,q:s_prop)
  (ensures E p q) -> (inf_leads_to E p q)
| inf_leads_to_transitivity : (p,q,r:s_prop)
  (inf_leads_to E p q) -> (inf_leads_to E q r) -> 
  (inf_leads_to E p r)
| inf_leads_to_disjunction : (T:Type)(P:T->s_prop)(p,q:s_prop)
  ((i:T)(inf_leads_to E (P i) q)) -> 
  (everywhere (s_iff p (s_ex T P))) ->
  (inf_leads_to E p q).

(*END-H*)

(*T* We have formally verified that all proofs given so far remain
valid if we replace |leads_to| by |inf_leads_to|. This is a a
consequence of the fact that the |leads_to| fragment of UNITY has been
developed in an entirely constructive way relative to the base
fragment of the logic.  The main purpose of the new definition is to
give assertions |(inf_leads_to sys p q)| in addition to their logical
interpretation the status of a standard inductive data type with
informative elements which are interpreted as proofs.  It is also
important for us that this type resides in |Type| and is therefore not
subject to the restrictions that are enforced by CIC for elimination over
the uninformative universe |Prop|
\cite{PaulinMohring93,HuPa99}. In fact, these
restrictions are essential for our use of |Prop| under a classical
interpretation satisfying the law of the excluded middle and proof
irrelevance. *T*)

(*T* Since |inf_leads_to| is more informative than |leads_to|, we have
the following theorem, which can also be seen as a casting function
from informative proofs to uninformative, i.e. abstract, proofs. *T*)

Theorem inf_leads_to_imp_leads_to : (E:view)
  (p,q:s_prop)(inf_leads_to E p q)->(leads_to E p q).

Intros E p q.
Induction 1.
Intros.
Apply leads_to_basis.
Trivial.
Intros.
Apply leads_to_transitivity with q:=q0.
Trivial.
Trivial.
Intros.
Apply leads_to_disjunction with P:=P.
Trivial.
Trivial.
Qed.

(*T* Of course, the converse implication cannot be proved, due to the
impossibility of generating informative objects from uninformative
objects in CIC, which is consistent with our proof irrelevance
axiom. *T*)

(*T* Exploting the fact that proofs are objects we now define
the compositionality property for proofs of |inf_leads_to|
assertions. We define the property recursively, using the
standard elimination principle |inf_leads_to_rect| that comes 
with |inf_leads_to|. 

\begin{verbatim}
Definition compositional := [E':view][E:view]
  (inf_leads_to_rect E 
    ([u,v:s_prop][l:(inf_leads_to E u v)] Prop)
    (* inf_leads_to_basis *)
    [p,q:s_prop][en:(ensures E p q)]
      (unless E' p q)
    (* inf_leads_to_transitivity *)
    [p,q,r:s_prop]
    [l1:(inf_leads_to E p q)][comp1:Prop]
    [l2:(inf_leads_to E q r)][comp2:Prop]
      (comp1 /\ comp2)
    (* inf_leads_to_disjunction *)
    [T:Type][P:T->s_prop][q:s_prop]
    [L:((i:T)(inf_leads_to E (P i) q))][Comp:(i:T)Prop]
      (i:T)(Comp i)).
\end{verbatim}
*T*)

(*BEGIN-H*)

Definition compositional := [E':view][E:view]
  (inf_leads_to_rect E 
    ([u,v:s_prop][l:(inf_leads_to E u v)] Prop)
    (* inf_leads_to_basis *)
    [p,q:s_prop][en:(ensures E p q)]
      (unless E' p q)
    (* inf_leads_to_transitivity *)
    [p,q,r:s_prop]
    [l1:(inf_leads_to E p q)][comp1:Prop]
    [l2:(inf_leads_to E q r)][comp2:Prop]
      (comp1 /\ comp2)
    (* inf_leads_to_disjunction *)
    [T:Type][P:T->s_prop][p,q:s_prop]
    [L:((i:T)(inf_leads_to E (P i) q))][Comp:(i:T)Prop]
    [E:(everywhere (s_iff p (s_ex T P)))]
      (i:T)(Comp i)).

(*END-H*)

(*T* Given a proof |prf:(inf_leads_to E p' q')| the compositionality
property |(com|\linebreak|positional E' E prf)| requires that each
|ensures| step in |E| is matched by a corresponding |unless| 
step in |E'|, a condition that expresses freedom of interference at the finest
level of granularity. *T*)

(*T* The compositionality theorem that covers
this case is |unless_ensures_union|. The idea of the subsequent
compositionality theorem for |inf_leads_to| is to reduce compositionality at 
the higher level of |inf_leads_to| to compositionality at the lower
level of |ensures| using the aforementioned theorem. *T*)

(*T* In fact, the compositionality theorem for |inf_leads_to| is easy
to prove by induction over the proof |prf|: *T*)

Theorem inf_leads_to_union : (E,E':view)(p,q:s_prop)
  (prf:(inf_leads_to E p q))
  (compositional E' E p q prf)->
  (inf_leads_to (Union act E E') p q).

Intros E E' p q.
Induction prf.
Intros.
Apply inf_leads_to_basis.
Apply ensures_unless_union.
Trivial.

Simpl in H.
Trivial.

Intros.
Apply inf_leads_to_transitivity with q:=q0.
Apply X.
Simpl in H.
Elim H.
Auto.

Apply X0.
Simpl in H.
Elim H.
Auto.

Intros.
Simpl in H.
Apply inf_leads_to_disjunction with P:=P.
Intros.
Apply X.
Apply H.

Trivial.
Qed.

(*BEGIN-H*)

Theorem inf_leads_to_true : (E:view)
  (p:s_prop)(inf_leads_to E p s_true).

Intros.
Apply inf_leads_to_basis.
Apply ensures_true.
Qed.

Theorem inf_leads_to_disjunction_2 : 
  (E:view)(T:Type)(P:T->s_prop)(q:s_prop)
  ((i:T)(inf_leads_to E (P i) q)) -> (inf_leads_to E (s_ex T P) q).

Intros.
Apply (inf_leads_to_disjunction E T P (s_ex T P) q).
Assumption.
Apply s_iff_refl.
Qed.

Theorem inf_leads_to_imp : (E:view)
  (p,q:s_prop)(everywhere (s_imp p q)) -> (inf_leads_to E p q).

Intros.
Apply inf_leads_to_basis.
Apply ensures_imp.
Assumption.
Qed.

Theorem inf_leads_to_refl : (E:view)
  (p:s_prop)(inf_leads_to E p p).

Intros.
Apply inf_leads_to_basis.
Apply ensures_refl.
Qed.

Theorem inf_leads_to_false : (E:view)
  (p:s_prop)(inf_leads_to E s_false p).

Intros.
Apply inf_leads_to_imp.
Apply s_imp_false.
Qed.


Theorem inf_leads_to_implication_l : (E:view)
  (p,q,r:s_prop)(everywhere (s_imp p q)) ->
  (inf_leads_to E q r) -> (inf_leads_to E p r).

Intros.
Apply inf_leads_to_transitivity with q:=q.
Apply inf_leads_to_imp.
Assumption.
Assumption.
Qed.

Theorem inf_leads_to_implication_r : (E:view)
  (p,q,r:s_prop)(everywhere (s_imp q r)) ->
  (inf_leads_to E p q) -> (inf_leads_to E p r).

Intros.
Apply inf_leads_to_transitivity with q:=q.
Assumption.
Apply inf_leads_to_imp.
Assumption.
Qed.

Theorem inf_leads_to_implication : (E:view)
  (p,p',q,q':s_prop)
  (everywhere (s_imp p p'))->
  (everywhere (s_imp q q'))->
  (inf_leads_to E p' q)-> (inf_leads_to E p q').

Intros.
Apply inf_leads_to_transitivity with q:=p'.
Apply inf_leads_to_imp.
Assumption.
Apply inf_leads_to_transitivity with q:=q.
Assumption.
Apply inf_leads_to_imp.
Assumption.
Qed.

Theorem inf_leads_to_weakening : (E:view)
  (p,q,r:s_prop)(inf_leads_to E p q)->(inf_leads_to E p (s_or q r)).

Intros.
Apply inf_leads_to_implication_r with q:=q.
Apply s_imp_or_l.
Assumption.
Qed.

Theorem inf_leads_to_strengthening : (E:view)
  (p,q,r:s_prop)(inf_leads_to E p q)->(inf_leads_to E (s_and p r) q).

Intros.
Apply inf_leads_to_implication_l with q:=p.
Apply s_imp_and_l.
Assumption.
Qed.

Theorem inf_leads_to_subst_r : (E:view)(p,q,q':s_prop)
  (everywhere (s_iff q q'))->
  (inf_leads_to E p q)->(inf_leads_to E p q').

Intros.
Apply inf_leads_to_implication_r with 2:=X.
Apply s_iff_imp.
Trivial.
Qed.

Theorem inf_leads_to_subst_l : (E:view)(p,p',q:s_prop)
  (everywhere (s_iff p p'))->
  (inf_leads_to E p q)->(inf_leads_to E p' q).

Intros.
Apply inf_leads_to_implication_l with 2:=X.
Apply s_iff_imp.
Apply s_iff_sym.
Trivial.
Qed.

Inductive inf_leads_to_pre [E:view;r:s_prop] : s_prop->Type :=
  inf_leads_to_pre_basis : (p:s_prop)
  (ensures E p r) -> (inf_leads_to_pre E r p)
| inf_leads_to_pre_transitivity : (p,q:s_prop)
  (ensures E p q) -> (inf_leads_to_pre E r q) -> (inf_leads_to_pre E r p)
| inf_leads_to_pre_disjunction : (T:Type)(P:T->s_prop)
  ((i:T)(inf_leads_to_pre E r (P i))) -> 
  (p:s_prop)(everywhere (s_iff p (s_ex T P))) -> 
  (inf_leads_to_pre E r p).

Theorem inf_leads_to_pre_imp_leads_to : (E:view)(p,q:s_prop)
  (inf_leads_to_pre E q p) -> (inf_leads_to E p q).

Intros.
Elim X.
Intros.
Constructor 1.
Assumption.

Intros.
Cut (inf_leads_to E p0 q0).
Intros.
Apply inf_leads_to_transitivity with q:=q0.
Assumption.

Assumption.

Constructor 1.
Assumption.

Intros.
Constructor 3 with P:=P.
Assumption.

Assumption.
Qed.

Theorem inf_leads_to_imp_precond : (E:view)(p,q:s_prop)
  (inf_leads_to E p q) -> (inf_leads_to_pre E q p).

Intros.
Elim X.
Intros.
Constructor 1.
Assumption.

Intros.
Elim X0.
Intros.
Constructor 2 with q:=q0.
Assumption.

Assumption.

Intros.
Constructor 2 with q:=q1.
Assumption.

Assumption.

Intros.
Constructor 3 with P:=P.
Assumption.

Assumption.

Intros.
Constructor 3 with P:=P.
Assumption.

Assumption.
Qed.

Theorem inf_leads_to_binary_disjunction : (E:view)
  (p,p',q:s_prop)(inf_leads_to E p q)->(inf_leads_to E p' q)-> 
  (inf_leads_to E (s_or p p') q).

Intros.
Generalize (inf_leads_to_disjunction_2 E bool
             [b:bool]Cases b of
                       true => p
                     | false => p'
                     end q).
Intros.
Cut (inf_leads_to E (s_ex bool [b:bool]Case b of p
                                                    p'
                                                    end) q).
Intros.
Apply inf_leads_to_implication_l
 with q:=(s_ex bool [b:bool]Case b of p
                                      p'
                                      end).
Unfold everywhere s_or s_ex.
Intros.
Unfold s_imp.
Intros.
Elim H.
Intros.
Split with true.
Trivial.

Intros.
Split with false.
Trivial.

Trivial.

Apply X1.
Induction i.
Trivial.

Trivial.
Qed.

Theorem inf_leads_to_ternary_disjunction : 
  (E:view)(p,p',p'',q:s_prop)
  (inf_leads_to E p q)->
  (inf_leads_to E p' q)->(inf_leads_to E p'' q)-> 
  (inf_leads_to E (s_or3 p p' p'') q).

Intros.
Specialize (inf_leads_to_binary_disjunction E ? ? ? X X0).
Intros.
Specialize (inf_leads_to_binary_disjunction E ? ? ? X2 X1).
Intros.
Apply inf_leads_to_implication_l with q:=(s_or (s_or p p') p'').
Unfold everywhere s_imp s_or3 s_or.
Tauto.

Trivial.
Qed.

Theorem inf_leads_to_big_disjunction : (E:view)
  (T:Type)(P,Q:T->s_prop)
  ((i:T)(inf_leads_to E (P i) (Q i)))->
  (inf_leads_to E (s_ex T P) (s_ex T Q)).
 
Intros.
Cut (m:T)(inf_leads_to E (Q m) (s_ex T Q)).
Intros.
Cut (i:T)(inf_leads_to E (P i) (s_ex T Q)).
Intros.
Apply inf_leads_to_disjunction with P:=P.
Assumption.

Apply s_iff_refl.

Intro.
Generalize (X i).
Intros.
Generalize (X0 i).
Intros.
Apply inf_leads_to_transitivity with 1:=X1 2:=X2.

Intros.
Apply inf_leads_to_imp.
Unfold everywhere s_imp s_ex.
Intros.
Split with m.
Assumption.
Qed.

Theorem inf_leads_to_small_disjunction : 
  (E:view)(p,q,p',q':s_prop)
  (inf_leads_to E p p') -> (inf_leads_to E q q')->
  (inf_leads_to E (s_or p q) (s_or p' q')).

Intros.
Generalize (inf_leads_to_big_disjunction E bool
             [b:bool]Cases b of
                       true => p
                     | false => q
                     end
             [b:bool]Cases b of
                       true => p'
                     | false => q'
                     end).
Intros.
Apply inf_leads_to_subst_r
 with q:=(s_ex bool [b:bool]<s_prop>Case b of p'
                                              q'
                                              end).
Unfold everywhere s_iff s_ex s_or.
Intros.
Split.
Intros.
Elim H.
Induction x.
Intros.
Left .
Assumption.

Intros.
Right .
Assumption.

Intros.
Elim H.
Intros.
Split with true.
Assumption.

Intros.
Split with false.
Assumption.

Apply inf_leads_to_subst_l
 with p:=(s_ex bool [b:bool]<s_prop>Case b of p
                                              q
                                              end).
Unfold everywhere s_iff s_ex s_or.
Intros.
Split.
Intros.
Elim H.
Induction x.
Intros.
Left .
Assumption.

Intros.
Right .
Assumption.

Intros.
Elim H.
Intros.
Split with true.
Assumption.

Intros.
Split with false.
Assumption.

Apply X1.
Induction i.
Assumption.

Assumption.
Qed.

Theorem inf_leads_to_impossible : (E:view)
  (p:s_prop)(inf_leads_to E p s_false)->(everywhere (s_not p)).

Intros.
Generalize (inf_leads_to_imp_precond E p s_false X).
Intros.
Clear X.
Elim X0.
Intros.
Apply ensures_false with E:=E.
Assumption.

Intros.
Apply ensures_false with E:=E.
Apply ensures_subst_r with q:=q.
Unfold everywhere s_iff s_false.
Unfold everywhere s_not in H.
Intros.
Generalize (H s).
Intros.
Split.
Unfold not in H0.
Assumption.

Intro.
Elim H1.

Assumption.

Intros.
Unfold everywhere s_not s_ex.
Unfold everywhere s_not in H.
Intros.
Unfold not.
Intros.
Generalize (e s).
Intros.
Elim H1.
Intros.
Generalize (H2 H0).
Intros.
Elim H4.
Intros i.
Intros.
Generalize (H i0 s).
Intros.
Apply H6.
Assumption.
Qed.

Theorem inf_leads_to_cancelation : (E:view)
  (p,q,b,r:s_prop)(inf_leads_to E p (s_or q b))->(inf_leads_to E b r)->
  (inf_leads_to E p (s_or q r)).

Intros.
Cut (inf_leads_to E (s_or q b) (s_or q r)).
Intros.
Apply inf_leads_to_transitivity with q:=(s_or q b).
Assumption.
Assumption.
Apply inf_leads_to_small_disjunction.
Apply (inf_leads_to_refl E).
Assumption.
Qed.

Theorem inf_leads_to_psp : (E:view)
  (p,q,r,b:s_prop)(inf_leads_to E p q)->(unless E r b)->
  (inf_leads_to E (s_and p r) (s_or (s_and q r) b)).

Intros.
Elim X.
Intros.
Constructor 1.
Generalize (ensures_conjunction E r p0 b q0).
Intros.
Generalize (H0 H e).
Intros.
Clear H0.
Apply ensures_subst_l with p:=(s_and r p0).
Unfold everywhere s_iff s_and.
Intros.
Split.
Intros.
Elim H0.
Intros.
Split.
Assumption.

Assumption.

Intros.
Elim H0.
Intros.
Split.
Assumption.

Assumption.

Apply ensures_implication_r
 with q:=(s_or3 (s_and r q0) (s_and p0 b) (s_and b q0)).
Unfold everywhere s_imp s_and s_or s_or3.
Intros.
Elim H0.
Intros.
Elim H2.
Intros.
Left .
Split.
Assumption.

Assumption.

Intros.
Elim H2.
Intros.
Right .
Elim H3.
Intros.
Assumption.

Intros.
Right .
Elim H3.
Intros.
Assumption.

Assumption.

Intros.
Cut (inf_leads_to E (s_and p0 r) (s_or b (s_and q0 r))).
Intros.
Intros.
Generalize (inf_leads_to_cancelation E (s_and p0 r) b (s_and q0 r)
             (s_or (s_and r0 r) b) X2 X1).
Intros.
Apply inf_leads_to_subst_r with q:=(s_or b (s_or (s_and r0 r) b)).
Unfold everywhere s_iff s_or s_and.
Intros.
Split.
Intros.
Elim H0.
Intros.
Right .
Assumption.

Intros.
Assumption.

Intros.
Elim H0.
Intros.
Right .
Left .
Assumption.

Intros.
Left .
Assumption.

Assumption.

Apply inf_leads_to_subst_r with q:=(s_or (s_and q0 r) b).
Unfold everywhere s_iff s_and s_or.
Intros.
Split.
Intros.
Elim H0.
Intros.
Right .
Assumption.

Intros.
Left .
Assumption.

Intros.
Elim H0.
Intros.
Right .
Assumption.

Intros.
Left .
Assumption.

Assumption.

Intros.
Generalize (inf_leads_to_disjunction_2 E T [i:T](s_and (P i) r)
             (s_or (s_and q0 r) b) X0).
Intros.
Apply inf_leads_to_implication_l
 with q:=(s_ex T [i:T](s_and (P i) r)).
Unfold everywhere s_imp s_and s_or.
Intros.
Generalize (e s).
Intros.
Elim H1.
Intros.
Elim H0.
Clear H0.
Intros.
Elim (H2 H0).
Intros.
Split with x.
Auto.

Assumption.
Qed.

Theorem inf_leads_to_stable_conjunction : (E:view)
  (p,q,r:s_prop)(stable E r)->(inf_leads_to E p q)->
  (inf_leads_to E (s_and p r) (s_and q r)).

Intros.
Generalize (inf_leads_to_psp E p q r s_false).
Intros.
Apply inf_leads_to_transitivity with q:=(s_or (s_and q r) s_false).
Apply X0.
Assumption.

Apply stable_imp_unless.
Assumption.

Apply inf_leads_to_imp.
Unfold everywhere s_imp s_or s_and s_false.
Intros.
Elim H0.
Intros.
Auto.

Intro.
Elim H1.
Qed.

Theorem rel_inf_leads_to : (E:view)(p,q,r:s_prop)
  (stable E r)->
  (inf_leads_to E (s_and r p) (s_imp r q))->
  (inf_leads_to E (s_and r p) (s_and r q)).

Intros.
Generalize (inf_leads_to_stable_conjunction E ? ? ? H X).
Clear H X.
Intros.
Apply inf_leads_to_implication with 3:=X.
Unfold everywhere s_imp s_and.
Tauto.
Clear X.
Unfold everywhere s_imp s_and.
Tauto.
Qed.

Theorem ind_invariant_imp_inf_leads_to : (E:view)(p,q,r:s_prop)
  (ind_invariant E p r)->
  (inf_leads_to E p q)->(inf_leads_to E p (s_and q r)).

Intros E p q r I H0.
Unfold ind_invariant in I.
Cut (inf_leads_to E (s_and p r) (s_and q r)).
Intros.
Apply inf_leads_to_subst_l with 2:=X.
Clear H0 X.
Elim I.
Clear I.
log_unfold .
Intros.
Generalize (H s).
Clear H H0.
Tauto.
Apply inf_leads_to_stable_conjunction with 1:=(proj2 ? ? I) 2:=H0.
Qed.

Inductive strong_inf_leads_to [E:view] : s_prop->s_prop->Type :=
  strong_inf_leads_to_basis : (p,q:s_prop)
  (ensures E p q) -> (strong_inf_leads_to E p q)
| strong_inf_leads_to_transitivity : (p,q,r:s_prop)
  (ensures E p q) -> (strong_inf_leads_to E q r) -> 
                        (strong_inf_leads_to E p r)
| strong_inf_leads_to_disjunction : (T:Type)(P:T->s_prop)(p,q:s_prop)
  ((i:T)(strong_inf_leads_to E (P i) q)) -> 
  (everywhere (s_iff p (s_ex T P))) ->
  (strong_inf_leads_to E p q).

Theorem strong_inf_leads_to_imp_inf_leads_to : (E:view)
  (p,q:s_prop)(strong_inf_leads_to E p q)->(inf_leads_to E p q).

Intros.
Elim X.
Intros.
Apply inf_leads_to_basis.
Trivial.

Intros.
Cut (inf_leads_to E p0 q0).
Intros.
Apply inf_leads_to_transitivity with q:=q0.
Trivial.

Trivial.

Apply inf_leads_to_basis.
Trivial.

Intros.
Apply inf_leads_to_disjunction with P:=P.
Intros.
Trivial.

Trivial.
Qed.

Theorem inf_leads_to_imp_strong_inf_leads_to :(E:view)
  (p,q:s_prop)(inf_leads_to E p q)->(strong_inf_leads_to E p q).

Intro.
Intro.
Induction 1.
Intros.
Apply strong_inf_leads_to_basis.
Trivial.

Intros.
Generalize X1.
Clear X1.
Elim i.
Intros.
Apply strong_inf_leads_to_transitivity with q:=q1.
Trivial.

Trivial.

Clear i X0 i0 X.
Intros.
Specialize (X0 X1).
Intros.
Apply X.
Trivial.

Intros.
Apply strong_inf_leads_to_disjunction with P:=P.
Intros.
Apply X1.
Trivial.

Trivial.

Intros.
Apply strong_inf_leads_to_disjunction with P:=P.
Intros.
Apply X0.

Trivial.
Qed.

Transparent strong_inf_leads_to_imp_inf_leads_to.
Transparent inf_leads_to_imp_strong_inf_leads_to.

Theorem inf_leads_to_strong_induction : 
  (IH:view->s_prop->s_prop->Type)(E:view)
  ((p,q:s_prop)(ensures E p q)->(IH E p q))->
  ((p,q,r:s_prop)
   ((ensures E p q)->(inf_leads_to E q r)->
    (IH E p q)->(IH E q r)->(IH E p r)))->
  ((T:Type)(P:T->s_prop)(p,q:s_prop)
   ((i:T)(inf_leads_to E (P i) q))->((i:T)(IH E (P i) q))->
   (everywhere (s_iff p (s_ex T P))) -> (IH E p q))->  
  ((p,q:s_prop)
   (inf_leads_to E p q)->(IH E p q)).

Intros.
Cut (strong_inf_leads_to E p q).
Intros.
Clear X2.
Elim X3.
Trivial.

Intros.
Apply X0 with q:=q0.
Trivial.

Apply strong_inf_leads_to_imp_inf_leads_to.
Trivial.

Apply X.
Trivial.

Trivial.

Intros.
Apply X1 with P:=P.
Intros.
Apply strong_inf_leads_to_imp_inf_leads_to.
Trivial.

Trivial.

Trivial.

Apply inf_leads_to_imp_strong_inf_leads_to.
Trivial.
Qed.

Opaque strong_inf_leads_to_imp_inf_leads_to.
Opaque inf_leads_to_imp_strong_inf_leads_to.

Theorem inf_leads_to_double_induction : 
  (IH:view->s_prop->s_prop->s_prop->s_prop->Type)(E:view)
  ((p,q,p',q':s_prop)
   (ensures E p q)->(inf_leads_to E p' q')->(IH E p q p' q'))->
  ((p,q,p',q':s_prop)
   (inf_leads_to E p q)->(ensures E p' q')->(IH E p q p' q'))->
  ((p,q,r,p',q',r':s_prop)
   ((ensures E p q)->(inf_leads_to E q r)->
    (ensures E p' q')->(inf_leads_to E q' r')->
    (IH E p q p' q')->
    (IH E p q q' r')->(IH E q r p' q')->
    (IH E q r q' r')->
    (IH E p r q' r')->(IH E q r p' r')->
    (IH E p r p' r')))->
  ((T:Type)(P':T->s_prop)(p,q,p',q':s_prop)
    (inf_leads_to E p q)->
    ((i:T)(inf_leads_to E (P' i) q'))->
    ((i:T)(IH E p q (P' i) q'))->
    (everywhere (s_iff p' (s_ex T P')))->
    (IH E p q p' q'))->
  ((T:Type)(P:T->s_prop)(p,q,p',q':s_prop)
    ((i:T)(inf_leads_to E (P i) q))->
    (inf_leads_to E p' q')->
    ((i:T)(IH E (P i) q p' q'))->
    (everywhere (s_iff p (s_ex T P)))->
    (IH E p q p' q'))->  
  ((p,q,p',q':s_prop)
   (inf_leads_to E p q)->(inf_leads_to E p' q')->(IH E p q p' q')).

Intros IH E H0 H1 H2 H3 H4.
Cut (p,q:s_prop)
     (inf_leads_to E p q)
      ->(p',q':s_prop)(inf_leads_to E p' q')->(IH E p q p' q').
Clear H0 H1 H2 H3 H4.
Intros.
Apply X.
Trivial.

Trivial.

Generalize (inf_leads_to_strong_induction
             [E:view]
              [p,q:s_prop]
               (p',q':s_prop)
                (inf_leads_to E p' q')->(IH E p q p' q') E).
Intros.
Apply X.
Intros.
Apply H0.
Trivial.

Trivial.

Intros.
Clear X.
Apply H2 with 1:=H 2:=X2 q':=p'0.
Apply ensures_refl.

Trivial.

Generalize (X3 p'0 p'0).
Intros.
Apply X.
Apply inf_leads_to_refl.

Apply X3.
Trivial.

Apply H1.
Trivial.

Apply ensures_refl.

Apply X4.
Trivial.

Generalize X5.
Generalize p'0 q'0.
Clear X5.
Clear p'0 q'0.
Generalize (inf_leads_to_strong_induction
             [E:view][p'0,q'0:s_prop](IH E p0 r p'0 q'0) E).
Intros.
Apply X.
Intros.
Apply H1.
Apply inf_leads_to_transitivity with q:=q0.
Apply inf_leads_to_basis.
Trivial.

Trivial.

Trivial.

Clear X.
Intros.
Specialize (inf_leads_to_basis E ? ? H5).
Intros.
Specialize (inf_leads_to_transitivity E p1 q1 r0 X8 X).
Intros.
Generalize (X4 p1 r0 X9).
Intros.
Apply (H2 p0 q0 r p1 q1 r0).
Trivial.

Trivial.

Trivial.

Trivial.

Apply H1.
Apply inf_leads_to_basis.
Trivial.

Trivial.

Apply H0.
Trivial.

Trivial.

Apply X4.
Apply inf_leads_to_basis.
Trivial.

Apply X4.
Trivial.

Trivial.

Apply X4.
Trivial.

Clear X.
Intros.
Apply H3 with P':=P.
Apply inf_leads_to_transitivity with q:=q0.
Apply inf_leads_to_basis.
Trivial.

Trivial.

Intros.
Apply X.

Trivial.

Trivial.

Trivial.

Apply X4.
Trivial.

Intros.
Apply H4 with P:=P.
Trivial.

Trivial.

Intros.
Apply X3.
Trivial.

Trivial.

Trivial.

Trivial.
Qed.

Theorem inf_leads_to_symmetric_double_induction : 
  (IH:view->s_prop->s_prop->s_prop->s_prop->Type)
  (E:view)
  ((p,q,p',q':s_prop)(IH E p q p' q')->(IH E p' q' p q))->
  ((p,q,p',q':s_prop)
   (ensures E p q)->(inf_leads_to E p' q')->(IH E p q p' q'))->
  ((p,q,r,p',q',r':s_prop)
   ((ensures E p q)->(inf_leads_to E q r)->
    (ensures E p' q')->(inf_leads_to E q' r')->
    (IH E p q p' q')->
    (IH E p q q' r')->(IH E q r p' q')->
    (IH E q r q' r')->
    (IH E p r q' r')->(IH E q r p' r')->
    (IH E p r p' r')))->
  ((T:Type)(P:T->s_prop)(p,q,p',q':s_prop)
    ((i:T)(inf_leads_to E (P i) q))->
    (inf_leads_to E p' q')->
    ((i:T)(IH E (P i) q p' q'))->
    (everywhere (s_iff p (s_ex T P)))->
    (IH E p q p' q'))->  
  ((p,q,p',q':s_prop)
   (inf_leads_to E p q)->(inf_leads_to E p' q')->(IH E p q p' q')).

Intros.
Apply inf_leads_to_double_induction.
Trivial.

Intros.
Apply X.
Apply X0.
Trivial.

Trivial.

Intros.
Apply X1 with 1:=H 2:=X5 3:=H0 4:=X6.
Trivial.

Trivial.

Trivial.

Trivial.

Trivial.

Trivial.

Intros.
Apply X.
Apply X2 with P:=P'.
Trivial.

Trivial.

Intros.
Apply X.
Auto.

Trivial.

Trivial.

Trivial.

Trivial.
Qed.

Lemma inf_leads_to_simple_conjunction_basis : (E:view)
  (p,q,p',q',r:s_prop)
  (ensures E p q)->
  (inf_leads_to E p' q')->
  (unless E q r)->
  (unless E q' r)->
  (inf_leads_to E (s_and p p') (s_or (s_and q q') r)).

Intros.
Cut (ensures E p q).
Intros ens.
Unfold ensures in H.
Cut (unless E p q).
Cut (transient E (s_and p (s_not q))).
Intros.
Clear H.
Specialize (unless_cancelation E p q r H3 H0).
Intros.
Specialize (inf_leads_to_psp E ? ? ? ? X H).
Intros.
Cut (inf_leads_to E (s_and p p') (s_or (s_and q' (s_or p q)) r)).
Intros.
Specialize (ensures_psp E ? ? ? ? ens H1).
Intros.
Specialize (inf_leads_to_basis E ? ? H4).
Intros.
Generalize (inf_leads_to_implication E (s_and p p') (s_and p p')
             (s_or (s_and q' (s_or p q)) r)
             (s_or (s_or r (s_and q q')) (s_and p q'))).
Intros.
Cut (inf_leads_to E (s_and p p') (s_or (s_and q' (s_or p q)) r))
     ->(inf_leads_to E (s_and p p')
         (s_or (s_or r (s_and q q')) (s_and p q'))).
Intros.
Specialize (X4 X1).
Intros.
Clear X4.
Specialize (inf_leads_to_cancelation E ? ? ? ? X5 X2).
Intros.
Apply (inf_leads_to_implication_r E) with 2:=X4.
Unfold everywhere s_imp s_or s_and.
Clear ens H2 H3 H X0 X1 H4 X2 X3 X4 X5.
Clear X H0 H1.
Tauto.

Intros.
Apply X3.
Apply s_imp_p_p.

Unfold everywhere s_imp s_or s_and.
Clear ens H2 H3 H X0 X1 H4 X2 X3 X4.
Clear X H0 H1.
Tauto.

Apply (inf_leads_to_implication_l E) with q:=(s_and p' (s_or p q)).
Unfold everywhere s_imp s_and s_or.
Clear ens H2 H3 H X0 X1 H4 X2 X3 X4.
Clear X H0 H1.
Tauto.

Trivial.

Apply (inf_leads_to_implication_l E) with q:=(s_and p' (s_or p q)).
Unfold everywhere s_imp s_and s_or.
Clear X H0 H1 ens H2 H3 H X0.
Tauto.

Trivial.

Elim H.
Auto.

Elim H.
Auto.

Trivial.
Qed.

Theorem inf_leads_to_simple_conjunction : (E:view)
  (p,q,p',q',r:s_prop)
  (inf_leads_to E p q)->
  (inf_leads_to E p' q')->
  (unless E q r)->
  (unless E q' r)->
  (inf_leads_to E (s_and p p') (s_or (s_and q q') r)).

Intro.
Intro.
Generalize (inf_leads_to_symmetric_double_induction
             [ppr:view]
              [p,q,p',q':s_prop]
               (r:s_prop)
                (unless E q r)
                 ->(unless E q' r)
                    ->(inf_leads_to E (s_and p p')
                        (s_or (s_and q q') r)) E).
Intros.
Apply X.
Intros.
Specialize (X2 ? H2 H1).
Intros.
Apply inf_leads_to_implication with 3:=X3.
Unfold everywhere s_imp s_and s_and.
Clear X0 X1 H H0 X2 H1 H2 X3.
Clear X.
Tauto.

Unfold everywhere s_imp s_or s_and.
Clear X X0 X1 H H0 X2 H1 H2 X3.
Tauto.

Intros.
Apply inf_leads_to_simple_conjunction_basis.
Trivial.

Trivial.

Trivial.

Trivial.

Intros.
Clear X.
Clear X4 X5 X6.
Specialize (X7 r1 H3 H4).
Specialize (X8 r1 H3 H4).
Specialize (X9 r1 H3 H4).
Clear X7 X8 X9.
Intros.
Cut (unless E p0 q0).
Intros.
Specialize (ensures_conjunction E p0 p'0 q0 q'0 H5 H2).
Intros.
Specialize (inf_leads_to_basis E ? ? H6).
Intros.
Clear H6.
Cut (inf_leads_to E (s_and p'0 q0) (s_or (s_and r0 r') r1)).
Intros.
Specialize (inf_leads_to_ternary_disjunction E (s_and p0 q'0)
             (s_and p'0 q0) (s_and q0 q'0) ? X4 X7 X5).
Intros.
Apply inf_leads_to_transitivity with 1:=X6 2:=X8.

Apply inf_leads_to_implication_l with 2:=X.
Unfold everywhere s_imp s_and.
Clear H1 X2 H2 X3 H3 H4 X X4 X5 H5 X6.
Clear X0 X1 H H0.
Tauto.

Unfold ensures in H1.
Elim H1.
Auto.

Intros.
Clear X.
Cut (i:T)(inf_leads_to E (s_and (P i) p'0) (s_or (s_and q0 q'0) r0)).
Intros.
Apply (inf_leads_to_disjunction E T [i:T](s_and (P i) p'0)).
Trivial.

Unfold everywhere s_iff s_and s_ex.
Unfold everywhere s_iff s_ex in H1.
Intros.
Specialize (H1 s).
Intros.
Elim H4.
Intros.
Split.
Intros.
Elim H7.
Intros.
Elim (H5 H8).
Intros.
Split with x.
Auto.

Intros.
Split.
Apply H6.
Elim H7.
Intros.
Split with x.
Elim H8.
Auto.

Elim H7.
Intros.
Elim H8.
Auto.

Intros.
Apply X4.
Trivial.

Trivial.

Trivial.

Trivial.

Trivial.

Trivial.
Qed.

Theorem inf_leads_to_simple_completion : (E:view)
  (p,q,p',q',r:s_prop)
  (inf_leads_to E p (s_or q r))-> 
  (inf_leads_to E p' (s_or q' r))->
  (unless E q r)->
  (unless E q' r)->
  (inf_leads_to E (s_and p p') (s_or (s_and q q') r)).

Intros.
Specialize (unless_refl E r).
Intros.
Generalize (unless_simple_disjunction E ? ? ? ? H H1).
Intro.
Generalize (unless_simple_disjunction E ? ? ? ? H0 H1).
Intros.
Generalize (inf_leads_to_simple_conjunction E ? ? ? ? ? X X0 H2 H3).
Intros.
Apply inf_leads_to_implication_r with 2:=X1.
Unfold everywhere s_and s_or s_imp.
Clear X X0 H H0 H1 H2 H3 X1.
Tauto.
Qed.

Theorem inf_leads_to_completion_nat : (E:view)
  (b:nat)(P,Q:nat->s_prop)(r:s_prop)
  ((i:nat)(lt i b)->(inf_leads_to E (P i) (s_or (Q i) r)))->
  ((i:nat)(lt i b)->(unless E (Q i) r))->
  (inf_leads_to E (s_all_nat b P) (s_or (s_all_nat b Q) r)).

Intros.
Generalize X.
Generalize H.
Clear X H.
Generalize b.
Clear b.
Induction b.
Intros.
Apply (inf_leads_to_implication_r E) with q:=s_true.
Unfold everywhere s_imp s_true s_or s_all_nat.
Intros.
Left .
Intros.
Elim (lt_n_O i H1).

Apply inf_leads_to_true.

Intros.
Cut (i:nat)(lt i n)->(unless E (Q i) r).
Intros.
Cut (i:nat)(lt i n)->(inf_leads_to E (P i) (s_or (Q i) r)).
Intros.
Specialize (X H0 X1).
Intros.
Clear X.
Cut (inf_leads_to E (P n) (s_or (Q n) r)).
Intros.
Cut (unless E (s_all_nat n Q) r).
Intros.
Cut (unless E (Q n) r).
Intros.
Generalize (inf_leads_to_simple_completion E ? ? ? ? ? X2 X H1 H2).
Intros.
Apply inf_leads_to_implication with 3:=X3.
Unfold everywhere s_imp s_all_nat s_and.
Intros.
Generalize (H3 n).
Intros.
Split.
Intros.
Apply H3.
Apply lt_S.
Trivial.

Apply H4.
Apply lt_n_Sn.

Unfold everywhere s_imp s_or s_and s_all_nat.
Intros.
Elim H3.
Intros.
Left .
Intros.
Elim H4.
Intros.
Specialize (lt_n_Sm_le i n H5).
Intros.
Elim (le_lt_or_eq i n H8).
Intros.
Apply H6.
Trivial.

Intros.
Rewrite H9.
Trivial.

Intros.
Right .
Trivial.

Apply H.
Apply lt_n_Sn.

Apply unless_left_big_conjunction.
Trivial.

Apply X0.
Apply lt_n_Sn.

Intros.
Apply X0.
Apply lt_S.
Trivial.

Intros.
Apply H.
Apply lt_S.
Trivial.
Qed.

Theorem inf_leads_to_completion : (E:view)
  (T:Type)(inf_finite T)->(P,Q:T->s_prop)(r:s_prop)
  ((i:T)(inf_leads_to E (P i) (s_or (Q i) r)))->
  ((i:T)(unless E (Q i) r))->
  (inf_leads_to E (s_all T P) (s_or (s_all T Q) r)).

Intros E T F P Q r.
Unfold finite in F.
Elim F.
Intro b.
Intro.
Clear F.
Unfold inf_card_le in y.
Elim y.
Intro hh.
Intro.
Clear y.
Intros.
Cut (inf_leads_to E (s_all_nat b [n:nat](P (hh n)))
      (s_or (s_all_nat b [n:nat](Q (hh n))) r)).
Intros.
Apply inf_leads_to_implication with 3:=X0.
Unfold everywhere s_imp s_all s_all_nat.
Intros.
Apply H0.

Unfold everywhere s_imp s_or s_all_nat s_all.
Intros.
Elim H0.
Intros.
Left .
Intros.
Elim (y0 t).
Intros.
Elim y.
Intros.
Rewrite <- H3.
Apply H1.
Trivial.

Intros.
Right .
Trivial.

Apply inf_leads_to_completion_nat.
Trivial.

Intros.
Apply H.
Qed.

Theorem inf_leads_to_acc_ind :
  (E:view)(A:Type)(R:A->A->Prop)(P,Q:A->s_prop)
  (IH:(x:A)((y:A)(R y x)->(inf_leads_to E (P y) (Q y)))->
         (inf_leads_to E (P x) (Q x)))
  (i:A)(WfTinf_Acc A R i)->(inf_leads_to E (P i) (Q i)).

Intros.
Elim X.
Intros.
Apply IH.
Trivial.
Qed.

Theorem inf_leads_to_wf_ind :
  (E:view)(A:Type)(R:A->A->Prop)(P,Q:A->s_prop)
  (wf:(WfTinf_well_founded A R))
  (IH:(x:A)((y:A)(R y x)->(inf_leads_to E (P y) (Q y)))->
         (inf_leads_to E (P x) (Q x)))
  (i:A)(inf_leads_to E (P i) (Q i)).

Unfold WfTinf_well_founded.
Intros.
Apply (inf_leads_to_acc_ind E A R P Q IH).
Trivial.
Qed.

Theorem inf_leads_to_induction : (E:view)
  (T:Type)(less:T->T->Prop)(variant:st->T)
  (WfTinf_well_founded T less)->
  (p,q:s_prop)
  ((m:T)(inf_leads_to E (s_and p [s:st] (variant s) == m)
                       (s_or (s_and p [s:st] (less (variant s) m)) q)))->
  (inf_leads_to E p q).

Intros.
Cut (m:T)(inf_leads_to E (s_and p [s:st](variant s)==m) q).
Intros.
Generalize (inf_leads_to_disjunction_2 E T
             [m:T](s_and p [s:st](variant s)==m) q).
Intros.
Generalize (X2 X1).
Intros.
Clear X2.
Apply inf_leads_to_implication_l
 with q:=(s_ex T [m:T](s_and p [s:st](variant s)==m)).
Unfold everywhere s_imp s_ex s_and.
Intros.
Split with (variant s).
Split.
Assumption.

Reflexivity.

Assumption.

Intros.
Apply (inf_leads_to_wf_ind E T less
        [m:T](s_and p [s:st](variant s)==m) [m:T]q X).
Intros.
Generalize (inf_leads_to_disjunction_2 E (sigT ? [y:T](less y x))).
Intros.
Generalize (X2
             [i:(sigT ? [y:T](less y x))]
              (s_and p [s:st](variant s)==(projT1 ? ? i))).
Intros.
Generalize (X3 q).
Intros.
Clear X2 X3.
Cut (inf_leads_to E
      (s_ex (sigT ? [y:T](less y x))
        [i:(sigT ? [y:T](less y x))]
         (s_and p [s:st](variant s)==(projT1 T [y:T](less y x) i))) q).
Intros.
Cut (inf_leads_to E q q).
Intros.
Generalize (inf_leads_to_small_disjunction E
             (s_ex (sigT ? [y:T](less y x))
               [i:(sigT ? [y:T](less y x))]
                (s_and p
                  [s:st](variant s)==(projT1 T [y:T](less y x) i))) q
             q q X2 X3).
Intros.
Apply inf_leads_to_transitivity
 with q:=(s_or
           (s_ex (sigT ? [y:T](less y x))
             [i:(sigT ? [y:T](less y x))]
              (s_and p
                [s:st](variant s)==(projT1 T [y:T](less y x) i))) q).
Generalize (X1 x).
Intros.
Apply inf_leads_to_implication_r
 with q:=(s_or (s_and p [s:st](less (variant s) x)) q).
Unfold everywhere s_imp s_or s_and s_ex.
Intros.
Elim H.
Intros.
Elim H0.
Intros.
Left .
Split with (existT T [y:T](less y x) (variant s) H2).
Split.
Assumption.

Reflexivity.

Intros.
Right .
Assumption.

Apply X0.

Apply inf_leads_to_implication_r with q:=(s_or q q).
Unfold everywhere s_imp s_or.
Intros.
Elim H.
Auto.

Auto.

Assumption.

Apply inf_leads_to_refl.

Apply (inf_leads_to_disjunction_2 E (sigT ? [y:T](less y x))).
Intros.
Elim i.
Intros y' H'.
Generalize (X1 y' H').
Intros.
Auto.
Qed.

Theorem inf_leads_to_var_induction : (E:view)
  (M:var)(less:(var_type M)->(var_type M)->Prop)
  (WfTinf_well_founded (var_type M) less)->
  (p,q:s_prop)
  ((m:(var_type M))(inf_leads_to E (s_and p [s:st] (s M) == m)
                     (s_or (s_and p [s:st] (less (s M) m)) q)))->
  (inf_leads_to E p q).

Intros.
Apply (inf_leads_to_induction E (var_type M) less [s:st](s M)).
Trivial.
Trivial.
Qed.

Theorem inf_leads_to_nat_induction : (E:view)
  (variant:st->nat)
  (p,q:s_prop)
  ((m:nat)(inf_leads_to E (s_and p [s:st] (variant s) = m)
                          (s_or (s_and p [s:st] (lt (variant s) m)) q)))->
  (inf_leads_to E p q).

Intros E v p q.
Intros.
Apply (inf_leads_to_induction E nat lt v inf_lt_wf p q).
Auto.
Intros.
Apply inf_leads_to_implication_l with 2:=(X m).
Unfold everywhere s_imp s_and.
Intros.
Elim H.
Intros.
Split.
Trivial.
Rewrite H1.
Reflexivity.
Qed.

Theorem inf_leads_to_rev_nat_induction : (E:view)
  (variant:st->nat)(maximum:nat)(p,q:s_prop)
  (everywhere (s_imp p [s:st](le (variant s) maximum)))->
  ((m:nat)(le m maximum)->
     (inf_leads_to E (s_and p [s:st] m = (variant s))
                     (s_or (s_and p [s:st] (lt m (variant s))) q)))->
  (inf_leads_to E p q).

Intros.
Apply (inf_leads_to_nat_induction E
        [s:st](minus maximum (variant s)) p q).
Intros.
Elim (le_lt_dec m maximum).
Intros L.
Cut (le (minus maximum m) maximum).
Intros L'.
Generalize (X (minus maximum m) L').
Intros.
Clear X.
Apply inf_leads_to_implication with 3:=X0.
Unfold everywhere s_imp s_and.
Intros.
ECI H0.
Split.
Assumption.

Generalize (H s H0).
Intros.
Generalize (le_plus_minus ? ? H2).
Intros.
Rewrite H3.
Rewrite H1.
Rewrite (plus_sym (variant s) m).
Apply minus_plus.

Unfold everywhere s_imp s_and s_or.
Intros.
ECI H0.
ECI H0.
Left .
Split.
Trivial.

Apply lt_minus_imp_lt_minus.
Trivial.

Apply (H s H0).

Trivial.

Auto.

Intros.
Apply le_minus.

Intros.
Apply (inf_leads_to_implication_l E
        (s_and p [s:st](minus maximum (variant s))=m) s_false
        (s_or (s_and p [s:st](lt (minus maximum (variant s)) m)) q)).
Unfold everywhere s_imp s_and s_false.
Intros.
Generalize (lt_imp_lt_minus_l (variant s) maximum m).
Intros.
GCI H1 y.
ECI H0.
Rewrite H2 in H1.
Apply (lt_n_n ? H1).

Apply inf_leads_to_false.
Qed.

(*END-H*)

(*T* This theorem reduces the proof of an
|inf_leads_to| assertion of a system with components |E| and |E'| to a
corresponding proof for one component 
|prf:(inf_|\linebreak|leads_to E p q)| that satisfies the compositionality property
|(compositional|\linebreak|E' E p q prf)|. Since the proof of |prf|
is typically derived using the standard proof rules for |inf_leads_to| 
that have been given before, the task of proving the
compositionality property can be considerably simplified
by using theorems that state how the compositionality property
behaves under application of the standard proof rules.
In fact, we have proved a theorem for each proof rule that
states a minimal sufficient condition to ensure compositionality
of the resulting |inf_leads_to| assertions. To convey the basic
idea we give a selection of these theorems below. In many cases
these theorems state that proof rules preserve the compositionality property.
The first three theorems correspond directly to the three cases of 
the inductive definition of |compositional|.
*T*)

Theorem inf_leads_to_basis_comp : 
  (E',E:view)(p,q:s_prop)
  (unless E' p q)->
  (en:(ensures E p q))
  (compositional E' E ? ? 
    (inf_leads_to_basis E ? ? en)).

Unfold compositional.
Intros.
Simpl.
Trivial.
Qed.

Theorem inf_leads_to_transitivity_comp : 
  (E',E:view)(p,q,r:s_prop)
  (lto1:(inf_leads_to E p q))
  (lto2:(inf_leads_to E q r))
  (compositional E' E ? ? lto1)->
  (compositional E' E ? ? lto2)->
  (compositional E' E ? ? 
    (inf_leads_to_transitivity E ? ? ? lto1 lto2)).

Unfold compositional.
Intros.
Simpl.
Auto.
Qed.

(*T*
\begin{verbatim}
Theorem inf_leads_to_disjunction_comp :
  (E',E:view)(T:Type)(P:T->s_prop)(p,q:s_prop)
  (lto:((i:T)(inf_leads_to E (P i) q)))
  ((i:T)(compositional E' E ? ? (lto i)))->
  (compositional E' E ? ?
    (inf_leads_to_disjunction E T P (s_ex T P) q lto)).
\end{verbatim}
*T*)

(*BEGIN-H*)

Theorem inf_leads_to_disjunction_comp :
  (E',E:view)(T:Type)(P:T->s_prop)(p,q:s_prop)
  (lto:((i:T)(inf_leads_to E (P i) q)))
  (ev:(everywhere (s_iff p (s_ex T P))))
  ((i:T)(compositional E' E ? ? (lto i)))->
  (compositional E' E ? ?
    (inf_leads_to_disjunction E T P p q lto ev)).

Unfold compositional.
Simpl.
Intros.
Auto.
Qed.

(*END-H*)

Transparent inf_leads_to_refl.

(*BEGIN-H*)

Theorem inf_leads_to_refl_comp :
  (E',E:view)(p:s_prop)
  (compositional E' E ? ? (inf_leads_to_refl E p)).

Unfold inf_leads_to_refl.
Intros.
Apply inf_leads_to_basis_comp.
Apply unless_imp.
Apply s_imp_p_p.
Qed.

Opaque inf_leads_to_refl.

Transparent inf_leads_to_imp.

Theorem inf_leads_to_imp_comp :
  (E',E:view)(p,q:s_prop)
  (ev:(everywhere (s_imp p q)))
  (compositional E' E ? ? (inf_leads_to_imp E p q ev)).

Intros.
Unfold compositional.
Unfold inf_leads_to_imp.
Simpl.
Apply unless_imp.
Trivial.
Qed.

Opaque inf_leads_to_imp.

Transparent inf_leads_to_false.

Theorem inf_leads_to_false_comp :
  (E',E:view)(p:s_prop)
  (compositional E' E ? ? (inf_leads_to_false E p)).

Intros.
Unfold inf_leads_to_false.
Apply inf_leads_to_imp_comp.
Qed.

Opaque inf_leads_to_false.

Transparent inf_leads_to_implication_l.

Theorem inf_leads_to_implication_l_comp :
  (E',E:view)(p,q,r:s_prop)
  (ev:(everywhere (s_imp p q)))
  (lto:(inf_leads_to E q r))
  (compositional E' E ? ? lto)->
  (compositional E' E ? ?
    (inf_leads_to_implication_l E p q r ev lto)).

Unfold inf_leads_to_implication_l.
Intros.
Apply inf_leads_to_transitivity_comp.
Apply inf_leads_to_imp_comp.
Trivial.
Qed.  

Opaque inf_leads_to_implication_l.

Transparent inf_leads_to_implication_r.

Theorem inf_leads_to_implication_r_comp :
  (E',E:view)(p,q,r:s_prop)
  (ev:(everywhere (s_imp q r)))
  (lto:(inf_leads_to E p q))
  (compositional E' E ? ? lto)->
  (compositional E' E ? ?
    (inf_leads_to_implication_r E p q r ev lto)).

Unfold inf_leads_to_implication_r.
Intros.
Apply inf_leads_to_transitivity_comp.
Trivial.
Apply inf_leads_to_imp_comp.
Qed.  

Opaque inf_leads_to_implication_r.

Transparent inf_leads_to_implication.

Theorem inf_leads_to_implication_comp :
  (E',E:view)(p,p',q,q':s_prop)
  (ev1:(everywhere (s_imp p p')))
  (ev2:(everywhere (s_imp q q')))
  (lto:(inf_leads_to E p' q))
  (compositional E' E ? ? lto)->
  (compositional E' E ? ?
    (inf_leads_to_implication E p p' q q' ev1 ev2 lto)).

Intros.
Unfold inf_leads_to_implication.
Apply inf_leads_to_transitivity_comp.
Apply inf_leads_to_imp_comp.
Apply inf_leads_to_transitivity_comp.
Trivial.
Apply inf_leads_to_imp_comp.
Qed.

Opaque inf_leads_to_implication.

Transparent inf_leads_to_subst_l.

Theorem inf_leads_to_subst_l_comp :
  (E',E:view)(p,p',q:s_prop)
  (ev:(everywhere (s_iff p p')))
  (lto:(inf_leads_to E p q))
  (compositional E' E ? ? lto)->
  (compositional E' E ? ?
    (inf_leads_to_subst_l E p p' q ev lto)).

Unfold inf_leads_to_subst_l.
Intros.
Apply inf_leads_to_implication_l_comp.
Trivial.
Qed.  

Opaque inf_leads_to_subst_l.

Transparent inf_leads_to_subst_r.

Theorem inf_leads_to_subst_r_comp :
  (E',E:view)(p,q,q':s_prop)
  (ev:(everywhere (s_iff q q')))
  (lto:(inf_leads_to E p q))
  (compositional E' E ? ? lto)->
  (compositional E' E ? ?
    (inf_leads_to_subst_r E p q q' ev lto)).

Unfold inf_leads_to_subst_r.
Intros.
Apply inf_leads_to_implication_r_comp.
Trivial.
Qed.  

Opaque inf_leads_to_subst_r.

Transparent inf_leads_to_disjunction_2.

Theorem inf_leads_to_disjunction_2_comp :
  (E,E':view)(T:Type)(P:T->s_prop)(q:s_prop)
  (lto:((i:T)(inf_leads_to E (P i) q)))
  ((i:T)(compositional E' E ? ? (lto i)))->
  (compositional E' E ? ? 
    (inf_leads_to_disjunction_2 E T P q lto)).

Unfold inf_leads_to_disjunction_2.
Intros.
Apply inf_leads_to_disjunction_comp.
Trivial.
Qed.

Opaque inf_leads_to_disjunction_2.

Transparent inf_leads_to_big_disjunction.

Theorem inf_leads_to_big_disjunction_comp :
  (E',E:view)(T:Type)(P,Q:T->s_prop)
  (lto:(i:T)(inf_leads_to E (P i) (Q i)))
  ((i:T)(compositional E' E ? ? (lto i)))->
  (compositional E' E ? ? 
    (inf_leads_to_big_disjunction E T P Q lto)).

Intros.
Unfold inf_leads_to_big_disjunction.
Apply inf_leads_to_disjunction_comp.
Intros.
Apply inf_leads_to_transitivity_comp.
Trivial.
Apply inf_leads_to_imp_comp.
Qed.

Opaque inf_leads_to_big_disjunction.

Transparent inf_leads_to_small_disjunction.

(*END-H*)

Theorem inf_leads_to_small_disjunction_comp :
  (E',E:view)(p,q,p',q':s_prop)
  (lto1:(inf_leads_to E p p'))
  (lto2:(inf_leads_to E q q'))
  (compositional E' E ? ? lto1)->
  (compositional E' E ? ? lto2)->
  (compositional E' E ? ? 
    (inf_leads_to_small_disjunction E p q p' q' lto1 lto2)).

Unfold inf_leads_to_small_disjunction.
Intros.
Apply inf_leads_to_subst_r_comp.
Apply inf_leads_to_subst_l_comp.
Apply inf_leads_to_big_disjunction_comp.
Intros.
Elim i.
Simpl.
Trivial.
Simpl.
Trivial.
Qed.

Opaque inf_leads_to_small_disjunction.

Transparent inf_leads_to_cancelation.

Theorem inf_leads_to_cancelation_comp : 
  (E',E:view)
  (p,q,r,b:s_prop)
  (lto1:(inf_leads_to E p (s_or q b)))
  (lto2:(inf_leads_to E b r))
  (compositional E' E ? ? lto1)->
  (compositional E' E ? ? lto2)->
  (compositional E' E ? ? 
    (inf_leads_to_cancelation E p q b r lto1 lto2)).

Intros.
Unfold inf_leads_to_cancelation.
Apply inf_leads_to_transitivity_comp.
Trivial.
Apply inf_leads_to_small_disjunction_comp.
Apply inf_leads_to_refl_comp.
Trivial.
Qed.

Opaque inf_leads_to_cancelation.

Transparent inf_leads_to_psp.

Theorem inf_leads_to_psp_comp : 
  (E',E:view)
  (p,q,r,b:s_prop)
  (lto:(inf_leads_to E p q))
  (un:(unless E r b))
  (compositional E' E ? ? lto)->
  (unless E' r b)->
  (compositional E' E ? ?
    (inf_leads_to_psp E p q r b lto un)).

Intros.
Generalize H.
Elim lto.
Simpl.
Intros.
Generalize (unless_conjunction E' p0 r q0 b H1 H0).
Intros.
Apply unless_implication_r with 2:=H2.
Clear H2.
log_unfold .
Clear H1 e H0 H un lto.
Tauto.

Intros.
Simpl.
Apply inf_leads_to_subst_r_comp.
Apply inf_leads_to_cancelation_comp.
Apply inf_leads_to_subst_r_comp.
Apply H1.
Elim H3.
Auto.

Apply H2.
Elim H3.
Auto.

Intros.
Simpl.
Apply inf_leads_to_implication_l_comp.
Apply inf_leads_to_disjunction_2_comp.
Intros.
Apply H1.
Trivial.
Qed.

Opaque inf_leads_to_psp.

Transparent inf_leads_to_stable_conjunction.

Theorem inf_leads_to_stable_conjunction_comp : 
  (E',E:view)
  (p,q,r:s_prop)
  (st:(stable E r))
  (lto:(inf_leads_to E p q))
  (stable E' r)->
  (compositional E' E ? ? lto)->
  (compositional E' E ? ? 
    (inf_leads_to_stable_conjunction E p q r st lto)).

Intros.
Unfold inf_leads_to_stable_conjunction.
Apply inf_leads_to_transitivity_comp.
Apply inf_leads_to_psp_comp.
Trivial.
Apply stable_imp_unless.
Trivial.
Apply inf_leads_to_imp_comp.
Qed.

Opaque inf_leads_to_stable_conjunction.

Transparent inf_leads_to_acc_ind.

(*BEGIN-H*)

Theorem inf_leads_to_acc_ind_comp :
  (E',E:view)(A:Type)(R:A->A->Prop)(P,Q:A->s_prop)
  (IH:(x:A)((y:A)(R y x)->(inf_leads_to E (P y) (Q y)))->
         (inf_leads_to E (P x) (Q x)))
  ((x:A)(lto:((y:A)(R y x)->(inf_leads_to E (P y) (Q y))))
        ((y:A)(l:(R y x))(compositional E' E ? ? (lto y l)))-> 
      (compositional E' E ? ? (IH x lto)))->
  (i:A)(acc:(WfTinf_Acc A R i))(compositional E' E ? ? 
    (inf_leads_to_acc_ind E A R P Q IH i acc)).

Intros.
Elim acc.
Clear acc.
Clear i.
Intros.
Generalize (H x
             [y:A]
              [r:(R y x)]
               (inf_leads_to_acc_ind E A R P Q IH y (w y r))).
Clear H.
Intros.
Cut (acc:(WfTinf_Acc A R x))
     (IH x
       [y:A][r:(R y x)](inf_leads_to_acc_ind E A R P Q IH y (w y r)))
      ==(inf_leads_to_acc_ind E A R P Q IH x
          (WfTinf_Acc_intro A R x w)).
Intros.
Cut (WfTinf_Acc A R x).
Intros.
Rewrite (H1 X) in H.
Apply H.
Clear H1 H.
Trivial.

Constructor 1.
Trivial.

Intros.
Unfold inf_leads_to_acc_ind.
Simpl.
Trivial.
Qed.

Opaque inf_leads_to_acc_ind.

Transparent inf_leads_to_wf_ind.

Theorem inf_leads_to_wf_ind_comp :
  (E',E:view)(A:Type)(R:A->A->Prop)(P,Q:A->s_prop)
  (wf:(WfTinf_well_founded A R))
  (IH:(x:A)((y:A)(R y x)->(inf_leads_to E (P y) (Q y)))->
         (inf_leads_to E (P x) (Q x)))
  ((x:A)(lto:((y:A)(R y x)->(inf_leads_to E (P y) (Q y))))
        ((y:A)(l:(R y x))(compositional E' E ? ? (lto y l)))-> 
      (compositional E' E ? ? (IH x lto)))->
  (i:A)(compositional E' E ? ? 
    (inf_leads_to_wf_ind E A R P Q wf IH i)).

Intros.
Unfold inf_leads_to_wf_ind.
Apply inf_leads_to_acc_ind_comp.
Trivial.
Qed.

Opaque inf_leads_to_wf_ind.

Transparent inf_leads_to_induction.

(*END-H*)

Theorem inf_leads_to_induction_comp : 
  (E',E:view)
  (T:Type)(less:T->T->Prop)(variant:st->T)
  (wf:(WfTinf_well_founded T less))
  (p,q:s_prop)
  (lto:((m:T)(inf_leads_to E 
     (s_and p [s:st] (variant s) == m)
     (s_or (s_and p [s:st] (less (variant s) m)) q))))
  ((m:T)(compositional E' E ? ? (lto m)))->
  (compositional E' E ? ?
    (inf_leads_to_induction E T less variant wf p q lto)).

Intros.
Unfold inf_leads_to_induction.
Apply inf_leads_to_implication_l_comp.
Apply inf_leads_to_disjunction_2_comp.
Intro.
Apply (inf_leads_to_wf_ind_comp E' E T less
        [m:T](s_and p [s:st](variant s)==m) [m:T]q wf0).
Intros.
Apply inf_leads_to_transitivity_comp.
Apply inf_leads_to_implication_r_comp.
Trivial.

Apply inf_leads_to_implication_r_comp.
Apply inf_leads_to_small_disjunction_comp.
Apply inf_leads_to_disjunction_2_comp.
Intros.
Elim i0.
Intros.
Simpl.
Trivial.

Apply inf_leads_to_refl_comp.
Qed.

Opaque inf_leads_to_induction.

Transparent inf_leads_to_nat_induction.

(*BEGIN-H*)

Theorem inf_leads_to_nat_induction_comp : 
  (E',E:view)
  (variant:st->nat)
  (p,q:s_prop)
  (lto:((m:nat)(inf_leads_to E (s_and p [s:st] (variant s) = m)
                (s_or (s_and p [s:st] (lt (variant s) m)) q))))
  ((m:nat)(compositional E' E ? ? (lto m)))->
  (compositional E' E ? ?
    (inf_leads_to_nat_induction E variant p q lto)).

Intros.
Unfold inf_leads_to_nat_induction.
Apply inf_leads_to_induction_comp.
Intros.
Apply inf_leads_to_implication_l_comp.
Trivial.
Qed.

Opaque inf_leads_to_nat_induction.

Transparent inf_leads_to_rev_nat_induction.

Theorem inf_leads_to_rev_nat_induction_comp : 
  (E',E:view)
  (variant:st->nat)(maximum:nat)
  (p,q:s_prop)
  (ev:(everywhere (s_imp p [s:st](le (variant s) maximum))))
  (lto:((m:nat)(le m maximum)->
           (inf_leads_to E (s_and p [s:st] m = (variant s))
                (s_or (s_and p [s:st] (lt m (variant s))) q))))
  ((m:nat)(L:(le m maximum))(compositional E' E ? ? (lto m L)))->
  (compositional E' E ? ?
    (inf_leads_to_rev_nat_induction E variant maximum p q ev lto)).

Intros.
Unfold inf_leads_to_rev_nat_induction.
Apply inf_leads_to_nat_induction_comp.
Intros.
Elim (le_lt_dec m maximum).
Intros.
Simpl.
Apply inf_leads_to_implication_comp.
Trivial.
Intros.
Simpl.
Apply inf_leads_to_implication_l_comp.
Apply inf_leads_to_false_comp.
Qed.

Opaque inf_leads_to_rev_nat_induction.

(*END-H*)