From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.182.252.166 with SMTP id zt6mr16161573obc.17.1398787181909;
 Tue, 29 Apr 2014 08:59:41 -0700 (PDT)
MIME-Version: 1.0
Path: 
 border2.nntp.dca.giganews.com!ottix-news.ottix.net!news.litech.org!news.glorb.com!peer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!l13no11982021iga.0!news-out.google.com!dz10ni26700qab.1!nntp.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Tue, 29 Apr 2014 10:59:41 -0500
From: benjaminhocking <benjaminhocking@gmail.com>
Subject: (SPARK Ada) Proving that bitwise and is associative?
Newsgroups: comp.lang.ada
X-UserIpAddress: 8.25.3.50
X-InternalId: 8ae70c43-5c84-4821-ade3-21db1b7d88b8
Message-ID: <nd2dnZa1N-bwUcLOnZ2dnUVZ_gOdnZ2d@giganews.com>
Date: Tue, 29 Apr 2014 10:59:41 -0500
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-RYeFdlq/WqBAhIkJhKTCt+rpN9FpJGRwZGygdySlaPzGMLhZblYPZfULzTs1AI6NkFh6RzOMYRVdnd+!1Z+I7OW8R6or4qhJcRiANLBjTdNC9Y5i6DrLIiS2A2y4SmCBljBKA2Wqf8rmdlM+J2Ug4URsyJCe!OQ==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.40
X-Original-Bytes: 1488
X-Received-Bytes: 1816
X-Received-Body-CRC: 3571117350
Xref: number.nntp.dca.giganews.com comp.lang.ada:186165
Date: 2014-04-29T10:59:41-05:00
List-Id: <comp.lang.ada>

I have the following check statements embedded in some SPARK Ada code:
      --# check (value and (mask_32 and Unsigned_32'Mod(LMask_8))) = 0;
      --# check ((value and mask_32) and Unsigned_32'Mod(LMask_8)) = 0;
The SPARK examiner is able to prove the first one (using inference) but not the second one, even though it has already proven the first one, so should be able to prove it by using the first one combined with the fact that bitwise and is associative. Does anyone have any suggestions for how I can help it?