DoTripletAux.v

Require Export Triplet.
Require Export Memory.
Section sect.
Variable n:rNat.
Variable a:(memory n).
Variable f:rNat ->bool.
Variable rMa:(realizeMemory n f a).

Local mEvalEval := (mEvalEval n f a rMa).

Theorem mEvalEvalTriplet:
  (op:rBoolOp)
  (i1, i2, i3:rZ) (Hi1:(rZLe i1 n)) (Hi2:(rZLe i2 n)) (Hi3:(rZLe i3 n))
  (evalTriplet f (Triplet op i1 i2 i3))=
  (evalTriplet
     f (Triplet op (mEval n a i1 Hi1) (mEval n a i2 Hi2) (mEval n a i3 Hi3))).
Intros op i1 i2 i3 Hi1 Hi2 Hi3; Simpl.
Rewrite (mEvalEval i1 Hi1); Auto.
Rewrite (mEvalEval i2 Hi2); Auto.
Rewrite (mEvalEval i3 Hi3); Auto.
Qed.
Hints Resolve mEvalEvalTriplet.

Theorem tContrAddEq:
  (i, j:rZ) (Hi:(rZLe i n)) (Hj:(rZLe j n)) (addEq n a i j Hi Hj)=(tContr n) ->
  (fEval f i)=(negb (fEval f j)).
Intros i j Hi Hj H'.
Inversion rMa.
Rewrite (H i (rZComp j) Hi (rZLeComp n j Hj)); Auto.
Rewrite (fEvalComp f j); Auto.
Rewrite (addEqContr n a i j Hi Hj); Auto.
Qed.

Theorem tSometrAddEq:
  (b:(memory n))
  (i, j, k, l:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (Hk:(rZLe k n))
  (Hl:(rZLe l n))
  (addEq n a i j Hi Hj)=(tSome n b) -> (mEval n b k Hk)=(mEval n b l Hl) ->
  (implb (eqb (fEval f i) (fEval f j)) (eqb (fEval f k) (fEval f l)))=true.
Intros b i j k l Hi Hj Hk Hl addEq0 mEval0; Inversion rMa.
Case (addEqInv n a b i j k l Hi Hj Hk Hl addEq0 mEval0); Intros isE0;
[Idtac |
   Case isE0; Clear isE0; Intros isE0;
    [Case isE0; Clear isE0; Intros isE0 isE1 |
      Case isE0; Clear isE0; Intros isE0;
       [Case isE0; Clear isE0; Intros isE0 isE1 |
         Case isE0; Clear isE0; Intros isE0; Case isE0; Clear isE0;
          Intros isE0 isE1]]]; Auto.
Rewrite (H k l Hk Hl); Auto.
Case (fEval f i); Case (fEval f j); Case (fEval f l); Simpl; Auto.
Rewrite (H j l Hj Hl); Auto; Rewrite (H i k Hi Hk); Auto.
Case (fEval f k); Case (fEval f l); Simpl; Auto.
Rewrite (H j (rZComp l) Hj (rZLeComp n l Hl)); Auto.
Rewrite (H i (rZComp k) Hi (rZLeComp n k Hk)); Auto.
Rewrite (fEvalComp f l); Rewrite (fEvalComp f k); Case (fEval f k);
Case (fEval f l); Simpl; Auto.
Rewrite isE0; Auto.
Rewrite isE1; Auto.
Rewrite (H j k Hj Hk); Auto; Rewrite (H i l Hi Hl); Auto.
Case (fEval f k); Case (fEval f l); Simpl; Auto.
Rewrite (H j (rZComp k) Hj (rZLeComp n k Hk)); Auto.
Rewrite (H i (rZComp l) Hi (rZLeComp n l Hl)); Auto.
Rewrite (fEvalComp f l); Rewrite (fEvalComp f k); Case (fEval f k);
Case (fEval f l); Simpl; Auto.
Rewrite isE0; Auto.
Rewrite isE1; Auto.
Qed.

Theorem tSometrAddEqbis:
  (b:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n)) (addEq n a i j Hi Hj)=(tSome n b) -> (realizeMemory n f b) ->
  (fEval f i)=(fEval f j).
Intros b i j Hi Hj H'1 rMb; Inversion rMb; Auto.
Apply H with Hi := Hi Hj := Hj; Auto.
Apply addEqSome with m1 := a; Auto.
Qed.

Theorem tSometrAddEqter:
  (b:(memory n))
  (i, j:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (addEq n a i j Hi Hj)=(tSome n b) -> (fEval f i)=(fEval f j) ->
  (realizeMemory n f b).
Intros b i j Hi Hj H' H'0.
Apply realizeMemoryDef.
Intros i0 j0 Hi0 Hj0 isE.
Generalize (tSometrAddEq b i j i0 j0 Hi Hj Hi0 Hj0 H' isE).
Rewrite H'0.
Case (fEval f j); Simpl; Case (fEval f i0); Simpl; Case (fEval f j0); Simpl;
Auto.
Qed.

Definition addEqDouble :=
   [p, q, r, s:rZ]
   [Hp:(rZLe p n)] [Hq:(rZLe q n)] [Hr:(rZLe r n)] [Hs:(rZLe s n)]
      Cases (addEq n a p q Hp Hq) of
          (tSome b) => Cases (addEq n b r s Hr Hs) of
                           (tSome c) => (tSome n c)
                          | tContr => (tContr n)
                          | tNop => (tSome n b)
                       end
         | tContr => (tContr n)
         | tNop => (addEq n a r s Hr Hs)
      end.

Theorem tContraddEqDoubleIsEqual:
  (i, j, k, l:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (Hk:(rZLe k n))
  (Hl:(rZLe l n)) (addEqDouble i j k l Hi Hj Hk Hl)=(tContr n) ->
  (orb
     (eqb (fEval f i) (negb (fEval f j)))
     (orb
        (eqb (fEval f k) (negb (fEval f l)))
        (orb
           (andb
              (eqb (fEval f k) (fEval f i)) (eqb (fEval f l) (negb (fEval f j))))
           (orb
              (andb
                 (eqb (fEval f k) (negb (fEval f i)))
                 (eqb (fEval f l) (fEval f j)))
              (orb
                 (andb
                    (eqb (fEval f k) (fEval f j))
                    (eqb (fEval f l) (negb (fEval f i))))
                 (andb
                    (eqb (fEval f k) (negb (fEval f j)))
                    (eqb (fEval f l) (fEval f i))))))))=true.
Inversion rMa.
Intros i j k l Hi Hj Hk Hl; Unfold addEqDouble.
Generalize (refl_equal ? (addEq n a i j Hi Hj));
Pattern 2 3 (addEq n a i j Hi Hj); Case (addEq n a i j Hi Hj).
Intros b H'0; Generalize (refl_equal ? (addEq n b k l Hk Hl));
Pattern 2 3 (addEq n b k l Hk Hl); Case (addEq n b k l Hk Hl).
Intros m H'1 H'2; Inversion H'2.
Intros H'1 H'2.
Cut (mEval n b k Hk)=(mEval n b (rZComp l) (rZLeComp n l Hl));
[Intros H'3 | Rewrite (addEqContr n b k l Hk Hl)]; Auto.
Case (addEqInv n a b i j k (rZComp l) Hi Hj Hk (rZLeComp n l Hl) H'0 H'3);
Intros isE0;
[Idtac |
   Case isE0; Clear isE0; Intros isE0;
    [Case isE0; Clear isE0; Intros isE0 isE1 |
      Case isE0; Clear isE0; Intros isE0;
       [Case isE0; Clear isE0; Intros isE0 isE1 |
         Case isE0; Clear isE0; Intros isE0; Case isE0; Clear isE0;
          Intros isE0 isE1]]]; Auto.
Rewrite (H k (rZComp l) Hk (rZLeComp n l Hl)); Auto.
Rewrite (fEvalComp f l); Case (fEval f i); Simpl; Case (fEval f j); Simpl;
Case (fEval f l); Simpl; Auto.
Rewrite (H i k Hi Hk); Auto; Rewrite (H j (rZComp l) Hj (rZLeComp n l Hl)); Auto.
Rewrite (fEvalComp f l); Case (fEval f k); Case (fEval f l); Simpl; Auto.
Rewrite (H j l Hj Hl); Auto.
Rewrite (H i (rZComp k) Hi (rZLeComp n k Hk)); Auto.
Rewrite (fEvalComp f k); Case (fEval f k); Case (fEval f l); Simpl; Auto.
Rewrite isE0; Auto.
Rewrite isE1; Auto.
Rewrite (mEvalComp n a l Hl (rZLeComp n l Hl)); Auto.
Rewrite (H j k Hj Hk); Auto; Rewrite (H i (rZComp l) Hi (rZLeComp n l Hl)); Auto.
Rewrite (fEvalComp f l); Case (fEval f k); Case (fEval f l); Simpl; Auto.
Rewrite (H j (rZComp k) Hj (rZLeComp n k Hk)); Auto.
Rewrite (H i l Hi Hl); Auto.
Rewrite (fEvalComp f k); Case (fEval f k); Case (fEval f l); Simpl; Auto.
Rewrite isE0; Auto.
Rewrite (mEvalComp n a l Hl (rZLeComp n l Hl)); Auto.
Rewrite (mEvalComp n a k Hk (rZLeComp n k Hk)); Auto.
Intros H'1 H'2; Inversion H'2.
Intros H'1 H'2; Rewrite (tContrAddEq i j Hi Hj); Auto.
Case (fEval f j); Simpl; Case (fEval f k); Simpl; Case (fEval f l); Simpl; Auto.
Intros H'0 H'1; Rewrite (tContrAddEq k l Hk Hl); Auto.
Case (fEval f j); Case (fEval f l); Simpl; Auto with bool.
Qed.

Theorem addEqDoubleNopDef:
  (i, j, k, l:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (Hk:(rZLe k n))
  (Hl:(rZLe l n))
  (mEval n a i Hi)=(mEval n a j Hj) -> (mEval n a k Hk)=(mEval n a l Hl) ->
  (addEqDouble i j k l Hi Hj Hk Hl)=(tNop n).
Intros i j k l Hi Hj Hk Hl H' H'0; Unfold addEqDouble.
Generalize (refl_equal ? (addEq n a i j Hi Hj));
Pattern 2 3 (addEq n a i j Hi Hj); Case (addEq n a i j Hi Hj); Auto.
Intros m H'1; Absurd (mEval n a i Hi)=(mEval n a j Hj); Auto.
Apply addEqDef1 with m2 := m; Auto.
Intros H'1; Absurd (mEval n a i Hi)=(mEval n a j Hj); Auto.
Rewrite (addEqContr n a i j Hi Hj); Auto.
Intros H'1.
Apply nopAddEq; Auto.
Qed.

Theorem addEqDoubleNopIsEqual1:
  (i, j, k, l:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (Hk:(rZLe k n)) (Hl:(rZLe l n)) (addEqDouble i j k l Hi Hj Hk Hl)=(tNop n) ->
  (mEval n a i Hi)=(mEval n a j Hj).
Intros i j k l Hi Hj Hk Hl; Unfold addEqDouble.
Generalize (refl_equal ? (addEq n a i j Hi Hj));
Pattern 2 3 (addEq n a i j Hi Hj); Case (addEq n a i j Hi Hj).
Intros m H'; Generalize (refl_equal ? (addEq n m k l Hk Hl));
Pattern 2 3 (addEq n m k l Hk Hl); Case (addEq n m k l Hk Hl); Auto.
Intros m0 H'0 H'1; Inversion H'1.
Intros H'0 H'1; Inversion H'1.
Intros H'0 H'1; Inversion H'1.
Intros H'0 H'1; Inversion H'1.
Intros H' H'0; Apply addEqNop; Auto.
Qed.

Theorem addEqDoubleIsEqual1:
  (b:(memory n))
  (i, j, k, l:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (Hk:(rZLe k n))
  (Hl:(rZLe l n)) (addEqDouble i j k l Hi Hj Hk Hl)=(tSome n b) ->
  (mEval n b i Hi)=(mEval n b j Hj).
Intros b i j k l Hi Hj Hk Hl; Unfold addEqDouble.
Generalize (refl_equal ? (addEq n a i j Hi Hj));
Pattern 2 3 (addEq n a i j Hi Hj); Case (addEq n a i j Hi Hj).
Intros m H'; Generalize (refl_equal ? (addEq n m k l Hk Hl));
Pattern 2 3 (addEq n m k l Hk Hl); Case (addEq n m k l Hk Hl).
Intros m0 H'0 H'1; Auto.
Apply addEqSomeDef1 with m1 := m i1 := k j1 := l Hi1 := Hk Hj1 := Hl; Auto.
Rewrite <- H'1; Auto.
Apply addEqSome with m1 := a; Auto.
Intros H'0 H'1; Inversion H'1.
Intros H'0 H'1.
Apply addEqSome with m1 := a; Auto.
Rewrite <- H'1; Auto.
Intros H' H'0; Inversion H'0.
Intros H' H'0.
Apply addEqSomeDef1 with m1 := a i1 := k j1 := l Hi1 := Hk Hj1 := Hl; Auto.
Qed.

Theorem addEqDoubleNopIsEqual2:
  (i, j, k, l:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (Hk:(rZLe k n)) (Hl:(rZLe l n)) (addEqDouble i j k l Hi Hj Hk Hl)=(tNop n) ->
  (mEval n a k Hk)=(mEval n a l Hl).
Intros i j k l Hi Hj Hk Hl; Unfold addEqDouble.
Generalize (refl_equal ? (addEq n a i j Hi Hj));
Pattern 2 3 (addEq n a i j Hi Hj); Case (addEq n a i j Hi Hj).
Intros m H'; Generalize (refl_equal ? (addEq n m k l Hk Hl));
Pattern 2 3 (addEq n m k l Hk Hl); Case (addEq n m k l Hk Hl); Auto.
Intros m0 H'0 H'1; Inversion H'1.
Intros H'0 H'1; Inversion H'1.
Intros H'0 H'1; Inversion H'1.
Intros H'0 H'1; Inversion H'1.
Intros H' H'0; Apply addEqNop; Auto.
Qed.

Theorem addEqDoubleIsEqual2:
  (b:(memory n))
  (i, j, k, l:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (Hk:(rZLe k n))
  (Hl:(rZLe l n)) (addEqDouble i j k l Hi Hj Hk Hl)=(tSome n b) ->
  (mEval n b k Hk)=(mEval n b l Hl).
Intros b i j k l Hi Hj Hk Hl; Unfold addEqDouble.
Generalize (refl_equal ? (addEq n a i j Hi Hj));
Pattern 2 3 (addEq n a i j Hi Hj); Case (addEq n a i j Hi Hj).
Intros m H'; Generalize (refl_equal ? (addEq n m k l Hk Hl));
Pattern 2 3 (addEq n m k l Hk Hl); Case (addEq n m k l Hk Hl).
Intros m0 H'0 H'1; Auto.
Apply addEqSome with m1 := m; Auto.
Rewrite <- H'1; Auto.
Intros H'0 H'1; Inversion H'1.
Intros H'0 H'1; Apply addEqNop; Auto.
Inversion H'1; Auto.
Rewrite <- H0; Auto.
Intros H' H'0; Inversion H'0.
Intros H' H'0; Apply addEqSome with m1 := a; Auto.
Qed.

Theorem someaddEqDouble:
  (b:(memory n))
  (i, j, k, l, u, v:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (Hk:(rZLe k n))
  (Hl:(rZLe l n))
  (Hu:(rZLe u n))
  (Hv:(rZLe v n))
  (addEqDouble i j k l Hi Hj Hk Hl)=(tSome n b) ->
  (mEval n b u Hu)=(mEval n b v Hv) ->
  (implb
     (andb (eqb (fEval f i) (fEval f j)) (eqb (fEval f k) (fEval f l)))
     (eqb (fEval f u) (fEval f v)))=true.
Intros b i j k l u v Hi Hj Hk Hl Hu Hv; Unfold addEqDouble.
Generalize (refl_equal ? (addEq n a i j Hi Hj));
Pattern 2 3 (addEq n a i j Hi Hj); Case (addEq n a i j Hi Hj).
Intros c H'0; Generalize (refl_equal ? (addEq n c k l Hk Hl));
Pattern 2 3 (addEq n c k l Hk Hl); Case (addEq n c k l Hk Hl).
Intros d H' H'1 H'2; Inversion H'1.
Rewrite H0 in H'.
Case (addEqInv n c b k l u v Hk Hl Hu Hv H' H'2); Intros isE0;
[Idtac |
   Case isE0; Clear isE0; Intros isE0;
    [Case isE0; Clear isE0; Intros isE0 isE1 |
      Case isE0; Clear isE0; Intros isE0;
       [Case isE0; Clear isE0; Intros isE0 isE1 |
         Case isE0; Clear isE0; Intros isE0; Case isE0; Clear isE0;
          Intros isE0 isE1]]].
Generalize (tSometrAddEq c i j u v Hi Hj Hu Hv H'0 isE0).
Case (fEval f u); Simpl; Case (fEval f v); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Case (fEval f k); Simpl; Case (fEval f l); Simpl; Auto.
Generalize (tSometrAddEq c i j l v Hi Hj Hl Hv H'0 isE1);
Generalize (tSometrAddEq c i j k u Hi Hj Hk Hu H'0 isE0).
Case (fEval f u); Simpl; Case (fEval f v); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Case (fEval f k); Simpl; Case (fEval f l); Simpl; Auto.
Cut (mEval n c k Hk)=(mEval n c (rZComp u) (rZLeComp n u Hu));
[Intros isE2 | Rewrite isE0]; Auto.
Cut (mEval n c l Hl)=(mEval n c (rZComp v) (rZLeComp n v Hv));
[Intros isE3 | Rewrite isE1]; Auto.
Generalize (tSometrAddEq c i j l (rZComp v) Hi Hj Hl (rZLeComp n v Hv) H'0 isE3);
Generalize (tSometrAddEq
               c i j k (rZComp u) Hi Hj Hk (rZLeComp n u Hu) H'0 isE2).
Rewrite (fEvalComp f v); Rewrite (fEvalComp f u); Case (fEval f u); Simpl;
Case (fEval f v); Simpl; Case (fEval f i); Simpl; Case (fEval f j); Simpl;
Case (fEval f k); Simpl; Case (fEval f l); Simpl; Auto.
Generalize (tSometrAddEq c i j l u Hi Hj Hl Hu H'0 isE1);
Generalize (tSometrAddEq c i j k v Hi Hj Hk Hv H'0 isE0).
Case (fEval f u); Simpl; Case (fEval f v); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Case (fEval f k); Simpl; Case (fEval f l); Simpl; Auto.
Cut (mEval n c k Hk)=(mEval n c (rZComp v) (rZLeComp n v Hv));
[Intros isE2 | Rewrite isE0]; Auto.
Cut (mEval n c l Hl)=(mEval n c (rZComp u) (rZLeComp n u Hu));
[Intros isE3 | Rewrite isE1]; Auto.
Generalize (tSometrAddEq c i j l (rZComp u) Hi Hj Hl (rZLeComp n u Hu) H'0 isE3);
Generalize (tSometrAddEq
               c i j k (rZComp v) Hi Hj Hk (rZLeComp n v Hv) H'0 isE2).
Rewrite (fEvalComp f v); Rewrite (fEvalComp f u); Case (fEval f u); Simpl;
Case (fEval f v); Simpl; Case (fEval f i); Simpl; Case (fEval f j); Simpl;
Case (fEval f k); Simpl; Case (fEval f l); Simpl; Auto.
Intros H' H'1; Inversion H'1.
Intros H' H'1 H'2; Inversion H'1.
Rewrite H0 in H'0.
Generalize (tSometrAddEq b i j u v Hi Hj Hu Hv H'0 H'2).
Case (fEval f u); Simpl; Case (fEval f v); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Case (fEval f k); Simpl; Case (fEval f l); Simpl; Auto.
Intros H' H'0; Inversion H'0.
Intros H' H'0 H'1.
Generalize (tSometrAddEq b k l u v Hk Hl Hu Hv H'0 H'1).
Case (fEval f u); Simpl; Case (fEval f v); Simpl; Case (fEval f i); Simpl;
Case (fEval f j); Simpl; Case (fEval f k); Simpl; Case (fEval f l); Simpl; Auto.
Qed.

Theorem mLessAddEqDouble:
  (b:(memory n))
  (i, j, k, l:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (Hk:(rZLe k n))
  (Hl:(rZLe l n)) (addEqDouble i j k l Hi Hj Hk Hl)=(tSome n b) ->(mLess n b a).
Intros b i j k l Hi Hj Hk Hl; Unfold addEqDouble.
Generalize (refl_equal ? (addEq n a i j Hi Hj));
Pattern 2 3 (addEq n a i j Hi Hj); Case (addEq n a i j Hi Hj).
Intros c H'0; Generalize (refl_equal ? (addEq n c k l Hk Hl));
Pattern 2 3 (addEq n c k l Hk Hl); Case (addEq n c k l Hk Hl).
Intros d H' H'1; Inversion H'1.
Apply (mLessTrans n) with y := c; Auto.
Apply addEqMless with i := k j := l Hi := Hk Hj := Hl; Auto.
Rewrite <- H0; Auto.
Apply addEqMless with i := i j := j Hi := Hi Hj := Hj; Auto.
Intros H' H'1; Inversion H'1.
Intros H' H'1; Inversion H'1.
Apply addEqMless with i := i j := j Hi := Hi Hj := Hj; Auto.
Rewrite <- H0; Auto.
Intros H' H'1; Inversion H'1.
Intros H' H'0.
Apply addEqMless with i := k j := l Hi := Hk Hj := Hl; Auto.
Qed.
End sect.

Theorem addEqDoubleSomeInc:
  (n:rNat)
  (m1, m2:(memory n))
  (i, j, k, l:rZ)
  (Hi:(rZLe i n))
  (Hj:(rZLe j n))
  (Hk:(rZLe k n))
  (Hl:(rZLe l n)) (addEqDouble n m1 i j k l Hi Hj Hk Hl)=(tSome n m2) ->
  (inclMem n m1 m2).
Intros n m1 m2 i j k l Hi Hj Hk Hl; Unfold addEqDouble.
Generalize (refl_equal ? (addEq n m1 i j Hi Hj));
Pattern 2 3 (addEq n m1 i j Hi Hj); Case (addEq n m1 i j Hi Hj).
Intros m3 H'0; Generalize (refl_equal ? (addEq n m3 k l Hk Hl));
Pattern 2 3 (addEq n m3 k l Hk Hl); Case (addEq n m3 k l Hk Hl).
Intros m4 H' H'1; Inversion H'1.
Rewrite <- H0; Auto.
Apply (inclMemTrans n) with y := m3; Auto.
Apply addEqSomeIncl with i := i j := j Hi := Hi Hj := Hj; Auto.
Apply addEqSomeIncl with i := k j := l Hi := Hk Hj := Hl; Auto.
Intros H' H'1; Inversion H'1.
Intros H' H'1; Inversion H'1.
Rewrite <- H0.
Apply addEqSomeIncl with i := i j := j Hi := Hi Hj := Hj; Auto.
Intros H' H'0; Inversion H'0.
Intros H' H'0.
Apply addEqSomeIncl with i := k j := l Hi := Hk Hj := Hl; Auto.
Qed.

Theorem addDoubleEqEq:
  (n:rNat)
  (m1, m2:(memory n))
  (i1, i2, j1, j2, k1, k2, l1, l2:rZ)
  (Hi1:(rZLe i1 n))
  (Hi2:(rZLe i2 n))
  (Hj1:(rZLe j1 n))
  (Hj2:(rZLe j2 n))
  (Hk1:(rZLe k1 n))
  (Hk2:(rZLe k2 n))
  (Hl1:(rZLe l1 n))
  (Hl2:(rZLe l2 n))
  (eqMem n m1 m2) ->
  (mEval n m1 i1 Hi1)=(mEval n m1 i2 Hi2) ->
  (mEval n m1 j1 Hj1)=(mEval n m1 j2 Hj2) ->
  (mEval n m1 k1 Hk1)=(mEval n m1 k2 Hk2) ->
  (mEval n m1 l1 Hl1)=(mEval n m1 l2 Hl2) ->
  (eqtMem
     n (addEqDouble n m1 i1 j1 k1 l1 Hi1 Hj1 Hk1 Hl1)
     (addEqDouble n m2 i2 j2 k2 l2 Hi2 Hj2 Hk2 Hl2)).
Intros n m1 m2 i1 i2 j1 j2 k1 k2 l1 l2 Hi1 Hi2 Hj1 Hj2 Hk1 Hk2 Hl1 Hl2 H' H'0
       H'1 H'2 H'3; Unfold addEqDouble.
Cut (eqtMem n (addEq n m1 i1 j1 Hi1 Hj1) (addEq n m2 i2 j2 Hi2 Hj2)).
2:Apply addEqEq; Auto.
Case (addEq n m1 i1 j1 Hi1 Hj1); Auto.
Intros m H'4; Inversion H'4.
Cut (eqtMem n (addEq n m k1 l1 Hk1 Hl1) (addEq n b k2 l2 Hk2 Hl2)).
Case (addEq n m k1 l1 Hk1 Hl1); Auto.
Intros m0 H'5; Inversion H'5.
Apply eqtMemDefSome; Auto.
Intros H'5; Inversion H'5.
Apply eqtMemDefContr; Auto.
Intros H'5; Inversion H'5.
Apply eqtMemDefSome; Auto.
Apply addEqEq; Auto.
Apply eqMeminv1 with m1 := b; Auto.
Apply (eqMemSym n); Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Apply eqMeminv1 with m1 := b; Auto.
Apply (eqMemSym n); Auto.
Apply addEqSomeDef1 with m1 := m2 i1 := i2 j1 := j2 Hi1 := Hi2 Hj1 := Hj2; Auto.
Apply eqMeminv1 with m1 := m1; Auto.
Intros H'5; Inversion H'5.
Apply eqtMemDefContr; Auto.
Intros H'5; Inversion H'5.
Apply addEqEq; Auto.
Qed.
Hints Resolve addDoubleEqEq.

25/03/99, 16:39