proposition: Theorem doTripletsTermExAux : forall (L : list triplet) (S1 S2 : State), doTripletsP S1 L S2 -> forall t : triplet, In t L -> doTripletsP S1 (rem _ tripletDec t L) S2 \/ (exists S3 : State, (exists S4 : State, doTripletsP S1 (rem _ tripletDec t L) S3 /\ doTripletP S3 t S4 /\ doTripletsP S4 (rem _ tripletDec t L) S2)).
proof: Proof. intros L S1 S2 H'; Elimc H'; clear L S1 S2; auto with stalmarck. intros S1 S2 S3 L t H' H'0 H'1 H'2 t0 H'3. case (tripletDec t t0); intros H. elim (H'2 t); [ intros H'6 | intros H'6; Elimc H'6; intros S0 E; Elimc E; intros S4 E; Elimc E; intros H'6 H'7; Elimc H'7; intros H'7 H'8 | idtac ]; auto with stalmarck. right; exists S1; exists S2; split; auto with stalmarck; split; auto with stalmarck. rewrite <- H; auto with stalmarck. rewrite <- H; auto with stalmarck. right; exists S1; exists S2; split; auto with stalmarck; split; auto with stalmarck. rewrite <- H; auto with stalmarck. apply doTripletsRTrans with (S2 := S0); auto with stalmarck. rewrite <- H; auto with stalmarck. apply doTripletsComp with (S1 := S4) (S2 := S3); auto with stalmarck. rewrite <- H; auto with stalmarck. apply doTripletInvol with (t := t) (S1 := S1) (S2 := S2); auto with stalmarck. apply doTripletsIncl with (L := rem triplet tripletDec t L); auto with stalmarck. elim (H'2 t0); [ intros H'6 | intros H'6; Elimc H'6; intros S0 E; Elimc E; intros S4 E; Elimc E; intros H'6 H'7; Elimc H'7; intros H'7 H'8 | idtac ]; auto with stalmarck. left. apply doTripletsTrans with (S2 := S2) (t := t); auto with stalmarck. right; exists S0; exists S4; split; [ idtac | split ]; auto with stalmarck. apply doTripletsTrans with (S2 := S2) (t := t); auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux)