Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
7e94fa68
Commit
7e94fa68
authored
Feb 23, 2016
by
MARCHE Claude
Browse files
sessions: more updates with Coq 8.5
parent
34c5aeb6
Changes
21
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/bag.mlw
View file @
7e94fa68
...
...
@@ -152,7 +152,9 @@ module BagImpl
t.contents <- Bag.remove x t.contents;
assert { forall v: 'a. numof t.data v 0 i = numof (at t.data 'L) v 0 i };
assert { forall v: 'a.
numof t.data v i n = numof (at t.data 'L) v (i+1) (n+1) }
numof t.data v i n = numof (at t.data 'L) v (i+1) (n+1) };
assert { forall v: 'a.
numof t.data v 0 n = numof t.data v 0 i + numof t.data v i n }
end
...
...
examples/bag/why3session.xml
View file @
7e94fa68
...
...
@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"1
0
"
memlimit=
"
1
000"
/>
<prover
id=
"1"
name=
"CVC4"
version=
"1.4"
timelimit=
"6"
memlimit=
"
1
000"
/>
<prover
id=
"
2
"
name=
"Z3"
version=
"4.3.
1
"
timelimit=
"6"
memlimit=
"1000"
/>
<prover
id=
"
3
"
name=
"
Z
3"
version=
"
4.3.2
"
timelimit=
"
1
0"
memlimit=
"
1
000"
/>
<prover
id=
"
4
"
name=
"
Alt-Ergo
"
version=
"
0.95.2
"
timelimit=
"
6
"
memlimit=
"
1
000"
/>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"
6"
steplimit=
"
1"
memlimit=
"
4
000"
/>
<prover
id=
"1"
name=
"CVC4"
version=
"1.4"
timelimit=
"6"
steplimit=
"1"
memlimit=
"
4
000"
/>
<prover
id=
"
3
"
name=
"Z3"
version=
"4.3.
2
"
timelimit=
"6"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"
5
"
name=
"
CVC
3"
version=
"
2.4.1
"
timelimit=
"
6
0"
steplimit=
"1"
memlimit=
"
4
000"
/>
<prover
id=
"
9
"
name=
"
Z3
"
version=
"
4.4.0
"
timelimit=
"
5
"
memlimit=
"
4
000"
/>
<file
name=
"../bag.mlw"
expanded=
"true"
>
<theory
name=
"Bag"
sum=
"d41d8cd98f00b204e9800998ecf8427e"
>
</theory>
...
...
@@ -14,97 +14,112 @@
</theory>
<theory
name=
"ResizableArraySpec"
sum=
"d41d8cd98f00b204e9800998ecf8427e"
>
</theory>
<theory
name=
"BagImpl"
sum=
"
4080129895e6d68d61618da0c53064c5"
expanded=
"true
"
>
<theory
name=
"BagImpl"
sum=
"
8044c27621c87bd642caf406894f291b
"
>
<goal
name=
"WP_parameter create"
expl=
"VC for create"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
steps=
"14"
/></proof>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"14"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter clear"
expl=
"VC for clear"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
steps=
"15"
/></proof>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"17"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter add"
expl=
"VC for add"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.38"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.38"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"22.13"
/></proof>
</goal>
<goal
name=
"WP_parameter get"
expl=
"VC for get"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
steps=
"11"
/></proof>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.00"
steps=
"10"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"WP_parameter remove"
expl=
"VC for remove"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"WP_parameter remove.1"
expl=
"1. precondition"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.04"
steps=
"4"
/></proof>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.04"
steps=
"4"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.2"
expl=
"2. precondition"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
steps=
"10"
/></proof>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"10"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.3"
expl=
"3. precondition"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
steps=
"8"
/></proof>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"8"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.4"
expl=
"4. precondition"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
steps=
"10"
/></proof>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"10"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.5"
expl=
"5. precondition"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
steps=
"11"
/></proof>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.02"
steps=
"11"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.6"
expl=
"6. assertion"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"1.75"
/></proof>
<proof
prover=
"1"
memlimit=
"1000"
><result
status=
"valid"
time=
"1.75"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"1.62"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.7"
expl=
"7. assertion"
>
<proof
prover=
"1"
timelimit=
"76"
><result
status=
"valid"
time=
"
8.94
"
/></proof>
<proof
prover=
"1"
timelimit=
"76"
memlimit=
"1000"
><result
status=
"valid"
time=
"
10.80
"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.8"
expl=
"8.
type invariant
"
>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.0
2
"
steps=
"
1
4"
/></proof>
<goal
name=
"WP_parameter remove.8"
expl=
"8.
assertion
"
>
<proof
prover=
"
0"
timelimit=
"5"
steplimit=
"-1
"
><result
status=
"valid"
time=
"0.0
6
"
steps=
"
3
4"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.9"
expl=
"9. type invariant"
>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.02"
steps=
"
37
"
/></proof>
<proof
prover=
"
0"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.02"
steps=
"
14
"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.10"
expl=
"10. type invariant"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.0
4
"
/></proof>
<proof
prover=
"
0"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.0
2"
steps=
"33
"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.11"
expl=
"11. postcondition"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
steps=
"16"
/></proof>
<goal
name=
"WP_parameter remove.11"
expl=
"11. type invariant"
>
<proof
prover=
"1"
timelimit=
"5"
steplimit=
"-1"
><result
status=
"valid"
time=
"2.35"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.12"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.12"
expl=
"12. postcondition"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
0"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.01"
steps=
"16"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.13"
expl=
"13. p
re
condition"
>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.01"
steps=
"8"
/></proof>
<goal
name=
"WP_parameter remove.13"
expl=
"13. p
ost
condition"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.14"
expl=
"14.
asser
tion"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.
32
"
/></proof>
<goal
name=
"WP_parameter remove.14"
expl=
"14.
precondi
tion"
>
<proof
prover=
"
0"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.
01"
steps=
"8
"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.15"
expl=
"15. assertion"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.
0
2"
/></proof>
<proof
prover=
"
1"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.
3
2"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.16"
expl=
"16.
type invariant
"
>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.0
1"
steps=
"1
2"
/></proof>
<goal
name=
"WP_parameter remove.16"
expl=
"16.
assertion
"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.17"
expl=
"17.
type invariant
"
>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.03"
steps=
"
33
"
/></proof>
<goal
name=
"WP_parameter remove.17"
expl=
"17.
assertion
"
>
<proof
prover=
"
0"
timelimit=
"5"
steplimit=
"-1
"
><result
status=
"valid"
time=
"0.03"
steps=
"
25
"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.18"
expl=
"18. type invariant"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01"
steps=
"12"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.19"
expl=
"19. type invariant"
>
<proof
prover=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.03"
steps=
"28"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.20"
expl=
"20. type invariant"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.1
9
"
expl=
"1
9
. postcondition"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.0
3
"
/></proof>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.0
2"
steps=
"14
"
/></proof>
<goal
name=
"WP_parameter remove.
2
1"
expl=
"
2
1. postcondition"
>
<proof
prover=
"
0"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.0
2"
steps=
"14
"
/></proof>
<proof
prover=
"
1"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.0
3
"
/></proof>
</goal>
<goal
name=
"WP_parameter remove.2
0
"
expl=
"2
0
. postcondition"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<goal
name=
"WP_parameter remove.2
2
"
expl=
"2
2
. postcondition"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
</transf>
</goal>
</theory>
<theory
name=
"Harness"
sum=
"5ec8c49a5e09c3af067f6882a666a776"
expanded=
"true"
>
<theory
name=
"Harness"
sum=
"5ec8c49a5e09c3af067f6882a666a776"
>
<goal
name=
"WP_parameter test1"
expl=
"VC for test1"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"WP_parameter test1.1"
expl=
"1. assertion"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.39"
steps=
"195"
/></proof>
<proof
prover=
"1"
timelimit=
"10"
><result
status=
"valid"
time=
"0.18"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"1.52"
steps=
"249"
/></proof>
<proof
prover=
"0"
timelimit=
"10"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.39"
steps=
"195"
/></proof>
<proof
prover=
"1"
timelimit=
"10"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.18"
/></proof>
<proof
prover=
"3"
timelimit=
"10"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter test1.2"
expl=
"2. assertion"
>
<proof
prover=
"2"
timelimit=
"10"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"3"
timelimit=
"10"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
</transf>
</goal>
...
...
examples/bag/why3shapes.gz
View file @
7e94fa68
No preview for this file type
examples/bitvectors/double/why3session.xml
View file @
7e94fa68
...
...
@@ -2,48 +2,42 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"1"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"Z3"
version=
"2.19"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"CVC4"
version=
"1.4"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"4"
name=
"CVC3"
version=
"2.2"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"5"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"6"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"7"
name=
"Coq"
version=
"8.4pl6"
timelimit=
"30"
memlimit=
"1000"
/>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"1"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"CVC4"
version=
"1.4"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"5"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"8"
name=
"Coq"
version=
"8.5"
timelimit=
"30"
steplimit=
"1"
memlimit=
"1000"
/>
<file
name=
"../double.why"
expanded=
"true"
>
<theory
name=
"BV_double"
sum=
"d41d8cd98f00b204e9800998ecf8427e"
>
</theory>
<theory
name=
"TestDouble"
sum=
"2dfd8f472574f55c4ed59e7a347e128e"
expanded=
"true"
>
<goal
name=
"nth_one1"
expanded=
"true"
>
<proof
prover=
"
6
"
timelimit=
"3"
><result
status=
"valid"
time=
"0.
32
"
steps=
"1
07
"
/></proof>
<proof
prover=
"
0
"
timelimit=
"3"
><result
status=
"valid"
time=
"0.
51
"
steps=
"1
14
"
/></proof>
</goal>
<goal
name=
"nth_one2"
expanded=
"true"
>
<proof
prover=
"
6
"
timelimit=
"3"
><result
status=
"valid"
time=
"0.20"
steps=
"10
5
"
/></proof>
<proof
prover=
"
0
"
timelimit=
"3"
><result
status=
"valid"
time=
"0.20"
steps=
"10
7
"
/></proof>
</goal>
<goal
name=
"nth_one3"
>
<proof
prover=
"
6
"
><result
status=
"valid"
time=
"0.26"
steps=
"1
11
"
/></proof>
<proof
prover=
"
0
"
><result
status=
"valid"
time=
"0.26"
steps=
"1
06
"
/></proof>
</goal>
<goal
name=
"sign_one"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.03"
steps=
"75"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.11"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.11"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.03"
steps=
"75"
/></proof>
</goal>
<goal
name=
"exp_one"
expanded=
"true"
>
<proof
prover=
"
6
"
timelimit=
"30"
><result
status=
"valid"
time=
"
1.44
"
steps=
"
3
05"
/></proof>
<proof
prover=
"
7
"
edited=
"double_TestDouble_exp_one_1.v"
><result
status=
"valid"
time=
"
1.01
"
/></proof>
<proof
prover=
"
0
"
timelimit=
"30"
><result
status=
"valid"
time=
"
2.78
"
steps=
"
8
05"
/></proof>
<proof
prover=
"
8
"
edited=
"double_TestDouble_exp_one_1.v"
><result
status=
"valid"
time=
"
0.70
"
/></proof>
</goal>
<goal
name=
"mantissa_one"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.63"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.36"
/></proof>
<proof
prover=
"5"
timelimit=
"11"
><result
status=
"valid"
time=
"2.74"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.09"
steps=
"105"
/></proof>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.09"
steps=
"87"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.78"
/></proof>
<proof
prover=
"5"
timelimit=
"11"
><result
status=
"valid"
time=
"2.30"
/></proof>
</goal>
<goal
name=
"double_value_of_1"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.04"
steps=
"94"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.04"
steps=
"93"
/></proof>
</goal>
</theory>
</file>
...
...
examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v
View file @
7e94fa68
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
ZArith
.
Require
Import
Rbase
.
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
int
.
Int
.
Require
int
.
Abs
.
Require
int
.
EuclideanDivision
.
Require
bool
.
Bool
.
Require
real
.
Real
.
Require
real
.
RealInfix
.
Require
real
.
FromInt
.
(
*
Why3
assumption
*
)
Definition
implb
(
x
:
bool
)
(
y
:
bool
)
:
bool
:=
match
(
x
,
y
)
with
|
(
true
,
false
)
=>
false
|
(
_
,
_
)
=>
true
end
.
Parameter
pow2
:
Z
->
Z
.
Axiom
Power_0
:
((
pow2
0
%
Z
)
=
1
%
Z
).
...
...
@@ -158,13 +152,29 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Axiom
pow2_63
:
((
pow2
63
%
Z
)
=
9223372036854775808
%
Z
).
Axiom
Div_pow
:
forall
(
x
:
Z
)
(
i
:
Z
),
(((
pow2
(
i
-
1
%
Z
)
%
Z
)
<=
x
)
%
Z
/
\
(
x
<
(
pow2
i
))
%
Z
)
->
((
int
.
EuclideanDivision
.
div
x
(
pow2
(
i
-
1
%
Z
)
%
Z
))
=
1
%
Z
).
Axiom
Div_mult_inst
:
forall
(
x
:
Z
)
(
z
:
Z
),
(
0
%
Z
<
x
)
%
Z
->
((
int
.
EuclideanDivision
.
div
((
x
*
1
%
Z
)
%
Z
+
z
)
%
Z
x
)
=
(
1
%
Z
+
(
int
.
EuclideanDivision
.
div
z
x
))
%
Z
).
Axiom
Div_double
:
forall
(
x
:
Z
)
(
y
:
Z
),
((
0
%
Z
<
y
)
%
Z
/
\
((
y
<=
x
)
%
Z
/
\
(
x
<
(
2
%
Z
*
y
)
%
Z
)
%
Z
))
->
((
int
.
EuclideanDivision
.
div
x
y
)
=
1
%
Z
).
Axiom
Div_pow
:
forall
(
x
:
Z
)
(
i
:
Z
),
(
0
%
Z
<
i
)
%
Z
->
((((
pow2
(
i
-
1
%
Z
)
%
Z
)
<=
x
)
%
Z
/
\
(
x
<
(
pow2
i
))
%
Z
)
->
((
int
.
EuclideanDivision
.
div
x
(
pow2
(
i
-
1
%
Z
)
%
Z
))
=
1
%
Z
)).
Axiom
Div_pow2
:
forall
(
x
:
Z
)
(
i
:
Z
),
(((
-
(
pow2
i
))
%
Z
<=
x
)
%
Z
/
\
(
x
<
(
-
(
pow2
(
i
-
1
%
Z
)
%
Z
))
%
Z
)
%
Z
)
->
((
int
.
EuclideanDivision
.
div
x
(
pow2
(
i
-
1
%
Z
)
%
Z
))
=
(
-
2
%
Z
)
%
Z
).
Axiom
Div_double_neg
:
forall
(
x
:
Z
)
(
y
:
Z
),
((((
-
2
%
Z
)
%
Z
*
y
)
%
Z
<=
x
)
%
Z
/
\
((
x
<
(
-
y
)
%
Z
)
%
Z
/
\
((
-
y
)
%
Z
<
0
%
Z
)
%
Z
))
->
((
int
.
EuclideanDivision
.
div
x
y
)
=
(
-
2
%
Z
)
%
Z
).
Axiom
Div_pow2
:
forall
(
x
:
Z
)
(
i
:
Z
),
(
0
%
Z
<
i
)
%
Z
->
((((
-
(
pow2
i
))
%
Z
<=
x
)
%
Z
/
\
(
x
<
(
-
(
pow2
(
i
-
1
%
Z
)
%
Z
))
%
Z
)
%
Z
)
->
((
int
.
EuclideanDivision
.
div
x
(
pow2
(
i
-
1
%
Z
)
%
Z
))
=
(
-
2
%
Z
)
%
Z
)).
Axiom
Mod_pow2_gen
:
forall
(
x
:
Z
)
(
i
:
Z
)
(
k
:
Z
),
((
0
%
Z
<=
k
)
%
Z
/
\
(
k
<
i
)
%
Z
)
->
((
int
.
EuclideanDivision
.
mod1
(
int
.
EuclideanDivision
.
div
(
x
+
(
pow2
i
))
%
Z
(
pow2
k
))
2
%
Z
)
=
(
int
.
EuclideanDivision
.
mod1
(
int
.
EuclideanDivision
.
div
x
(
pow2
k
))
2
%
Z
)).
Parameter
pow21
:
Z
->
R
.
...
...
@@ -182,7 +192,7 @@ Axiom Power_s_all : forall (n:Z),
Axiom
Power_p_all
:
forall
(
n
:
Z
),
((
pow21
(
n
-
1
%
Z
)
%
Z
)
=
((
05
/
10
)
%
R
*
(
pow21
n
))
%
R
).
Axiom
Power_1_2
:
((
05
/
10
)
%
R
=
(
Rdiv
1
%
R
2
%
R
)
%
R
).
Axiom
Power_1_2
:
((
05
/
10
)
%
R
=
(
1
%
R
/
2
%
R
)
%
R
).
Axiom
Power_11
:
((
pow21
1
%
Z
)
=
2
%
R
).
...
...
@@ -191,11 +201,11 @@ Axiom Power_neg1 : ((pow21 (-1%Z)%Z) = (05 / 10)%R).
Axiom
Power_non_null_aux
:
forall
(
n
:
Z
),
(
0
%
Z
<=
n
)
%
Z
->
~
((
pow21
n
)
=
0
%
R
).
Axiom
Power_neg_aux
:
forall
(
n
:
Z
),
(
0
%
Z
<=
n
)
%
Z
->
((
pow21
(
-
n
)
%
Z
)
=
(
Rdiv
1
%
R
(
pow21
n
))
%
R
).
((
pow21
(
-
n
)
%
Z
)
=
(
1
%
R
/
(
pow21
n
))
%
R
).
Axiom
Power_non_null
:
forall
(
n
:
Z
),
~
((
pow21
n
)
=
0
%
R
).
Axiom
Power_neg
:
forall
(
n
:
Z
),
((
pow21
(
-
n
)
%
Z
)
=
(
Rdiv
1
%
R
(
pow21
n
))
%
R
).
Axiom
Power_neg
:
forall
(
n
:
Z
),
((
pow21
(
-
n
)
%
Z
)
=
(
1
%
R
/
(
pow21
n
))
%
R
).
Axiom
Power_sum_aux
:
forall
(
n
:
Z
)
(
m
:
Z
),
(
0
%
Z
<=
m
)
%
Z
->
((
pow21
(
n
+
m
)
%
Z
)
=
((
pow21
n
)
*
(
pow21
m
))
%
R
).
...
...
@@ -204,11 +214,13 @@ Axiom Power_sum1 : forall (n:Z) (m:Z),
((
pow21
(
n
+
m
)
%
Z
)
=
((
pow21
n
)
*
(
pow21
m
))
%
R
).
Axiom
Pow2_int_real
:
forall
(
x
:
Z
),
(
0
%
Z
<=
x
)
%
Z
->
((
pow21
x
)
=
(
IZR
(
pow2
x
))).
((
pow21
x
)
=
(
Reals
.
Raxioms
.
IZR
(
pow2
x
))).
Axiom
size_positive
:
(
1
%
Z
<
32
%
Z
)
%
Z
.
Parameter
bv
:
Type
.
Axiom
bv
:
Type
.
Parameter
bv_WhyType
:
WhyType
bv
.
Existing
Instance
bv_WhyType
.
Parameter
nth
:
bv
->
Z
->
bool
.
...
...
@@ -223,7 +235,7 @@ Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvone
n
)
=
true
).
(
*
Why3
assumption
*
)
Definition
eq
(
v1
:
bv
)
(
v2
:
bv
)
:
Prop
:=
forall
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
Definition
eq
(
v1
:
bv
)
(
v2
:
bv
)
:
Prop
:=
forall
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
32
%
Z
)
%
Z
)
->
((
nth
v1
n
)
=
(
nth
v2
n
)).
Axiom
extensionality
:
forall
(
v1
:
bv
)
(
v2
:
bv
),
(
eq
v1
v2
)
->
(
v1
=
v2
).
...
...
@@ -231,21 +243,24 @@ Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
Parameter
bw_and
:
bv
->
bv
->
bv
.
Axiom
Nth_bw_and
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
32
%
Z
)
%
Z
)
->
((
nth
(
bw_and
v1
v2
)
n
)
=
(
andb
(
nth
v1
n
)
(
nth
v2
n
))).
(
n
<
32
%
Z
)
%
Z
)
->
((
nth
(
bw_and
v1
v2
)
n
)
=
(
Init
.
Datatypes
.
andb
(
nth
v1
n
)
(
nth
v2
n
))).
Parameter
bw_or
:
bv
->
bv
->
bv
.
Axiom
Nth_bw_or
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
32
%
Z
)
%
Z
)
->
((
nth
(
bw_or
v1
v2
)
n
)
=
(
orb
(
nth
v1
n
)
(
nth
v2
n
))).
(
n
<
32
%
Z
)
%
Z
)
->
((
nth
(
bw_or
v1
v2
)
n
)
=
(
Init
.
Datatypes
.
orb
(
nth
v1
n
)
(
nth
v2
n
))).
Parameter
bw_xor
:
bv
->
bv
->
bv
.
Axiom
Nth_bw_xor
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
32
%
Z
)
%
Z
)
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
xorb
(
nth
v1
n
)
(
nth
v2
n
))).
(
n
<
32
%
Z
)
%
Z
)
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
Init
.
Datatypes
.
xorb
(
nth
v1
n
)
(
nth
v2
n
))).
Axiom
Nth_bw_xor_v1true
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
32
%
Z
)
%
Z
)
/
\
((
nth
v1
n
)
=
true
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
negb
(
nth
v2
n
))).
n
)
=
(
Init
.
Datatypes
.
negb
(
nth
v2
n
))).
Axiom
Nth_bw_xor_v1false
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
32
%
Z
)
%
Z
)
/
\
((
nth
v1
n
)
=
false
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
nth
v2
...
...
@@ -253,7 +268,7 @@ Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
Axiom
Nth_bw_xor_v2true
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
32
%
Z
)
%
Z
)
/
\
((
nth
v2
n
)
=
true
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
negb
(
nth
v1
n
))).
n
)
=
(
Init
.
Datatypes
.
negb
(
nth
v1
n
))).
Axiom
Nth_bw_xor_v2false
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
32
%
Z
)
%
Z
)
/
\
((
nth
v2
n
)
=
false
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
nth
v1
...
...
@@ -262,7 +277,7 @@ Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
Parameter
bw_not
:
bv
->
bv
.
Axiom
Nth_bw_not
:
forall
(
v
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
32
%
Z
)
%
Z
)
->
((
nth
(
bw_not
v
)
n
)
=
(
negb
(
nth
v
n
))).
((
nth
(
bw_not
v
)
n
)
=
(
Init
.
Datatypes
.
negb
(
nth
v
n
))).
Parameter
lsr
:
bv
->
Z
->
bv
.
...
...
@@ -296,19 +311,19 @@ Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
Parameter
to_nat_sub
:
bv
->
Z
->
Z
->
Z
.
Axiom
to_nat_sub_zero
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
((
(
0
%
Z
<=
i
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
/
\
(
j
<
32
%
Z
)
%
Z
)
->
(((
nth
b
j
)
=
false
)
->
((
to_nat_sub
b
j
Axiom
to_nat_sub_zero
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
(
i
<=
j
)
%
Z
/
\
(
j
<
32
%
Z
)
%
Z
)
)
->
(((
nth
b
j
)
=
false
)
->
((
to_nat_sub
b
j
i
)
=
(
to_nat_sub
b
(
j
-
1
%
Z
)
%
Z
i
))).
Axiom
to_nat_sub_one
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
((
(
0
%
Z
<=
i
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
/
\
(
j
<
32
%
Z
)
%
Z
)
->
(((
nth
b
j
)
=
true
)
->
((
to_nat_sub
b
j
Axiom
to_nat_sub_one
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
(
i
<=
j
)
%
Z
/
\
(
j
<
32
%
Z
)
%
Z
)
)
->
(((
nth
b
j
)
=
true
)
->
((
to_nat_sub
b
j
i
)
=
((
pow2
(
j
-
i
)
%
Z
)
+
(
to_nat_sub
b
(
j
-
1
%
Z
)
%
Z
i
))
%
Z
)).
Axiom
to_nat_sub_high
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
(
j
<
i
)
%
Z
->
((
to_nat_sub
b
j
i
)
=
0
%
Z
).
Axiom
to_nat_of_zero2
:
forall
(
b
:
bv
)
(
i
:
Z
)
(
j
:
Z
),
((
(
j
<
32
%
Z
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
/
\
(
0
%
Z
<=
i
)
%
Z
)
->
((
forall
(
k
:
Z
),
((
k
<=
j
)
%
Z
/
\
Axiom
to_nat_of_zero2
:
forall
(
b
:
bv
)
(
i
:
Z
)
(
j
:
Z
),
((
j
<
32
%
Z
)
%
Z
/
\
(
(
i
<=
j
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
Z
)
)
->
((
forall
(
k
:
Z
),
((
k
<=
j
)
%
Z
/
\
(
i
<
k
)
%
Z
)
->
((
nth
b
k
)
=
false
))
->
((
to_nat_sub
b
j
0
%
Z
)
=
(
to_nat_sub
b
i
0
%
Z
))).
...
...
@@ -316,8 +331,8 @@ Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < 32%Z)%Z /\
(
0
%
Z
<=
i
)
%
Z
)
->
((
forall
(
k
:
Z
),
((
k
<=
j
)
%
Z
/
\
(
i
<=
k
)
%
Z
)
->
((
nth
b
k
)
=
false
))
->
((
to_nat_sub
b
j
i
)
=
0
%
Z
)).
Axiom
to_nat_of_one
:
forall
(
b
:
bv
)
(
i
:
Z
)
(
j
:
Z
),
((
(
j
<
32
%
Z
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
/
\
(
0
%
Z
<=
i
)
%
Z
)
->
((
forall
(
k
:
Z
),
((
k
<=
j
)
%
Z
/
\
Axiom
to_nat_of_one
:
forall
(
b
:
bv
)
(
i
:
Z
)
(
j
:
Z
),
((
j
<
32
%
Z
)
%
Z
/
\
(
(
i
<=
j
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
Z
)
)
->
((
forall
(
k
:
Z
),
((
k
<=
j
)
%
Z
/
\
(
i
<=
k
)
%
Z
)
->
((
nth
b
k
)
=
true
))
->
((
to_nat_sub
b
j
i
)
=
((
pow2
((
j
-
i
)
%
Z
+
1
%
Z
)
%
Z
)
-
1
%
Z
)
%
Z
)).
...
...
@@ -374,13 +389,15 @@ Axiom nth_from_int2c_low_odd : forall (n:Z),
Axiom
nth_from_int2c_0
:
forall
(
i
:
Z
),
((
i
<
32
%
Z
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
Z
)
->
((
nth
(
from_int2c
0
%
Z
)
i
)
=
false
).
Axiom
nth_from_int2c_plus_pow2
:
forall
(
x
:
Z
)
(
k
:
Z
)
(
i
:
Z
),
((
0
%
Z
<=
k
)
%
Z
/
\
(
k
<
i
)
%
Z
)
->
((
nth
(
from_int2c
(
x
+
(
pow2
i
))
%
Z
)
k
)
=
(
nth
(
from_int2c
x
)
k
)).
Axiom
nth_from_int2c_plus_pow2
:
forall
(
x
:
Z
)
(
k
:
Z
)
(
i
:
Z
),
((
(
0
%
Z
<=
k
)
%
Z
/
\
(
k
<
i
)
%
Z
)
/
\
(
k
<
(
32
%
Z
-
1
%
Z
)
%
Z
)
%
Z
)
->
((
nth
(
from_int2c
(
x
+
(
pow2
i
))
%
Z
)
k
)
=
(
nth
(
from_int2c
x
)
k
)).
Axiom
size_positive1
:
(
1
%
Z
<
64
%
Z
)
%
Z
.
Parameter
bv1
:
Type
.
Axiom
bv1
:
Type
.
Parameter
bv1_WhyType
:
WhyType
bv1
.
Existing
Instance
bv1_WhyType
.
Parameter
nth1
:
bv1
->
Z
->
bool
.
...
...
@@ -395,7 +412,7 @@ Axiom Nth_one1 : forall (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
((
nth1
bvone1
n
)
=
true
).
(
*
Why3
assumption
*
)
Definition
eq1
(
v1
:
bv1
)
(
v2
:
bv1
)
:
Prop
:=
forall
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
Definition
eq1
(
v1
:
bv1
)
(
v2
:
bv1
)
:
Prop
:=
forall
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
64
%
Z
)
%
Z
)
->
((
nth1
v1
n
)
=
(
nth1
v2
n
)).
Axiom
extensionality1
:
forall
(
v1
:
bv1
)
(
v2
:
bv1
),
(
eq1
v1
v2
)
->
(
v1
=
v2
).
...
...
@@ -403,23 +420,24 @@ Axiom extensionality1 : forall (v1:bv1) (v2:bv1), (eq1 v1 v2) -> (v1 = v2).
Parameter
bw_and1
:
bv1
->
bv1
->
bv1
.
Axiom
Nth_bw_and1
:
forall
(
v1
:
bv1
)
(
v2
:
bv1
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
64
%
Z
)
%
Z
)
->
((
nth1
(
bw_and1
v1
v2
)
n
)
=
(
andb
(
nth1
v1
n
)
(
nth1
v2
n
))).
(
n
<
64
%
Z
)
%
Z
)
->
((
nth1
(
bw_and1
v1
v2
)
n
)
=
(
Init
.
Datatypes
.
andb
(
nth1
v1
n
)
(
nth1
v2
n
))).
Parameter
bw_or1
:
bv1
->
bv1
->
bv1
.
Axiom
Nth_bw_or1
:
forall
(
v1
:
bv1
)
(
v2
:
bv1
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
64
%
Z
)
%
Z
)
->
((
nth1
(
bw_or1
v1
v2
)
n
)
=
(
orb
(
nth1
v1
n
)
(
nth1
v2
n
))).
(
n
<
64
%
Z
)
%
Z
)
->
((
nth1
(
bw_or1
v1
v2
)
n
)
=
(
Init
.
Datatypes
.
orb
(
nth1
v1
n
)
(
nth1
v2
n
))).
Parameter
bw_xor1
:
bv1
->
bv1
->
bv1
.
Axiom
Nth_bw_xor1
:
forall
(
v1
:
bv1
)
(
v2
:
bv1
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
64
%
Z
)
%
Z
)
->
((
nth1
(
bw_xor1
v1
v2
)
n
)
=
(
xorb
(
nth1
v1
n
)
(
nth1
v2
n
))).
(
n
<
64
%
Z
)
%
Z
)
->
((
nth1
(
bw_xor1
v1
v2
)
n
)
=
(
Init
.
Datatypes
.
xorb
(
nth1
v1
n
)
(
nth1
v2
n
))).
Axiom
Nth_bw_xor_v1true1
:
forall
(
v1
:
bv1
)
(
v2
:
bv1
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
64
%
Z
)
%
Z
)
/
\
((
nth1
v1
n
)
=
true
))
->
((
nth1
(
bw_xor1
v1
v2
)
n
)
=
(
negb
(
nth1
v2
n
))).
n
)
=
(
Init
.
Datatypes
.
negb
(
nth1
v2
n
))).
Axiom
Nth_bw_xor_v1false1
:
forall
(
v1
:
bv1
)
(
v2
:
bv1
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
64
%
Z
)
%
Z
)
/
\
((
nth1
v1
n
)
=
false
))
->
((
nth1
(
bw_xor1
v1
v2
)
...
...
@@ -427,7 +445,7 @@ Axiom Nth_bw_xor_v1false1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
Axiom
Nth_bw_xor_v2true1
:
forall
(
v1
:
bv1
)
(
v2
:
bv1
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
64
%
Z
)
%
Z
)
/
\
((
nth1
v2
n
)
=
true
))
->
((
nth1
(
bw_xor1
v1
v2
)
n
)
=
(
negb
(
nth1
v1
n
))).
n
)
=
(
Init
.
Datatypes
.
negb
(
nth1
v1
n
))).
Axiom
Nth_bw_xor_v2false1
:
forall
(
v1
:
bv1
)
(
v2
:
bv1
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
64
%
Z
)
%
Z
)
/
\
((
nth1
v2
n
)
=
false
))
->
((
nth1
(
bw_xor1
v1
v2
)
...
...
@@ -436,7 +454,7 @@ Axiom Nth_bw_xor_v2false1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
Parameter
bw_not1
:
bv1
->
bv1
.
Axiom
Nth_bw_not1
:
forall
(
v
:
bv1
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
64
%
Z
)
%
Z
)
->
((
nth1
(
bw_not1
v
)
n
)
=
(
negb
(
nth1
v
n
))).
((
nth1
(
bw_not1
v
)
n
)
=
(
Init
.
Datatypes
.
negb
(
nth1
v
n
))).
Parameter
lsr1
:
bv1
->
Z
->
bv1
.
...
...
@@ -470,19 +488,19 @@ Axiom lsl_nth_low1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
Parameter
to_nat_sub1
:
bv1
->
Z
->
Z
->
Z
.
Axiom
to_nat_sub_zero1
:
forall
(
b
:
bv1
)
(
j
:
Z
)
(
i
:
Z
),
((
(
0
%
Z
<=
i
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
/
\
(
j
<
64
%
Z
)
%
Z
)
->
(((
nth1
b
j
)
=
false
)
->
((
to_nat_sub1
b
j
Axiom
to_nat_sub_zero1
:
forall
(
b
:
bv1
)
(
j
:
Z
)
(
i
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
(
i
<=
j
)
%
Z
/
\
(
j
<
64
%
Z
)
%
Z
)
)
->
(((
nth1
b
j
)
=
false
)
->
((
to_nat_sub1
b
j
i
)
=
(
to_nat_sub1
b
(
j
-
1
%
Z
)
%
Z
i
))).
Axiom
to_nat_sub_one1
:
forall
(
b
:
bv1
)
(
j
:
Z
)
(
i
:
Z
),
((
(
0
%
Z
<=
i
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
/
\
(
j
<
64
%
Z
)
%
Z
)
->
(((
nth1
b
j
)
=
true
)
->
((
to_nat_sub1
b
j
Axiom
to_nat_sub_one1
:
forall
(
b
:
bv1
)
(
j
:
Z
)
(
i
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
(
i
<=
j
)
%
Z
/
\
(
j
<
64
%
Z
)
%
Z
)
)
->
(((
nth1
b
j
)
=
true
)
->
((
to_nat_sub1
b
j