DoTripletEq.v
Require Export DoTripletAux.
Require Import Option.
Section sect.
Variable n:rNat.
Variable a:(memory n).
Variable f:rNat ->bool.
Variable rMa:(realizeMemory n f a).
Variables p, q, r:rZ.
Hypothesis Hp:(rZLe p n).
Hypothesis Hq:(rZLe q n).
Hypothesis Hr:(rZLe r n).
Mutual Inductive
doTripletEqP: (tMemory n) ->Prop :=
doTripletEqPpq:
(mEval n a p Hp)=(mEval n a q Hq) ->
(doTripletEqP (addEq n a r rZTrue Hr (rZLeTrue n)))
| doTripletEqPpmq:
(mEval n a p Hp)=(rZComp (mEval n a q Hq)) ->
(doTripletEqP (addEq n a r rZFalse Hr (rZLeFalse n)))
| doTripletEqPpr:
(mEval n a p Hp)=(mEval n a r Hr) ->
(doTripletEqP (addEq n a q rZTrue Hq (rZLeTrue n)))
| doTripletEqPpmr:
(mEval n a p Hp)=(rZComp (mEval n a r Hr)) ->
(doTripletEqP (addEq n a q rZFalse Hq (rZLeFalse n)))
| doTripletEqPqr:
(mEval n a q Hq)=(mEval n a r Hr) ->
(doTripletEqP (addEq n a p rZTrue Hp (rZLeTrue n)))
| doTripletEqPqmr:
(mEval n a q Hq)=(rZComp (mEval n a r Hr)) ->
(doTripletEqP (addEq n a p rZFalse Hp (rZLeFalse n)))
| doTripletEqPpT:
(mEval n a p Hp)=rZTrue ->(doTripletEqP (addEq n a q r Hq Hr))
| doTripletEqPpF:
(mEval n a p Hp)=rZFalse ->
(doTripletEqP (addEq n a q (rZComp r) Hq (rZLeComp n r Hr)))
| doTripletEqPqT:
(mEval n a q Hq)=rZTrue ->(doTripletEqP (addEq n a p r Hp Hr))
| doTripletEqPqF:
(mEval n a q Hq)=rZFalse ->
(doTripletEqP (addEq n a p (rZComp r) Hp (rZLeComp n r Hr)))
| doTripletEqPrT:
(mEval n a r Hr)=rZTrue ->(doTripletEqP (addEq n a p q Hp Hq))
| doTripletEqPrF:
(mEval n a r Hr)=rZFalse ->
(doTripletEqP (addEq n a p (rZComp q) Hp (rZLeComp n q Hq))) .
Local tContrAddEq := (tContrAddEq n a f rMa).
Local tSometrAddEq := (tSometrAddEq n a f rMa).
Local tSometrAddEqbis := (tSometrAddEqbis n a f).
Theorem
tContrRealizeMemoryEq:
(doTripletEqP (tContr n)) ->(evalTriplet f (Triplet rEq p q r))=false.
Intros doT; Inversion doT; Simpl; Auto.
Rewrite (realizeMemoryinv1 n f a p q Hp Hq); Auto.
Rewrite (tContrAddEq r rZTrue Hr (rZLeTrue n)); Auto.
Case (fEval f q); Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a p q Hp Hq); Auto.
Rewrite (tContrAddEq r rZFalse Hr (rZLeFalse n)); Auto.
Case (fEval f q); Simpl; Auto.
Rewrite (realizeMemoryinv1 n f a p r Hp Hr); Auto.
Rewrite (tContrAddEq q rZTrue Hq (rZLeTrue n)); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a p r Hp Hr); Auto.
Rewrite (tContrAddEq q rZFalse Hq (rZLeFalse n)); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinv1 n f a q r Hq Hr); Auto.
Rewrite (tContrAddEq p rZTrue Hp (rZLeTrue n)); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a q r Hq Hr); Auto.
Rewrite (tContrAddEq p rZFalse Hp (rZLeFalse n)); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a p Hp); Auto.
Rewrite (tContrAddEq q r Hq Hr); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvFalse n f a p Hp); Auto.
Rewrite (tContrAddEq q (rZComp r) Hq (rZLeComp n r Hr)); Auto.
Rewrite fEvalComp; Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a q Hq); Auto.
Rewrite (tContrAddEq p r Hp Hr); Auto.
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvFalse n f a q Hq); Auto.
Rewrite (tContrAddEq p (rZComp r) Hp (rZLeComp n r Hr)); Auto.
Rewrite (fEvalComp f r); Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a r Hr); Auto.
Rewrite (tContrAddEq p q Hp Hq); Auto.
Case (fEval f q); Simpl; Auto.
Rewrite (realizeMemoryinvFalse n f a r Hr); Auto.
Rewrite (tContrAddEq p (rZComp q) Hp (rZLeComp n q Hq)); Auto.
Rewrite (fEvalComp f q); Case (fEval f q); Simpl; Auto.
Qed.
Theorem
tSomeRealizeMemoryEqEval:
(b:(memory n)) (realizeMemory n f b) -> (doTripletEqP (tSome n b)) ->
(evalTriplet f (Triplet rEq p q r))=true.
Intros b rMb doT; Inversion rMb; Inversion doT; Simpl; Auto.
Rewrite (realizeMemoryinv1 n f a p q Hp Hq); Auto.
Rewrite (tSometrAddEqbis b r rZTrue Hr (rZLeTrue n)); Auto.
Case (fEval f q); Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a p q Hp Hq); Auto.
Rewrite (tSometrAddEqbis b r rZFalse Hr (rZLeFalse n)); Auto.
Case (fEval f q); Simpl; Auto.
Rewrite (realizeMemoryinv1 n f a p r Hp Hr); Auto.
Rewrite (tSometrAddEqbis b q rZTrue Hq (rZLeTrue n)); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinv2 n f a p r Hp Hr); Auto.
Rewrite (tSometrAddEqbis b q rZFalse Hq (rZLeFalse n)); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinv1 n f a q r Hq Hr); Auto.
Rewrite (tSometrAddEqbis b p rZTrue Hp (rZLeTrue n)); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinv2 n f a q r Hq Hr); Auto.
Rewrite (tSometrAddEqbis b p rZFalse Hp (rZLeFalse n)); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinvTrue n f a p Hp); Auto.
Rewrite (tSometrAddEqbis b q r Hq Hr); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinvFalse n f a p Hp); Auto.
Rewrite (tSometrAddEqbis b q (rZComp r) Hq (rZLeComp n r Hr)); Auto.
Rewrite (fEvalComp f r); Case (fEval f r); Auto.
Rewrite (realizeMemoryinvTrue n f a q Hq); Auto.
Rewrite (tSometrAddEqbis b p r Hp Hr); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinvFalse n f a q Hq); Auto.
Rewrite (tSometrAddEqbis b p (rZComp r) Hp (rZLeComp n r Hr)); Auto.
Rewrite (fEvalComp f r); Case (fEval f r); Auto.
Rewrite (realizeMemoryinvTrue n f a r Hr); Auto.
Rewrite (tSometrAddEqbis b p q Hp Hq); Auto.
Case (fEval f q); Auto.
Rewrite (realizeMemoryinvFalse n f a r Hr); Auto.
Rewrite (tSometrAddEqbis b p (rZComp q) Hp (rZLeComp n q Hq)); Auto.
Rewrite (fEvalComp f q); Case (fEval f q); Auto.
Qed.
Theorem
tNopRealizeMemoryEqEval:
(doTripletEqP (tNop n)) ->(evalTriplet f (Triplet rEq p q r))=true.
Intros doT; Inversion rMa; Inversion doT; Simpl; Auto.
Rewrite (realizeMemoryinv1 n f a p q Hp Hq); Auto.
Rewrite (H r rZTrue Hr (rZLeTrue n)); Auto.
Case (fEval f q); Simpl; Auto.
Rewrite (realizeMemoryinv2 n f a p q Hp Hq); Auto.
Rewrite (H r rZFalse Hr (rZLeFalse n)); Auto.
Case (fEval f q); Simpl; Auto.
Rewrite (realizeMemoryinv1 n f a p r Hp Hr); Auto.
Rewrite (H q rZTrue Hq (rZLeTrue n)); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinv2 n f a p r Hp Hr); Auto.
Rewrite (H q rZFalse Hq (rZLeFalse n)); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinv1 n f a q r Hq Hr); Auto.
Rewrite (H p rZTrue Hp (rZLeTrue n)); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinv2 n f a q r Hq Hr); Auto.
Rewrite (H p rZFalse Hp (rZLeFalse n)); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinvTrue n f a p Hp); Auto.
Rewrite (H q r Hq Hr); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinvFalse n f a p Hp); Auto.
Rewrite (H q (rZComp r) Hq (rZLeComp n r Hr)); Auto.
Rewrite (fEvalComp f r); Case (fEval f r); Auto.
Rewrite (realizeMemoryinvTrue n f a q Hq); Auto.
Rewrite (H p r Hp Hr); Auto.
Case (fEval f r); Auto.
Rewrite (realizeMemoryinvFalse n f a q Hq); Auto.
Rewrite (H p (rZComp r) Hp (rZLeComp n r Hr)); Auto.
Rewrite (fEvalComp f r); Case (fEval f r); Auto.
Rewrite (realizeMemoryinvTrue n f a r Hr); Auto.
Rewrite (H p q Hp Hq); Auto.
Case (fEval f q); Auto.
Rewrite (realizeMemoryinvFalse n f a r Hr); Auto.
Rewrite (H p (rZComp q) Hp (rZLeComp n q Hq)); Auto.
Rewrite (fEvalComp f q); Case (fEval f q); Auto.
Qed.
Theorem
tSomeRealizeMemoryEq:
(b:(memory n))
(doTripletEqP (tSome n b)) -> (evalTriplet f (Triplet rEq p q r))=true ->
(realizeMemory n f b).
Intros b doT Eval0; Apply realizeMemoryDef; Auto.
Intros i j Hi Hj H'.
Generalize Eval0; Clear Eval0; Inversion doT; Simpl; Auto.
Rewrite (realizeMemoryinv1 n f a p q Hp Hq); Auto.
Generalize (tSometrAddEq b r rZTrue i j Hr (rZLeTrue n) Hi Hj H H').
Case (fEval f i); Case (fEval f j); Case (fEval f r); Case (fEval f q); Simpl;
Auto.
Rewrite (realizeMemoryinv2 n f a p q Hp Hq); Auto.
Generalize (tSometrAddEq b r rZFalse i j Hr (rZLeFalse n) Hi Hj H H').
Case (fEval f i); Case (fEval f j); Case (fEval f r); Case (fEval f q); Simpl;
Auto.
Rewrite (realizeMemoryinv1 n f a p r Hp Hr); Auto.
Generalize (tSometrAddEq b q rZTrue i j Hq (rZLeTrue n) Hi Hj H H').
Case (fEval f i); Case (fEval f j); Case (fEval f r); Case (fEval f q); Simpl;
Auto.
Rewrite (realizeMemoryinv2 n f a p r Hp Hr); Auto.
Generalize (tSometrAddEq b q rZFalse i j Hq (rZLeFalse n) Hi Hj H H').
Case (fEval f i); Case (fEval f j); Case (fEval f r); Case (fEval f q); Simpl;
Auto.
Rewrite (realizeMemoryinv1 n f a q r Hq Hr); Auto.
Generalize (tSometrAddEq b p rZTrue i j Hp (rZLeTrue n) Hi Hj H H').
Case (fEval f i); Case (fEval f j); Case (fEval f r); Case (fEval f p); Simpl;
Auto.
Rewrite (realizeMemoryinv2 n f a q r Hq Hr); Auto.
Generalize (tSometrAddEq b p rZFalse i j Hp (rZLeFalse n) Hi Hj H H').
Case (fEval f i); Case (fEval f j); Case (fEval f p); Case (fEval f r); Simpl;
Auto.
Rewrite (realizeMemoryinvTrue n f a p Hp); Auto.
Generalize (tSometrAddEq b q r i j Hq Hr Hi Hj H H').
Case (fEval f i); Case (fEval f j); Case (fEval f q); Case (fEval f r); Simpl;
Auto.
Rewrite (realizeMemoryinvFalse n f a p Hp); Auto.
Generalize (tSometrAddEq b q (rZComp r) i j Hq (rZLeComp n r Hr) Hi Hj H H').
Rewrite (fEvalComp f r); Case (fEval f i); Case (fEval f j); Case (fEval f q);
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a q Hq); Auto.
Generalize (tSometrAddEq b p r i j Hp Hr Hi Hj H H').
Case (fEval f i); Case (fEval f j); Case (fEval f p); Case (fEval f r); Simpl;
Auto.
Rewrite (realizeMemoryinvFalse n f a q Hq); Auto.
Generalize (tSometrAddEq b p (rZComp r) i j Hp (rZLeComp n r Hr) Hi Hj H H').
Rewrite (fEvalComp f r); Case (fEval f i); Case (fEval f j); Case (fEval f p);
Case (fEval f r); Simpl; Auto.
Rewrite (realizeMemoryinvTrue n f a r Hr); Auto.
Generalize (tSometrAddEq b p q i j Hp Hq Hi Hj H H').
Case (fEval f i); Case (fEval f j); Case (fEval f p); Case (fEval f q); Simpl;
Auto.
Rewrite (realizeMemoryinvFalse n f a r Hr); Auto.
Generalize (tSometrAddEq b p (rZComp q) i j Hp (rZLeComp n q Hq) Hi Hj H H').
Rewrite (fEvalComp f q); Case (fEval f i); Case (fEval f j); Case (fEval f p);
Case (fEval f q); Simpl; Auto.
Qed.
Theorem
mLessDoTripletEq:
(b:(memory n)) (doTripletEqP (tSome n b)) ->(mLess n b a).
Intros b doT; Inversion doT.
Apply addEqMless with i := r j := rZTrue Hi := Hr Hj := (rZLeTrue n); Auto.
Apply addEqMless with i := r j := rZFalse Hi := Hr Hj := (rZLeFalse n); Auto.
Apply addEqMless with i := q j := rZTrue Hi := Hq Hj := (rZLeTrue n); Auto.
Apply addEqMless with i := q j := rZFalse Hi := Hq Hj := (rZLeFalse n); Auto.
Apply addEqMless with i := p j := rZTrue Hi := Hp Hj := (rZLeTrue n); Auto.
Apply addEqMless with i := p j := rZFalse Hi := Hp Hj := (rZLeFalse n); Auto.
Apply addEqMless with i := q j := r Hi := Hq Hj := Hr; Auto.
Apply addEqMless with i := q j := (rZComp r) Hi := Hq Hj := (rZLeComp n r Hr);
Auto.
Apply addEqMless with i := p j := r Hi := Hp Hj := Hr; Auto.
Apply addEqMless with i := p j := (rZComp r) Hi := Hp Hj := (rZLeComp n r Hr);
Auto.
Apply addEqMless with i := p j := q Hi := Hp Hj := Hq; Auto.
Apply addEqMless with i := p j := (rZComp q) Hi := Hp Hj := (rZLeComp n q Hq);
Auto.
Qed.
Theorem
doTripletEqSomeInc:
(b:(memory n)) (doTripletEqP (tSome n b)) ->(inclMem n a b).
Intros b doT; Inversion doT; Auto.
Apply addEqSomeIncl with i := r j := rZTrue Hi := Hr Hj := (rZLeTrue n); Auto.
Apply addEqSomeIncl with i := r j := rZFalse Hi := Hr Hj := (rZLeFalse n); Auto.
Apply addEqSomeIncl with i := q j := rZTrue Hi := Hq Hj := (rZLeTrue n); Auto.
Apply addEqSomeIncl with i := q j := rZFalse Hi := Hq Hj := (rZLeFalse n); Auto.
Apply addEqSomeIncl with i := p j := rZTrue Hi := Hp Hj := (rZLeTrue n); Auto.
Apply addEqSomeIncl with i := p j := rZFalse Hi := Hp Hj := (rZLeFalse n); Auto.
Apply addEqSomeIncl with i := q j := r Hi := Hq Hj := Hr; Auto.
Apply addEqSomeIncl with i := q j := (rZComp r) Hi := Hq Hj := (rZLeComp n r Hr);
Auto.
Apply addEqSomeIncl with i := p j := r Hi := Hp Hj := Hr; Auto.
Apply addEqSomeIncl with i := p j := (rZComp r) Hi := Hp Hj := (rZLeComp n r Hr);
Auto.
Apply addEqSomeIncl with i := p j := q Hi := Hp Hj := Hq; Auto.
Apply addEqSomeIncl with i := p j := (rZComp q) Hi := Hp Hj := (rZLeComp n q Hq);
Auto.
Qed.
Definition
doTripletEq :=
Cases (rZDec (mEval n a p Hp) (mEval n a q Hq)) of
left => (Some ? (addEq n a r rZTrue Hr (rZLeTrue n)))
| right => Cases (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))) of
left => (Some ? (addEq n a r rZFalse Hr (rZLeFalse n)))
| right =>
Cases (rZDec (mEval n a p Hp) (mEval n a r Hr)) of
left =>
(Some ? (addEq n a q rZTrue Hq (rZLeTrue n)))
| right =>
Cases (rZDec
(mEval n a p Hp)
(rZComp (mEval n a r Hr))) of
left =>
(Some
? (addEq n a q rZFalse Hq (rZLeFalse n)))
| right =>
Cases (rZDec
(mEval n a q Hq) (mEval n a r Hr)) of
left =>
(Some
?
(addEq
n a p rZTrue Hp (rZLeTrue n)))
| right =>
Cases (rZDec
(mEval n a q Hq)
(rZComp (mEval n a r Hr))) of
left =>
(Some
?
(addEq
n a p rZFalse Hp
(rZLeFalse n)))
| right =>
Cases (rZDec
(mEval n a p Hp)
rZTrue) of
left =>
(Some
?
(addEq
n a q r Hq Hr))
| right =>
Cases (rZDec
(mEval
n a p Hp)
rZFalse) of
left =>
(Some
?
(addEq
n a q
(rZComp
r) Hq
(rZLeComp
n r Hr)))
| right =>
Cases (rZDec
(mEval
n
a
q
Hq)
rZTrue) of
left =>
(Some
?
(addEq
n
a
p
r
Hp
Hr))
| right =>
Cases (rZDec
(mEval
n
a
q
Hq)
rZFalse) of
left
=>
(Some
?
(addEq
n
a
p
(rZComp
r)
Hp
(rZLeComp
n
r
Hr)))
| right
=>
Cases (rZDec
(mEval
n
a
r
Hr)
rZTrue) of
left
=>
(Some
?
(addEq
n
a
p
q
Hp
Hq))
| right
=>
Cases (rZDec
(mEval
n
a
r
Hr)
rZFalse) of
left
=>
(Some
?
(addEq
n
a
p
(rZComp
q)
Hp
(rZLeComp
n
q
Hq)))
| right
=>
(None
?)
end
end
end
end
end
end
end
end
end
end
end
end.
End sect.
Hints Resolve
doTripletEqPpq doTripletEqPpmq doTripletEqPpr doTripletEqPpmr doTripletEqPqr
doTripletEqPqmr doTripletEqPpT doTripletEqPpF doTripletEqPqT doTripletEqPqT
doTripletEqPqF doTripletEqPrT doTripletEqPrF.
Theorem
doTripletEqisP:
(n:rNat)
(a:(memory n))
(b:(tMemory n))
(p, q, r:rZ)
(Hp:(rZLe p n))
(Hq:(rZLe q n)) (Hr:(rZLe r n)) (doTripletEq n a p q r Hp Hq Hr)=(Some ? b) ->
(doTripletEqP n a p q r Hp Hq Hr b).
Intros n a b p q r Hp Hq Hr; Unfold doTripletEq.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a p Hp) rZFalse); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a q Hq) rZFalse); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a r Hr) rZTrue); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Case (rZDec (mEval n a r Hr) rZFalse); Intros Eq0;
[Intros EqS; Inversion EqS | Clear Eq0]; Auto.
Intros H'; Inversion H'.
Qed.
Theorem
doTripletEqisNotP:
(n:rNat)
(a:(memory n))
(b:(tMemory n))
(p, q, r:rZ)
(Hp:(rZLe p n))
(Hq:(rZLe q n))
(Hr:(rZLe r n)) (doTripletEq n a p q r Hp Hq Hr)=(None (tMemory n)) ->
~ (doTripletEqP n a p q r Hp Hq Hr b).
Intros n a b p q r Hp Hq Hr; Unfold doTripletEq.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eq0;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eq1;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eq2;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eq3;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eq4;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eq5;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eq6;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a p Hp) rZFalse); Intros Eq7;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eq8;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a q Hq) rZFalse); Intros Eq9;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a r Hr) rZTrue); Intros Eq10;
[Intros EqS; Inversion EqS | Idtac].
Case (rZDec (mEval n a r Hr) rZFalse); Intros Eq11;
[Intros EqS; Inversion EqS | Idtac].
Intros H'; Red; Intros H'0; Inversion H'0; Auto.
Qed.
Theorem
doTripletEqNopNop:
(n:rNat)
(a:(memory n))
(b:(tMemory n))
(p, q, r:rZ)
(Hp:(rZLe p n))
(Hq:(rZLe q n))
(Hr:(rZLe r n))
(doTripletEqP n a p q r Hp Hq Hr b) ->
(doTripletEq n a p q r Hp Hq Hr)=(Some ? (tNop n)) ->b=(tNop n).
Intros n a b p q r Hp Hq Hr H'; Elim H'; Auto.
Intros Eqp H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp'; Auto.
Intros H'1; Inversion H'1; Auto.
Case Eqp'; Auto.
Intros Eqp H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp'; Auto.
Absurd (mEval n a p Hp)=(rZComp (mEval n a q Hq)); Auto.
Rewrite <- Eqp'; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp''; Auto.
Intros H'1; Inversion H'1; Auto.
Case Eqp''; Auto.
Intros Eqp H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp'; Auto.
Intros H'0; Inversion H'0.
Rewrite <- Eqp'; Rewrite Eqp; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp''; Auto.
Intros H'0; Inversion H'0.
Rewrite <- (rZCompInv (mEval n a q Hq)); Rewrite <- Eqp''; Rewrite Eqp;
Rewrite (mEvalRzTrue n a); Change (rZComp (mEval n a r Hr))=(rZComp rZFalse);
Rewrite <- (mEvalRzFalse n a); Apply rZCompComp; Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eqp'''; Auto.
Intros H'1; Inversion H'1; Auto.
Case Eqp'''; Auto.
Intros Eqp H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp'; Auto.
Intros H'0; Inversion H'0.
Rewrite (mEvalRzFalse n a); Rewrite <- Eqp'; Rewrite Eqp;
Change (rZComp (mEval n a r Hr))=(rZComp rZTrue); Rewrite <- (mEvalRzTrue n a);
Apply rZCompComp; Auto.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp''; Auto.
Case Eqp'; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp'''; Auto.
Intros H'0; Inversion H'0.
Rewrite <- (rZCompInv (mEval n a q Hq)); Rewrite <- Eqp'''; Rewrite Eqp;
Rewrite (rZCompInv (mEval n a r Hr)); Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eqp''''; Auto.
Absurd (mEval n a p Hp)=(rZComp (mEval n a r Hr)); Auto; Rewrite Eqp''''; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp''''''; Auto.
Intros H'1; Inversion H'1; Auto.
Case Eqp''''''; Auto.
Intros Eqq H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp; Auto.
Intros H'0; Inversion H'0.
Rewrite Eqp; Rewrite Eqq; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp'; Auto.
Intros H'0; Inversion H'0.
Rewrite Eqp'; Rewrite Eqq; Rewrite (mEvalRzTrue n a);
Change (rZComp (mEval n a r Hr))=(rZComp rZFalse);
Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eqp''; Auto.
Case Eqp; Rewrite Eqq; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'''; Auto.
Case Eqp'; Rewrite Eqq; Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq'; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqq'; Auto.
Intros Eqq H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp; Auto.
Intros H'0; Inversion H'0.
Rewrite Eqp; Rewrite Eqq; Rewrite (mEvalRzFalse n a);
Change (rZComp (mEval n a r Hr))=(rZComp rZTrue); Rewrite <- (mEvalRzTrue n a);
Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp'; Auto.
Intros H'0; Inversion H'0.
Rewrite Eqp'; Rewrite Eqq; Rewrite (rZCompInv (mEval n a r Hr)); Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eqp''; Auto.
Absurd (mEval n a p Hp)=(rZComp (mEval n a q Hq)); Auto.
Rewrite Eqp''; Rewrite Eqq; Rewrite (rZCompInv (mEval n a r Hr)); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'''; Auto.
Case Eqp; Rewrite Eqp'''; Rewrite Eqq; Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq'; Auto.
Absurd (mEval n a q Hq)=(rZComp (mEval n a r Hr)); Auto; Rewrite Eqq'; Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq''; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqq''; Auto.
Intros Eqp H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp'; Auto.
Intros H'0; Inversion H'0.
Apply sym_equal; Rewrite <- Eqp'; Rewrite Eqp; Rewrite <- (mEvalRzTrue n a);
Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp''; Auto.
Intros H'0; Inversion H'0.
Apply sym_equal; Rewrite <- (rZCompInv (mEval n a q Hq)); Rewrite <- Eqp'';
Rewrite Eqp; Simpl; Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eqp'''; Auto.
Intros H'0; Inversion H'0.
Rewrite <- Eqp'''; Rewrite Eqp; Rewrite <- (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp''''; Auto.
Intros H'0; Inversion H'0.
Rewrite <- (rZCompInv (mEval n a r Hr)); Rewrite <- Eqp''''; Rewrite Eqp; Simpl;
Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq; Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq'; Auto.
Intros H'0; Inversion H'0; Absurd (mEval n a p Hp)=rZTrue; Auto.
Rewrite (addEqNop n a p rZFalse Hp (rZLeFalse n)); Auto;
Rewrite (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp'''''; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqp'''''; Auto.
Intros Eqp H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq;
Rewrite (mEvalComp n a r Hr (rZLeComp n r Hr)); Auto.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp'; Auto.
Intros H'0; Auto; Inversion H'0.
Apply sym_equal; Rewrite <- Eqp'; Rewrite Eqp;
Change (rZComp (mEval n a r Hr))=(rZComp rZTrue); Rewrite <- (mEvalRzTrue n a);
Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp''; Auto.
Intros H'0; Inversion H'0.
Apply sym_equal; Rewrite <- (rZCompInv (mEval n a q Hq)); Rewrite <- Eqp'';
Rewrite Eqp; Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eqp'''; Auto.
Intros H'0; Inversion H'0.
Rewrite <- Eqp'''; Rewrite Eqp; Simpl; Rewrite <- (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp''''; Auto.
Intros H'0; Inversion H'0.
Rewrite <- Eqp''''; Rewrite Eqp; Simpl; Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq; Auto.
Intros H'0; Inversion H'0;
Absurd (mEval n a p Hp)=(mEval n a rZTrue (rZLeTrue n)); Auto.
Rewrite Eqp; Rewrite (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq'; Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp'''''; Auto.
Absurd (mEval n a p Hp)=rZTrue; Auto; Rewrite Eqp; Auto.
Case (rZDec (mEval n a p Hp) rZFalse); Intros Eqp''''''; Auto.
Rewrite <- (mEvalComp n a r Hr (rZLeComp n r Hr)); Intros H'1; Inversion H'1;
Auto.
Case Eqp''''''; Auto.
Intros Eqq H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp; Auto.
Intros H'0; Inversion H'0.
Apply sym_equal; Rewrite Eqp; Rewrite Eqq; Rewrite <- (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp'; Auto.
Intros H'0; Inversion H'0.
Apply sym_equal; Rewrite Eqp'; Rewrite Eqq; Simpl;
Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eqp''; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'''; Auto.
Intros H'0; Inversion H'0;
Absurd (mEval n a q Hq)=(mEval n a rZFalse (rZLeFalse n)); Auto.
Rewrite (mEvalRzFalse n a); Rewrite Eqq; Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq'; Auto.
Intros H'0; Inversion H'0; Auto.
Rewrite <- Eqq'; Rewrite Eqq; Rewrite <- (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq''; Auto.
Intros H'0; Inversion H'0; Auto.
Rewrite <- (rZCompInv (mEval n a r Hr)); Rewrite <- Eqq''; Rewrite Eqq; Simpl;
Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp''''; Auto.
Case Eqp; Rewrite Eqp''''; Rewrite Eqq; Auto.
Case (rZDec (mEval n a p Hp) rZFalse); Intros Eqp'''''; Auto.
Case Eqp'; Rewrite Eqp'''''; Rewrite Eqq; Auto.
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eqq'''; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqq'''; Auto.
Intros Eqq H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq;
Rewrite (mEvalComp n a r Hr (rZLeComp n r Hr)); Auto.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp; Auto.
Intros H'0; Auto; Inversion H'0.
Apply sym_equal; Rewrite Eqp; Rewrite Eqq;
Change (rZComp (mEval n a r Hr))=(rZComp rZTrue); Rewrite <- (mEvalRzTrue n a);
Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp'; Auto.
Intros H'0; Inversion H'0.
Apply sym_equal; Rewrite Eqp'; Rewrite Eqq; Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eqp''; Auto.
Intros H'0; Inversion H'0.
Absurd (mEval n a q Hq)=(mEval n a rZTrue (rZLeTrue n)); Auto; Rewrite Eqq;
Rewrite (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'''; Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq'; Auto.
Intros H'0; Inversion H'0.
Rewrite <- Eqq'; Rewrite Eqq; Simpl; Rewrite <- (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq''; Auto.
Intros H'0; Inversion H'0.
Rewrite <- Eqq''; Rewrite Eqq; Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp''''; Auto.
Case Eqp'; Rewrite Eqp''''; Rewrite Eqq; Auto.
Case (rZDec (mEval n a p Hp) rZFalse); Intros Eqp'''''; Auto.
Case Eqp; Rewrite Eqp'''''; Rewrite Eqq; Auto.
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eqq'''; Auto.
Absurd (mEval n a q Hq)=rZTrue; Auto; Rewrite Eqq; Auto.
Case (rZDec (mEval n a q Hq) rZFalse); Intros Eqq''''; Auto.
Intros H'0; Inversion H'0; Rewrite <- (mEvalComp n a r Hr (rZLeComp n r Hr));
Auto.
Case Eqq''''; Auto.
Intros Eqr H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq;
Auto.
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp; Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp'; Auto.
Intros H'0; Inversion H'0;
Absurd (mEval n a r Hr)=(mEval n a rZFalse (rZLeFalse n)); Auto.
Rewrite (mEvalRzFalse n a); Rewrite Eqr; Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eqp''; Auto.
Intros H'0; Inversion H'0.
Apply sym_equal; Rewrite Eqp''; Rewrite Eqr; Rewrite <- (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'''; Auto.
Intros H'0; Inversion H'0.
Apply sym_equal; Rewrite Eqp'''; Rewrite Eqr; Simpl;
Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq; Auto.
Intros H'0; Inversion H'0.
Rewrite Eqq; Rewrite Eqr; Rewrite <- (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq'; Auto.
Intros H'0; Inversion H'0.
Rewrite Eqq'; Rewrite Eqr; Simpl; Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp''''; Auto.
Case Eqp''; Rewrite Eqp''''; Rewrite Eqr; Auto.
Case (rZDec (mEval n a p Hp) rZFalse); Intros Eqp'''''; Auto.
Case Eqp'''; Rewrite Eqp'''''; Rewrite Eqr; Auto.
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eqq''; Auto.
Case Eqq; Rewrite Eqq''; Rewrite Eqr; Auto.
Case (rZDec (mEval n a q Hq) rZFalse); Intros Eqq'''; Auto.
Case Eqq'; Rewrite Eqq'''; Rewrite Eqr; Auto.
Case (rZDec (mEval n a r Hr) rZTrue); Intros Eqq''''; Auto.
Intros H'0; Inversion H'0; Auto.
Case Eqq''''; Auto.
Intros Eqr H'1; Apply nopAddEq; Generalize H'1; Clear H'1; Unfold doTripletEq;
Auto; Rewrite (mEvalComp n a q Hq (rZLeComp n q Hq)).
Case (rZDec (mEval n a p Hp) (mEval n a q Hq)); Intros Eqp; Auto.
Intros H'0; Inversion H'0;
Absurd (mEval n a r Hr)=(mEval n a rZTrue (rZLeTrue n)); Auto.
Rewrite Eqr; Rewrite (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a q Hq))); Intros Eqp'; Auto.
Case (rZDec (mEval n a p Hp) (mEval n a r Hr)); Intros Eqp''; Auto.
Intros H'0; Inversion H'0.
Apply sym_equal; Rewrite Eqp''; Rewrite Eqr;
Change (rZComp (mEval n a q Hq))=(rZComp rZTrue); Rewrite <- (mEvalRzTrue n a);
Auto.
Case (rZDec (mEval n a p Hp) (rZComp (mEval n a r Hr))); Intros Eqp'''; Auto.
Intros H'0; Inversion H'0.
Apply sym_equal; Rewrite Eqp'''; Rewrite Eqr; Rewrite <- (mEvalRzFalse n a);
Auto.
Case (rZDec (mEval n a q Hq) (mEval n a r Hr)); Intros Eqq; Auto.
Intros H'0; Inversion H'0.
Rewrite Eqq; Rewrite Eqr; Simpl; Rewrite <- (mEvalRzTrue n a); Auto.
Case (rZDec (mEval n a q Hq) (rZComp (mEval n a r Hr))); Intros Eqq'; Auto.
Intros H'0; Inversion H'0.
Rewrite Eqq'; Rewrite Eqr; Simpl; Rewrite <- (mEvalRzFalse n a); Auto.
Case (rZDec (mEval n a p Hp) rZTrue); Intros Eqp''''; Auto.
Case Eqp'''; Rewrite Eqp''''; Rewrite Eqr; Auto.
Case (rZDec (mEval n a p Hp) rZFalse); Intros Eqp'''''; Auto.
Case Eqp''; Rewrite Eqp'''''; Rewrite Eqr; Auto.
Case (rZDec (mEval n a q Hq) rZTrue); Intros Eqq''; Auto.
Case Eqq'; Rewrite Eqq''; Rewrite Eqr; Auto.
Case (rZDec (mEval n a q Hq) rZFalse); Intros Eqq'''; Auto.
Case Eqq; Rewrite Eqq'''; Rewrite Eqr; Auto.
Case (rZDec (mEval n a r Hr) rZTrue); Intros Eqq''''; Auto.
Absurd (mEval n a r Hr)=rZTrue; Auto; Rewrite Eqr; Auto.
Case (rZDec (mEval n a r Hr) rZFalse); Intros Eqq'''''; Auto.
Intros H'0; Inversion H'0; Rewrite <- (mEvalComp n a q Hq (rZLeComp n q Hq));
Auto.
Case Eqq'''''; Auto.
Qed.
Theorem
doTripletEqEqEq:
(n:rNat)
(m1, m2:(memory n))
(p1, p2, q1, q2, r1, r2:rZ)
(Hp1:(rZLe p1 n))
(Hp2:(rZLe p2 n))
(Hq1:(rZLe q1 n))
(Hq2:(rZLe q2 n))
(Hr1:(rZLe r1 n))
(Hr2:(rZLe r2 n))
(eqMem n m1 m2) ->
(mEval n m1 p1 Hp1)=(mEval n m1 p2 Hp2) ->
(mEval n m1 q1 Hq1)=(mEval n m1 q2 Hq2) ->
(mEval n m1 r1 Hr1)=(mEval n m1 r2 Hr2) ->
(eqOption
(tMemory n) (eqtMem n) (doTripletEq n m1 p1 q1 r1 Hp1 Hq1 Hr1)
(doTripletEq n m2 p2 q2 r2 Hp2 Hq2 Hr2)).
Intros n m1 m2 p1 p2 q1 q2 r1 r2 Hp1 Hp2 Hq1 Hq2 Hr1 Hr2 eqM Eqp Eqq Eqr;
Unfold doTripletEq.
Cut (eqMem n m2 m1); [Intros Eqm2m1 | Apply (eqMemSym n)]; Auto.
Cut (mEval n m2 p1 Hp1)=(mEval n m2 p2 Hp2);
[Intros Eqp' | Apply eqMeminv1 with m1 := m1]; Auto.
Cut (mEval n m2 q1 Hq1)=(mEval n m2 q2 Hq2);
[Intros Eqq' | Apply eqMeminv1 with m1 := m1]; Auto.
Cut (mEval n m2 r1 Hr1)=(mEval n m2 r2 Hr2);
[Intros Eqr' | Apply eqMeminv1 with m1 := m1]; Auto.
Case (rZDec (mEval n m1 p1 Hp1) (mEval n m1 q1 Hq1));
Case (rZDec (mEval n m2 p2 Hp2) (mEval n m2 q2 Hq2)); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminv1 with m1 := m1; Auto; Rewrite <- Eqq;
Rewrite <- Eqp; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminv2 with m2 := m2; Auto; Rewrite Eqq';
Rewrite Eqp'; Auto.
Intros H'0 H'1; Clear H'0 H'1;
Case (rZDec (mEval n m1 p1 Hp1) (rZComp (mEval n m1 q1 Hq1)));
Case (rZDec (mEval n m2 p2 Hp2) (rZComp (mEval n m2 q2 Hq2))); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvopp1 with m1 := m1; Auto;
Rewrite <- Eqq; Rewrite <- Eqp; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvopp2 with m2 := m2; Auto; Rewrite Eqq';
Rewrite Eqp'; Auto.
Intros H'0 H'1; Clear H'0 H'1;
Case (rZDec (mEval n m1 p1 Hp1) (mEval n m1 r1 Hr1));
Case (rZDec (mEval n m2 p2 Hp2) (mEval n m2 r2 Hr2)); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminv1 with m1 := m1; Auto; Rewrite <- Eqr;
Rewrite <- Eqp; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminv2 with m2 := m2; Auto; Rewrite Eqr';
Rewrite Eqp'; Auto.
Intros H'0 H'1; Clear H'0 H'1;
Case (rZDec (mEval n m1 p1 Hp1) (rZComp (mEval n m1 r1 Hr1)));
Case (rZDec (mEval n m2 p2 Hp2) (rZComp (mEval n m2 r2 Hr2))); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvopp1 with m1 := m1; Auto;
Rewrite <- Eqr; Rewrite <- Eqp; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvopp2 with m2 := m2; Auto; Rewrite Eqr';
Rewrite Eqp'; Auto.
Intros H'0 H'1; Clear H'0 H'1;
Case (rZDec (mEval n m1 q1 Hq1) (mEval n m1 r1 Hr1));
Case (rZDec (mEval n m2 q2 Hq2) (mEval n m2 r2 Hr2)); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminv1 with m1 := m1; Auto; Rewrite <- Eqr;
Rewrite <- Eqq; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminv2 with m2 := m2; Auto; Rewrite Eqr';
Rewrite Eqq'; Auto.
Intros H'0 H'1; Clear H'0 H'1;
Case (rZDec (mEval n m1 q1 Hq1) (rZComp (mEval n m1 r1 Hr1)));
Case (rZDec (mEval n m2 q2 Hq2) (rZComp (mEval n m2 r2 Hr2))); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvopp1 with m1 := m1; Auto;
Rewrite <- Eqr; Rewrite <- Eqq; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvopp2 with m2 := m2; Auto; Rewrite Eqr';
Rewrite Eqq'; Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 p1 Hp1) rZTrue);
Case (rZDec (mEval n m2 p2 Hp2) rZTrue); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvTrue with m1 := m1; Auto;
Rewrite <- Eqp; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvTrue with m1 := m2; Auto; Rewrite Eqp';
Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 p1 Hp1) rZFalse);
Case (rZDec (mEval n m2 p2 Hp2) rZFalse); Auto.
Intros H' H'0.
Apply eqOptionSome; Auto; Apply addEqEq; Auto;
Apply trans_equal with y := (rZComp (mEval n m1 r1 Hr1)); Auto;
Apply trans_equal with y := (rZComp (mEval n m1 r2 Hr2)); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvFalse with m1 := m1; Auto;
Rewrite <- Eqp; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvFalse with m1 := m2; Auto; Rewrite Eqp';
Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 q1 Hq1) rZTrue);
Case (rZDec (mEval n m2 q2 Hq2) rZTrue); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvTrue with m1 := m1; Auto;
Rewrite <- Eqq; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvTrue with m1 := m2; Auto; Rewrite Eqq';
Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 q1 Hq1) rZFalse);
Case (rZDec (mEval n m2 q2 Hq2) rZFalse); Auto.
Intros H' H'0; Apply eqOptionSome; Auto; Apply addEqEq; Auto;
Apply trans_equal with y := (rZComp (mEval n m1 r1 Hr1)); Auto;
Apply trans_equal with y := (rZComp (mEval n m1 r2 Hr2)); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvFalse with m1 := m1; Auto;
Rewrite <- Eqq; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvFalse with m1 := m2; Auto; Rewrite Eqq';
Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 r1 Hr1) rZTrue);
Case (rZDec (mEval n m2 r2 Hr2) rZTrue); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvTrue with m1 := m1; Auto;
Rewrite <- Eqr; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvTrue with m1 := m2; Auto; Rewrite Eqr';
Auto.
Intros H'0 H'1; Clear H'0 H'1; Case (rZDec (mEval n m1 r1 Hr1) rZFalse);
Case (rZDec (mEval n m2 r2 Hr2) rZFalse); Auto.
Intros H' H'0; Apply eqOptionSome; Auto; Apply addEqEq; Auto;
Apply trans_equal with y := (rZComp (mEval n m1 q1 Hq1)); Auto;
Apply trans_equal with y := (rZComp (mEval n m1 q2 Hq2)); Auto.
Intros H'0 H'1; Case H'0; Apply eqMeminvFalse with m1 := m1; Auto;
Rewrite <- Eqr; Auto.
Intros H'0 H'1; Case H'1; Apply eqMeminvFalse with m1 := m2; Auto; Rewrite Eqr';
Auto.
Qed.
Hints Resolve doTripletEqEqEq.
23/02/99, 18:38