From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on
	ip-172-31-74-118.ec2.internal
X-Spam-Level: 
X-Spam-Status: No, score=0.8 required=3.0 tests=BAYES_50 autolearn=ham
	autolearn_force=no version=3.4.6
X-Received: by 2002:a05:620a:15e8:: with SMTP id p8mr2930263qkm.27.1630669981230;
        Fri, 03 Sep 2021 04:53:01 -0700 (PDT)
X-Received: by 2002:a5b:142:: with SMTP id c2mr4133996ybp.425.1630669981104;
 Fri, 03 Sep 2021 04:53:01 -0700 (PDT)
Path: eternal-september.org!reader02.eternal-september.org!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Fri, 3 Sep 2021 04:53:00 -0700 (PDT)
In-Reply-To: <7df72bca-16f6-4aac-9f95-ef09cf0bbca3n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=80.194.57.154; posting-account=xS3LTwoAAAB3aeXopC8a-M58TGE8K6go
NNTP-Posting-Host: 80.194.57.154
References: <10e82e71-53f5-46d0-8960-46a7593b964dn@googlegroups.com>
 <86r1e80zu2.fsf@stephe-leake.org> <4fc90fe9-f75e-437c-babd-05ea194d42e6n@googlegroups.com>
 <7df72bca-16f6-4aac-9f95-ef09cf0bbca3n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <1f2990ab-ee11-4f6e-8541-460e0b6bc6c8n@googlegroups.com>
Subject: Re: Postcondition on Strings.Maps.To_Sequence
From: Mark Wilson <markwilson@wilsonnet.technology>
Injection-Date: Fri, 03 Sep 2021 11:53:01 +0000
Content-Type: text/plain; charset="UTF-8"
Xref: reader02.eternal-september.org comp.lang.ada:62618
List-Id: <comp.lang.ada>

You'll also need to prove that each character in the sequence is unique ...