It really depends on whether you consider adding arrays to this project is valuable (!26 ). Maybe not everything in this MR is necessary. I can look into each lemma in details. However, things like multiplication and comparisons are going to be useful.
This is the first MR to split !26 into multiple ones.
Jason Hu (d9797ee5) at 22 Dec 23:20
add more operations to the language
OK I will reorganize a bit. stay tuned.
Jason Hu (1fd580db) at 01 Aug 20:54
add an inversion lemma
please kindly review and advise if my additions make sense
Jason Hu (817867e7) at 01 Aug 18:36
add reasoning for booleans
Jason Hu (3aa73650) at 01 Aug 15:22
Merge remote-tracking branch 'origin/master' into bounded
... and 1 more commit
please kindly review and advise if my additions make sense