proposition: Theorem doTripletFCorrect : forall (Ar : rArray vM) (t : triplet) (S : State), wellFormedArray Ar -> rArrayState Ar S -> match doTripletF Ar t with | None => forall S' : State, ~ doTripletP S t S' | Some (triple Ar' false L) => wellFormedArray Ar' /\ (exists S' : State, doTripletP S t S' /\ rArrayState Ar' S') /\ OlistRz L /\ (forall e : rNat, ~ InRz (rZPlus e) L -> rArrayGet _ Ar' e = rArrayGet _ Ar e) | Some (triple Ar' true L) => exists S' : State, doTripletP S t S' /\ contradictory S' end.
proof: Proof. intros Ar t S H' H'0; unfold doTripletF, letP in |- *. case t. intros b p q r; case b. case (rZDec (evalZ Ar p) (rZComp (evalZ Ar q))); intros Eq0. generalize (addEqMem2Correct Ar (evalZ Ar r) rZFalse (evalZ Ar q) rZTrue); case (addEqMem2 Ar (evalZ Ar r) rZFalse (evalZ Ar q) rZTrue). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (q, rZTrue) (addEq (r, rZFalse) S)); split; auto with stalmarck. apply doTripletAndPpmq; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq2; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (q, rZTrue) (addEq (r, rZFalse) S)); split; auto with stalmarck. apply doTripletAndPpmq; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq2; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar p) (rZComp (evalZ Ar r))); intros Eq1. generalize (addEqMem2Correct Ar (evalZ Ar r) rZTrue (evalZ Ar q) rZFalse); case (addEqMem2 Ar (evalZ Ar r) rZTrue (evalZ Ar q) rZFalse). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (q, rZFalse) (addEq (r, rZTrue) S)); split; auto with stalmarck. apply doTripletAndPpmr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq2; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (q, rZFalse) (addEq (r, rZTrue) S)); split; auto with stalmarck. apply doTripletAndPpmr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq2; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar q) (evalZ Ar r)); intros Eq2. generalize (addEqMemCorrect Ar (evalZ Ar p) (evalZ Ar r)); case (addEqMem Ar (evalZ Ar p) (evalZ Ar r)). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, r) S); split; auto with stalmarck. apply doTripletAndPqr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, r) S); split; auto with stalmarck. apply doTripletAndPqr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar q) (rZComp (evalZ Ar r))); intros Eq3. generalize (addEqMemCorrect Ar (evalZ Ar p) rZFalse); case (addEqMem Ar (evalZ Ar p) rZFalse). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, rZFalse) S); split; auto with stalmarck. apply doTripletAndPqmr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, rZFalse) S); split; auto with stalmarck. apply doTripletAndPqmr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar p) rZTrue); intros Eq4. generalize (addEqMem2Correct Ar (evalZ Ar r) rZTrue (evalZ Ar q) rZTrue); case (addEqMem2 Ar (evalZ Ar r) rZTrue (evalZ Ar q) rZTrue). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (q, rZTrue) (addEq (r, rZTrue) S)); split; auto with stalmarck. apply doTripletAndPpT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq2; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (q, rZTrue) (addEq (r, rZTrue) S)); split; auto with stalmarck. apply doTripletAndPpT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq2; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar q) rZTrue); intros Eq5. generalize (addEqMemCorrect Ar (evalZ Ar p) (evalZ Ar r)); case (addEqMem Ar (evalZ Ar p) (evalZ Ar r)). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, r) S); split; auto with stalmarck. apply doTripletAndPqT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, r) S); split; auto with stalmarck. apply doTripletAndPqT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar q) rZFalse); intros Eq6. generalize (addEqMemCorrect Ar (evalZ Ar p) rZFalse); case (addEqMem Ar (evalZ Ar p) rZFalse). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, rZFalse) S); split; auto with stalmarck. apply doTripletAndPqF; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZFalse; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, rZFalse) S); split; auto with stalmarck. apply doTripletAndPqF; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZFalse; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar r) rZTrue); intros Eq7. generalize (addEqMemCorrect Ar (evalZ Ar p) (evalZ Ar q)); case (addEqMem Ar (evalZ Ar p) (evalZ Ar q)). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, q) S); split; auto with stalmarck. apply doTripletAndPrT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, q) S); split; auto with stalmarck. apply doTripletAndPrT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar r) rZFalse); intros Eq8. generalize (addEqMemCorrect Ar (evalZ Ar p) rZFalse); case (addEqMem Ar (evalZ Ar p) rZFalse). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, rZFalse) S); split; auto with stalmarck. apply doTripletAndPrF; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZFalse; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, rZFalse) S); split; auto with stalmarck. apply doTripletAndPrF; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZFalse; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros S'; red in |- *; intros H'1; inversion H'1; auto with stalmarck. Contradict Eq0; rewrite <- evalZComp; apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq1; rewrite <- evalZComp; apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq2; apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq3; rewrite <- evalZComp; apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq4; rewrite <- (evalZTrue Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq5; rewrite <- (evalZTrue Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq6; rewrite <- (evalZFalse Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq7; rewrite <- (evalZTrue Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq8; rewrite <- (evalZFalse Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. case (rZDec (evalZ Ar p) (evalZ Ar q)); intros Eq0. generalize (addEqMemCorrect Ar (evalZ Ar r) rZTrue); case (addEqMem Ar (evalZ Ar r) rZTrue). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (r, rZTrue) S); split; auto with stalmarck. apply doTripletEqPpq; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (r, rZTrue) S); split; auto with stalmarck. apply doTripletEqPpq; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar p) (rZComp (evalZ Ar q))); intros Eq1. generalize (addEqMemCorrect Ar (evalZ Ar r) rZFalse); case (addEqMem Ar (evalZ Ar r) rZFalse). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (r, rZFalse) S); split; auto with stalmarck. apply doTripletEqPpmq; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (r, rZFalse) S); split; auto with stalmarck. apply doTripletEqPpmq; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar p) (evalZ Ar r)); intros Eq2. generalize (addEqMemCorrect Ar (evalZ Ar q) rZTrue); case (addEqMem Ar (evalZ Ar q) rZTrue). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (q, rZTrue) S); split; auto with stalmarck. apply doTripletEqPpr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (q, rZTrue) S); split; auto with stalmarck. apply doTripletEqPpr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar p) (rZComp (evalZ Ar r))); intros Eq3. generalize (addEqMemCorrect Ar (evalZ Ar q) rZFalse); case (addEqMem Ar (evalZ Ar q) rZFalse). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (q, rZFalse) S); split; auto with stalmarck. apply doTripletEqPpmr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (q, rZFalse) S); split; auto with stalmarck. apply doTripletEqPpmr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar q) (evalZ Ar r)); intros Eq4. generalize (addEqMemCorrect Ar (evalZ Ar p) rZTrue); case (addEqMem Ar (evalZ Ar p) rZTrue). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, rZTrue) S); split; auto with stalmarck. apply doTripletEqPqr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, rZTrue) S); split; auto with stalmarck. apply doTripletEqPqr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar q) (rZComp (evalZ Ar r))); intros Eq5. generalize (addEqMemCorrect Ar (evalZ Ar p) rZFalse); case (addEqMem Ar (evalZ Ar p) rZFalse). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, rZFalse) S); split; auto with stalmarck. apply doTripletEqPqmr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, rZFalse) S); split; auto with stalmarck. apply doTripletEqPqmr; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar p) rZTrue); intros Eq6. generalize (addEqMemCorrect Ar (evalZ Ar q) (evalZ Ar r)); case (addEqMem Ar (evalZ Ar q) (evalZ Ar r)). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (q, r) S); split; auto with stalmarck. apply doTripletEqPpT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (q, r) S); split; auto with stalmarck. apply doTripletEqPpT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar p) rZFalse); intros Eq7. generalize (addEqMemCorrect Ar (evalZ Ar q) (rZComp (evalZ Ar r))); case (addEqMem Ar (evalZ Ar q) (rZComp (evalZ Ar r))). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (q, rZComp r) S); split; auto with stalmarck. apply doTripletEqPpF; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZFalse; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; try apply eqStateRzInv; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (q, rZComp r) S); split; auto with stalmarck. apply doTripletEqPpF; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZFalse; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; try apply eqStateRzInv; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar q) rZTrue); intros Eq8. generalize (addEqMemCorrect Ar (evalZ Ar p) (evalZ Ar r)); case (addEqMem Ar (evalZ Ar p) (evalZ Ar r)). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, r) S); split; auto with stalmarck. apply doTripletEqPqT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, r) S); split; auto with stalmarck. apply doTripletEqPqT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar q) rZFalse); intros Eq9. generalize (addEqMemCorrect Ar (evalZ Ar p) (rZComp (evalZ Ar r))); case (addEqMem Ar (evalZ Ar p) (rZComp (evalZ Ar r))). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, rZComp r) S); split; auto with stalmarck. apply doTripletEqPqF; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZFalse; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; try apply eqStateRzInv; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, rZComp r) S); split; auto with stalmarck. apply doTripletEqPqF; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZFalse; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; try apply eqStateRzInv; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar r) rZTrue); intros Eq10. generalize (addEqMemCorrect Ar (evalZ Ar p) (evalZ Ar q)); case (addEqMem Ar (evalZ Ar p) (evalZ Ar q)). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, q) S); split; auto with stalmarck. apply doTripletEqPrT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, q) S); split; auto with stalmarck. apply doTripletEqPrT; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZTrue; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; apply eqStateEvalZ; auto with stalmarck. case (rZDec (evalZ Ar r) rZFalse); intros Eq11. generalize (addEqMemCorrect Ar (evalZ Ar p) (rZComp (evalZ Ar q))); case (addEqMem Ar (evalZ Ar p) (rZComp (evalZ Ar q))). intros Ar' b' L'; case b'. intros H'2; generalize (H'2 S H' H'0); intros H'3; exists (addEq (p, rZComp q) S); split; auto with stalmarck. apply doTripletEqPrF; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZFalse; auto with stalmarck. apply contradictoryEq with (1 := H'3); auto with stalmarck. apply eqStateEq1; auto with stalmarck; try apply eqStateRzInv; apply eqStateEvalZ; auto with stalmarck. intros H'2; elim (H'2 S); [ intros H'6 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. split; auto with stalmarck. split; auto with stalmarck. exists (addEq (p, rZComp q) S); split; auto with stalmarck. apply doTripletEqPrF; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZFalse; auto with stalmarck. apply rArrayStateEqState with (1 := H'7); auto with stalmarck. apply eqStateEq1; auto with stalmarck; try apply eqStateRzInv; apply eqStateEvalZ; auto with stalmarck. intros S'; red in |- *; intros H'1; inversion H'1; auto with stalmarck. Contradict Eq0; apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq1; rewrite <- evalZComp; apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq2; apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq3; rewrite <- evalZComp; apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq4; apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq5; rewrite <- evalZComp; apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq6; rewrite <- (evalZTrue Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq7; rewrite <- (evalZFalse Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq8; rewrite <- (evalZTrue Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq9; rewrite <- (evalZFalse Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq10; rewrite <- (evalZTrue Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. Contradict Eq11; rewrite <- (evalZFalse Ar H'); apply rArrayStateDef1 with (S := S); auto with stalmarck. Qed.
imports: Stalmarck(interState doTriplet)