Commit 96f69b5e authored by Stefan Berghofer's avatar Stefan Berghofer Committed by Sylvain Dailler

Improved checking of realizations for Isabelle

Rather than using pre-generated files, the *.xml files describing the
Why3 theories to be realized are generated again before compiling the
corresponding Isabelle theories. Instead of the generated *.xml files,
we use a file containing their hash values to detect changes in the
realizations. Since there may be different realizations for different
versions of Isabelle, we provide a file with hash values for every
supported version of Isabelle. The files containing the hash values
can be updated via the update-isabelle target.

(cherry picked from commit 039e0f0a321c36ea3bea231e4376f5833cd2ad8a)
parent cba18b81
......@@ -126,7 +126,7 @@ TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
# Variables added for checking realizations
GENERATED_PREFIX_COQ="lib/coq"
GENERATED_PREFIX_ISABELLE="lib/isabelle"
GENERATED_PREFIX_ISABELLE=lib/isabelle
###############
# main target
......@@ -1283,28 +1283,30 @@ clean::
rm -f $(ISABELLEVERSIONSPECIFICTARGETS)
ISABELLELIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELIBS_INT_FILES)))
ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/int/, $(ISABELLELIBS_INT_FILES)))
ISABELLELIBS_BOOL_FILES = Bool
ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix lib/isabelle/bool/, $(ISABELLELIBS_BOOL_FILES)))
ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/bool/, $(ISABELLELIBS_BOOL_FILES)))
ISABELLELIBS_REAL_FILES = Real RealInfix Abs MinMax FromInt Truncate Square ExpLog Trigonometry PowerInt # not yet realized : PowerReal Hyperbolic Polar
ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix lib/isabelle/real/, $(ISABELLELIBS_REAL_FILES)))
ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/real/, $(ISABELLELIBS_REAL_FILES)))
ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix lib/isabelle/number/, $(ISABELLELIBS_NUMBER_FILES)))
ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/number/, $(ISABELLELIBS_NUMBER_FILES)))
ISABELLELIBS_SET_FILES = Set Fset
ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix lib/isabelle/set/, $(ISABELLELIBS_SET_FILES)))
ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/set/, $(ISABELLELIBS_SET_FILES)))
ISABELLELIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix lib/isabelle/map/, $(ISABELLELIBS_MAP_FILES)))
ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/map/, $(ISABELLELIBS_MAP_FILES)))
ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut
ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix lib/isabelle/list/, $(ISABELLELIBS_LIST_FILES)))
ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/list/, $(ISABELLELIBS_LIST_FILES)))
ISABELLELIBS_BV_FILES = Pow2int BV8 BV16 BV32 BV64 BVConverter_32_64 BVConverter_16_64 BVConverter_8_64 BVConverter_16_32 BVConverter_8_32 BVConverter_8_16
ISABELLELIBS_BV = $(addsuffix .xml, $(addprefix lib/isabelle/bv/, $(ISABELLELIBS_BV_FILES)))
ISABELLELIBS_BV = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/bv/, $(ISABELLELIBS_BV_FILES)))
ISABELLELIBS = $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
drivers/isabelle-realizations.aux: Makefile
$(SHOW) 'Generate $@'
......@@ -1336,7 +1338,10 @@ else
ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
endif
update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
$(GENERATED_PREFIX_ISABELLE)/realizations.@ISABELLEVERSION@: $(ISABELLELIBS)
$(HIDE)sha1sum $^ | sed -e "s,$(GENERATED_PREFIX_ISABELLE)/,," > $@
update-isabelle: $(GENERATED_PREFIX_ISABELLE)/realizations.@ISABELLEVERSION@
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/int.why
......@@ -1392,11 +1397,9 @@ $(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.au
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bv
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bv/
$(GENERATED_PREFIX_ISABELLE)/last_build: $(ISABELLEVERSIONSPECIFICTARGETS)
# $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
ifeq (@enable_isabelle_libs@,yes)
$(GENERATED_PREFIX_ISABELLE)/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS)
ifneq (@enable_local@,yes)
cp -r $(GENERATED_PREFIX_ISABELLE) "$(LIBDIR)/why3"
endif
......@@ -1410,41 +1413,20 @@ endif
echo " [$(ISABELLE_TARGET_DIR)]"; \
fi)
install_no_local::
$(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
install_no_local:: $(GENERATED_PREFIX_ISABELLE)/last_build
install_local:: $(GENERATED_PREFIX_ISABELLE)/last_build
clean::
rm -f $(GENERATED_PREFIX_ISABELLE)/*/*.xml
# do not update isabelle realizations systematically
# all: update-isabelle
# Removed cleaning of xml
#clean::
# rm -f $(GENERATED_PREFIX_ISABELLE)/*/*.xml
endif
else
all: drivers/isabelle-realizations.aux
install_no_local::
$(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
install_no_local:: $(GENERATED_PREFIX_ISABELLE)/last_build
install_local:: $(GENERATED_PREFIX_ISABELLE)/last_build
# do not update isabelle realizations systematically
# all: update-isabelle
# Removed cleaning of xml
#clean::
# rm -f $(GENERATED_PREFIX_ISABELLE)/*/*.xml
endif
all: drivers/isabelle-realizations.aux
clean::
rm -f drivers/isabelle-realizations.aux
......
......@@ -6,15 +6,13 @@ mkdir -p $TMPREAL/lib
res=0
echo "Testing Isabelle realizations"
# First copy current realizations in a tmp directory
cp -r lib/isabelle $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
LANG=C diff -r -q -x '*.bak' -x '*~' -x '*.aux' lib/isabelle $TMPREAL/lib/isabelle > $TMPREAL/diff-isabelle
LANG=C diff lib/isabelle $TMPREAL/lib/isabelle/realizations.* > $TMPREAL/diff-isabelle
if test -s "$TMPREAL/diff-isabelle"; then
echo "Isabelle realizations FAILED, please regenerate and prove them"
sed -e "s,$TMPREAL/lib/isabelle,new," $TMPREAL/diff-isabelle
cat $TMPREAL/diff-isabelle
res=1
else
echo "Isabelle realizations OK"
......
<theory name="bool.Bool" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/></realized><lemma name="andb_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.conj"/><var name="x"><type name="HOL.bool"/></var><var name="y"><type name="HOL.bool"/></var></app><case><var name="x"><type name="HOL.bool"/></var><pat><const name="HOL.True"/><var name="y"><type name="HOL.bool"/></var></pat><pat><const name="HOL.False"/><const name="HOL.False"/></pat></case></app></concls></lemma><lemma name="orb_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.disj"/><var name="x"><type name="HOL.bool"/></var><var name="y"><type name="HOL.bool"/></var></app><case><var name="x"><type name="HOL.bool"/></var><pat><const name="HOL.False"/><var name="y"><type name="HOL.bool"/></var></pat><pat><const name="HOL.True"/><const name="HOL.True"/></pat></case></app></concls></lemma><lemma name="notb_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.Not"/><var name="x"><type name="HOL.bool"/></var></app><case><var name="x"><type name="HOL.bool"/></var><pat><const name="HOL.False"/><const name="HOL.True"/></pat><pat><const name="HOL.True"/><const name="HOL.False"/></pat></case></app></concls></lemma><lemma name="xorb_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="x"><type name="HOL.bool"/></var><var name="y"><type name="HOL.bool"/></var></app></app><case><var name="x"><type name="HOL.bool"/></var><pat><const name="HOL.False"/><var name="y"><type name="HOL.bool"/></var></pat><pat><const name="HOL.True"/><app><const name="HOL.Not"/><var name="y"><type name="HOL.bool"/></var></app></pat></case></app></concls></lemma><lemma name="implb_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.implies"/><var name="x"><type name="HOL.bool"/></var><var name="y"><type name="HOL.bool"/></var></app><case><var name="x"><type name="HOL.bool"/></var><pat><const name="HOL.False"/><const name="HOL.True"/></pat><pat><const name="HOL.True"/><var name="y"><type name="HOL.bool"/></var></pat></case></app></concls></lemma></theory>
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
<theory name="bv.BVConverter_16_32" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV32"/><require name="bv.BV16"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_16_32"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV32"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_16_32"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV16"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_16_32"><prems><app><const name="ule" path="bv.BV32"><pred><type name="t" path="bv.BV32"/><type name="t" path="bv.BV32"/></pred></const><var name="x"><type name="t" path="bv.BV32"/></var><num val="65535"><type name="t" path="bv.BV32"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV16"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_16_32"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV32"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="bv.BVConverter_16_64" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV64"/><require name="bv.BV16"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_16_64"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV64"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_16_64"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV16"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_16_64"><prems><app><const name="ule" path="bv.BV64"><pred><type name="t" path="bv.BV64"/><type name="t" path="bv.BV64"/></pred></const><var name="x"><type name="t" path="bv.BV64"/></var><num val="65535"><type name="t" path="bv.BV64"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV16"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_16_64"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV64"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="bv.BVConverter_32_64" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV64"/><require name="bv.BV32"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_32_64"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV64"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_32_64"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV32"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_32_64"><prems><app><const name="ule" path="bv.BV64"><pred><type name="t" path="bv.BV64"/><type name="t" path="bv.BV64"/></pred></const><var name="x"><type name="t" path="bv.BV64"/></var><num val="4294967295"><type name="t" path="bv.BV64"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV32"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_32_64"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV64"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="bv.BVConverter_8_16" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV16"/><require name="bv.BV8"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_8_16"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV16"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_8_16"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV8"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_8_16"><prems><app><const name="ule" path="bv.BV16"><pred><type name="t" path="bv.BV16"/><type name="t" path="bv.BV16"/></pred></const><var name="x"><type name="t" path="bv.BV16"/></var><num val="255"><type name="t" path="bv.BV16"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV8"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_8_16"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV16"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="bv.BVConverter_8_32" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV32"/><require name="bv.BV8"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_8_32"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV32"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_8_32"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV8"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_8_32"><prems><app><const name="ule" path="bv.BV32"><pred><type name="t" path="bv.BV32"/><type name="t" path="bv.BV32"/></pred></const><var name="x"><type name="t" path="bv.BV32"/></var><num val="255"><type name="t" path="bv.BV32"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV8"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_8_32"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV32"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="bv.BVConverter_8_64" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV64"/><require name="bv.BV8"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_8_64"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV64"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_8_64"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV8"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_8_64"><prems><app><const name="ule" path="bv.BV64"><pred><type name="t" path="bv.BV64"/><type name="t" path="bv.BV64"/></pred></const><var name="x"><type name="t" path="bv.BV64"/></var><num val="255"><type name="t" path="bv.BV64"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV8"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_8_64"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV64"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
This diff is collapsed.
<theory name="int.Abs" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/></realized><lemma name="abs_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Int.int"/></var></app><app><const name="HOL.If"/><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="x"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var><app><const name="Groups.uminus_class.uminus"/><var name="x"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Abs_le" altname="Abs_le" path="int.Abs"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Int.int"/></var></app><var name="y"><type name="Int.int"/></var></app><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.uminus_class.uminus"/><var name="y"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Abs_pos" altname="Abs_pos" path="int.Abs"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Int.int"/></var></app></app></concls></lemma></theory>
\ No newline at end of file
This diff is collapsed.
<theory name="int.Div2" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/></realized><lemma name="div2" altname="div2" path="int.Div2"><prems/><concls><app><const name="HOL.Ex"/><abs name="y"><type name="Int.int"/><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="x"><type name="Int.int"/></var><app><const name="Groups.times_class.times"/><num val="2"><type name="Int.int"/></num><var name="y"><type name="Int.int"/></var></app></app><app><const name="HOL.eq"/><var name="x"><type name="Int.int"/></var><app><const name="Groups.plus_class.plus"/><app><const name="Groups.times_class.times"/><num val="2"><type name="Int.int"/></num><var name="y"><type name="Int.int"/></var></app><num val="1"><type name="Int.int"/></num></app></app></app></abs></app></concls></lemma></theory>
\ No newline at end of file
This diff is collapsed.
<theory name="int.Int" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/></realized><lemma name="infix_lseq_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="HOL.disj"/><app><const name="Orderings.ord_class.less"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="HOL.eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Assoc" altname="Assoc" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.plus_class.plus"/><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><var name="z"><type name="Int.int"/></var></app><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Int.int"/></var><app><const name="Groups.plus_class.plus"/><var name="y"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Unit_def_l" altname="Unit_def_l" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.plus_class.plus"/><num val="0"><type name="Int.int"/></num><var name="x"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var></app></concls></lemma><lemma name="Unit_def_r" altname="Unit_def_r" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app><var name="x"><type name="Int.int"/></var></app></concls></lemma><lemma name="Inv_def_l" altname="Inv_def_l" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.plus_class.plus"/><app><const name="Groups.uminus_class.uminus"/><var name="x"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var></app><num val="0"><type name="Int.int"/></num></app></concls></lemma><lemma name="Inv_def_r" altname="Inv_def_r" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Int.int"/></var><app><const name="Groups.uminus_class.uminus"/><var name="x"><type name="Int.int"/></var></app></app><num val="0"><type name="Int.int"/></num></app></concls></lemma><lemma name="Comm" altname="Comm" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Groups.plus_class.plus"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="Assoc1" altname="Assoc" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><var name="z"><type name="Int.int"/></var></app><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><app><const name="Groups.times_class.times"/><var name="y"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Mul_distr_l" altname="Mul_distr_l" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><app><const name="Groups.plus_class.plus"/><var name="y"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></app><app><const name="Groups.plus_class.plus"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Mul_distr_r" altname="Mul_distr_r" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><app><const name="Groups.plus_class.plus"/><var name="y"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var></app><app><const name="Groups.plus_class.plus"/><app><const name="Groups.times_class.times"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app><app><const name="Groups.times_class.times"/><var name="z"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="infix_mn_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.minus_class.minus"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Int.int"/></var><app><const name="Groups.uminus_class.uminus"/><var name="y"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Comm1" altname="Comm" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Groups.times_class.times"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="Unitary" altname="Unitary" path="int.Int"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><num val="1"><type name="Int.int"/></num><var name="x"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var></app></concls></lemma><lemma name="NonTrivialRing" altname="NonTrivialRing" path="int.Int"><prems/><concls><app><const name="HOL.Not"/><app><const name="HOL.eq"/><num val="0"><type name="Int.int"/></num><num val="1"><type name="Int.int"/></num></app></app></concls></lemma><lemma name="Refl" altname="Refl" path="int.Int"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></concls></lemma><lemma name="Trans" altname="Trans" path="int.Int"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><var name="y"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></concls></lemma><lemma name="Antisymm" altname="Antisymm" path="int.Int"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></concls></lemma><lemma name="Total" altname="Total" path="int.Int"><prems/><concls><app><const name="HOL.disj"/><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="ZeroLessOne" altname="ZeroLessOne" path="int.Int"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><num val="1"><type name="Int.int"/></num></app></concls></lemma><lemma name="CompatOrderAdd" altname="CompatOrderAdd" path="int.Int"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app><app><const name="Groups.plus_class.plus"/><var name="y"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="CompatOrderMult" altname="CompatOrderMult" path="int.Int"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="z"><type name="Int.int"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app><app><const name="Groups.times_class.times"/><var name="y"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="int.MinMax" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/></realized><lemma name="min_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.min"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="HOL.If"/><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="max_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.max"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="HOL.If"/><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="Min_r" altname="Min_r" path="int.MinMax"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.min"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><var name="y"><type name="Int.int"/></var></app></concls></lemma><lemma name="Max_l" altname="Max_l" path="int.MinMax"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.max"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var></app></concls></lemma><lemma name="Min_comm" altname="Min_comm" path="int.MinMax"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.min"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.min"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="Max_comm" altname="Max_comm" path="int.MinMax"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.max"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.max"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="Min_assoc" altname="Min_assoc" path="int.MinMax"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.min"/><app><const name="Orderings.ord_class.min"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><var name="z"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.min"/><var name="x"><type name="Int.int"/></var><app><const name="Orderings.ord_class.min"/><var name="y"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Max_assoc" altname="Max_assoc" path="int.MinMax"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.max"/><app><const name="Orderings.ord_class.max"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><var name="z"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.max"/><var name="x"><type name="Int.int"/></var><app><const name="Orderings.ord_class.max"/><var name="y"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="int.Power" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/></realized><lemma name="Power_0" altname="Power_0" path="int.Power"><prems/><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><num val="0"><type name="Int.int"/></num></app></app><num val="1"><type name="Int.int"/></num></app></concls></lemma><lemma name="Power_s" altname="Power_s" path="int.Power"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><app><const name="Groups.plus_class.plus"/><var name="n"><type name="Int.int"/></var><num val="1"><type name="Int.int"/></num></app></app></app><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app></app></app></concls></lemma><lemma name="Power_s_alt" altname="Power_s_alt" path="int.Power"><prems><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><app><const name="Groups.minus_class.minus"/><var name="n"><type name="Int.int"/></var><num val="1"><type name="Int.int"/></num></app></app></app></app></app></concls></lemma><lemma name="Power_1" altname="Power_1" path="int.Power"><prems/><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><num val="1"><type name="Int.int"/></num></app></app><var name="x"><type name="Int.int"/></var></app></concls></lemma><lemma name="Power_sum" altname="Power_sum" path="int.Power"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="m"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><app><const name="Groups.plus_class.plus"/><var name="n"><type name="Int.int"/></var><var name="m"><type name="Int.int"/></var></app></app></app><app><const name="Groups.times_class.times"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="m"><type name="Int.int"/></var></app></app></app></app></concls></lemma><lemma name="Power_mult" altname="Power_mult" path="int.Power"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="m"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><app><const name="Groups.times_class.times"/><var name="n"><type name="Int.int"/></var><var name="m"><type name="Int.int"/></var></app></app></app><app><const name="Power.power_class.power"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Int.nat"/><var name="m"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Power_comm1" altname="Power_comm1" path="int.Power"><prems><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Groups.times_class.times"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><var name="y"><type name="Int.int"/></var></app><app><const name="Groups.times_class.times"/><var name="y"><type name="Int.int"/></var><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app></app></app></concls></lemma><lemma name="Power_comm2" altname="Power_comm2" path="int.Power"><prems><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Groups.times_class.times"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Groups.times_class.times"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Power.power_class.power"/><var name="y"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app></app></app></concls></lemma><lemma name="Power_non_neg" altname="Power_non_neg" path="int.Power"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="x"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="y"><type name="Int.int"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="y"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Power_monotonic" altname="Power_monotonic" path="int.Power"><prems><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Int.int"/></num><var name="x"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><var name="n"><type name="Int.int"/></var><var name="m"><type name="Int.int"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Power.power_class.power"/><var name="x"><type name="Int.int"/></var><app><const name="Int.nat"/><var name="m"><type name="Int.int"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.Append" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/><require name="list.Length"/><require name="list.Mem"/></realized><lemma name="infix_plpl_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><case><var name="l1"><type name="List.list"><tvar name="a"/></type></var><pat><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const><var name="l2"><type name="List.list"><tvar name="a"/></type></var></pat><pat><app><const name="List.list.Cons"/><var name="x1"><tvar name="a"/></var><var name="r1"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.list.Cons"/><var name="x1"><tvar name="a"/></var><app><const name="List.append"/><var name="r1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></pat></case></app></concls></lemma><lemma name="Append_assoc" altname="Append_assoc" path="list.Append"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><app><const name="List.append"/><var name="l2"><type name="List.list"><tvar name="a"/></type></var><var name="l3"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="List.append"/><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><var name="l3"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma><lemma name="Append_l_nil" altname="Append_l_nil" path="list.Append"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.append"/><var name="l"><type name="List.list"><tvar name="a"/></type></var><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const></app><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></concls></lemma><lemma name="Append_length" altname="Append_length" path="list.Append"><prems/><concls><app><const name="HOL.eq"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></app><app><const name="Groups.plus_class.plus"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></app></app></concls></lemma><lemma name="mem_append" altname="mem_append" path="list.Append"><prems/><concls><app><const name="HOL.eq"/><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></app><app><const name="HOL.disj"/><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></app></app></concls></lemma><lemma name="mem_decomp" altname="mem_decomp" path="list.Append"><prems><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></prems><concls><app><const name="HOL.Ex"/><abs name="l1"><type name="List.list"><tvar name="a"/></type><app><const name="HOL.Ex"/><abs name="l2"><type name="List.list"><tvar name="a"/></type><app><const name="HOL.eq"/><var name="l"><type name="List.list"><tvar name="a"/></type></var><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></app></abs></app></abs></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.Combine" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="list.List"/></realized><function><eqn altname="combine" path="list.Combine"><app><const name="HOL.eq"/><app><var name="combine"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="b"/></type><type name="List.list"><prodt><tvar name="a"/><tvar name="b"/></prodt></type></fun></var><var name="x"><type name="List.list"><tvar name="a"/></type></var><var name="y"><type name="List.list"><tvar name="b"/></type></var></app><case><prod><var name="x"><type name="List.list"><tvar name="a"/></type></var><var name="y"><type name="List.list"><tvar name="b"/></type></var></prod><pat><prod><app><const name="List.list.Cons"/><var name="x0"><tvar name="a"/></var><var name="x1"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.list.Cons"/><var name="y0"><tvar name="b"/></var><var name="y1"><type name="List.list"><tvar name="b"/></type></var></app></prod><app><const name="List.list.Cons"/><prod><var name="x0"><tvar name="a"/></var><var name="y0"><tvar name="b"/></var></prod><app><var name="combine"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="b"/></type><type name="List.list"><prodt><tvar name="a"/><tvar name="b"/></prodt></type></fun></var><var name="x1"><type name="List.list"><tvar name="a"/></type></var><var name="y1"><type name="List.list"><tvar name="b"/></type></var></app></app></pat><pat><const name="Pure.dummy_pattern"/><const name="List.list.Nil"><type name="List.list"><prodt><tvar name="a"/><tvar name="b"/></prodt></type></const></pat></case></app></eqn></function></theory>
\ No newline at end of file
<theory name="list.Distinct" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/><require name="list.Length"/><require name="list.Mem"/><require name="list.Append"/></realized><lemma name="distinct_zero" altname="distinct_zero" path="list.Distinct"><prems/><concls><app><const name="List.distinct"/><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const></app></concls></lemma><lemma name="distinct_one" altname="distinct_one" path="list.Distinct"><prems/><concls><app><const name="List.distinct"/><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const></app></app></concls></lemma><lemma name="distinct_many" altname="distinct_many" path="list.Distinct"><prems><app><const name="HOL.Not"/><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></app><app><const name="List.distinct"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></prems><concls><app><const name="List.distinct"/><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma><lemma name="distinct_append" altname="distinct_append" path="list.Distinct"><prems><app><const name="List.distinct"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.distinct"/><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="HOL.All"/><abs name="x"><tvar name="a"/><app><const name="HOL.implies"/><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="HOL.Not"/><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></app></app></abs></app></prems><concls><app><const name="List.distinct"/><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.HdTl" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="list.List"/></realized><definition altname="hd" path="list.HdTl"><app><const name="HOL.eq"/><app><var name="hd"><fun><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><case><var name="l"><type name="List.list"><tvar name="a"/></type></var><pat><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const><const name="Option.option.None"><type name="Option.option"><tvar name="a"/></type></const></pat><pat><app><const name="List.list.Cons"/><var name="h"><tvar name="a"/></var><const name="Pure.dummy_pattern"/></app><app><const name="Option.option.Some"/><var name="h"><tvar name="a"/></var></app></pat></case></app></definition><definition altname="tl" path="list.HdTl"><app><const name="HOL.eq"/><app><var name="tl"><fun><type name="List.list"><tvar name="a"/></type><type name="Option.option"><type name="List.list"><tvar name="a"/></type></type></fun></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><case><var name="l"><type name="List.list"><tvar name="a"/></type></var><pat><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const><const name="Option.option.None"><type name="Option.option"><type name="List.list"><tvar name="a"/></type></type></const></pat><pat><app><const name="List.list.Cons"/><const name="Pure.dummy_pattern"/><var name="t"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="Option.option.Some"/><var name="t"><type name="List.list"><tvar name="a"/></type></var></app></pat></case></app></definition></theory>
\ No newline at end of file
<theory name="list.HdTlNoOpt" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="list.List"/></realized><lemma name="hd_cons" altname="hd_cons" path="list.HdTlNoOpt"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.list.hd"/><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app></app><var name="x"><tvar name="a"/></var></app></concls></lemma><lemma name="tl_cons" altname="tl_cons" path="list.HdTlNoOpt"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.list.tl"/><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app></app><var name="r"><type name="List.list"><tvar name="a"/></type></var></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.Length" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/></realized><lemma name="length_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><case><var name="l"><type name="List.list"><tvar name="a"/></type></var><pat><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const><num val="0"><type name="Int.int"/></num></pat><pat><app><const name="List.list.Cons"/><const name="Pure.dummy_pattern"/><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="Groups.plus_class.plus"/><num val="1"><type name="Int.int"/></num><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="r"><type name="List.list"><tvar name="a"/></type></var></app></app></app></pat></case></app></concls></lemma><lemma name="Length_nonnegative" altname="Length_nonnegative" path="list.Length"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma><lemma name="Length_nil" altname="Length_nil" path="list.Length"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.eq"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><num val="0"><type name="Int.int"/></num></app><app><const name="HOL.eq"/><var name="l"><type name="List.list"><tvar name="a"/></type></var><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.List" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/></realized></theory>
\ No newline at end of file
<theory name="list.Mem" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="list.List"/></realized><lemma name="mem_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><case><var name="l"><type name="List.list"><tvar name="a"/></type></var><pat><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const><const name="HOL.False"/></pat><pat><app><const name="List.list.Cons"/><var name="y"><tvar name="a"/></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="x"><tvar name="a"/></var><var name="y"><tvar name="a"/></var></app><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="r"><type name="List.list"><tvar name="a"/></type></var></app></app></app></pat></case></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.Nth" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/></realized><function><eqn altname="nth" path="list.Nth"><app><const name="HOL.eq"/><app><var name="nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></var><var name="n"><type name="Int.int"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><case><var name="l"><type name="List.list"><tvar name="a"/></type></var><pat><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const><const name="Option.option.None"><type name="Option.option"><tvar name="a"/></type></const></pat><pat><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="HOL.If"/><app><const name="HOL.eq"/><var name="n"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app><app><const name="Option.option.Some"/><var name="x"><tvar name="a"/></var></app><app><var name="nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></var><app><const name="Groups.minus_class.minus"/><var name="n"><type name="Int.int"/></var><num val="1"><type name="Int.int"/></num></app><var name="r"><type name="List.list"><tvar name="a"/></type></var></app></app></pat></case></app></eqn></function></theory>
\ No newline at end of file
<theory name="list.NthHdTl" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/><require name="list.Nth"/><require name="list.HdTl"/></realized><lemma name="Nth_tl" altname="Nth_tl" path="list.NthHdTl"><prems><app><const name="HOL.eq"/><app><const name="tl" path="list.HdTl"><fun><type name="List.list"><tvar name="a"/></type><type name="Option.option"><type name="List.list"><tvar name="a"/></type></type></fun></const><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="Option.option.Some"/><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="i"><type name="Int.int"/></var><app><const name="Groups.uminus_class.uminus"/><num val="1"><type name="Int.int"/></num></app></app></app></prems><concls><app><const name="HOL.eq"/><app><const name="nth" path="list.Nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><var name="i"><type name="Int.int"/></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="nth" path="list.Nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><app><const name="Groups.plus_class.plus"/><var name="i"><type name="Int.int"/></var><num val="1"><type name="Int.int"/></num></app><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma><lemma name="Nth0_head" altname="Nth0_head" path="list.NthHdTl"><prems/><concls><app><const name="HOL.eq"/><app><const name="nth" path="list.Nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><num val="0"><type name="Int.int"/></num><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="hd" path="list.HdTl"><fun><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.NthLength" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/><require name="list.Length"/><require name="list.Nth"/></realized><lemma name="nth_none_1" altname="nth_none_1" path="list.NthLength"><prems><app><const name="Orderings.ord_class.less"/><var name="i"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="nth" path="list.Nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><var name="i"><type name="Int.int"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><const name="Option.option.None"><type name="Option.option"><tvar name="a"/></type></const></app></concls></lemma><lemma name="nth_none_2" altname="nth_none_2" path="list.NthLength"><prems><app><const name="Orderings.ord_class.less_eq"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><var name="i"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="nth" path="list.Nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><var name="i"><type name="Int.int"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><const name="Option.option.None"><type name="Option.option"><tvar name="a"/></type></const></app></concls></lemma><lemma name="nth_none_3" altname="nth_none_3" path="list.NthLength"><prems><app><const name="HOL.eq"/><app><const name="nth" path="list.Nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><var name="i"><type name="Int.int"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><const name="Option.option.None"><type name="Option.option"><tvar name="a"/></type></const></app></prems><concls><app><const name="HOL.disj"/><app><const name="Orderings.ord_class.less"/><var name="i"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app><app><const name="Orderings.ord_class.less_eq"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><var name="i"><type name="Int.int"/></var></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.NthLengthAppend" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/><require name="list.Length"/><require name="list.Mem"/><require name="list.Nth"/><require name="list.NthLength"/><require name="list.Append"/></realized><lemma name="nth_append_1" altname="nth_append_1" path="list.NthLengthAppend"><prems><app><const name="Orderings.ord_class.less"/><var name="i"><type name="Int.int"/></var><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app></app></prems><concls><app><const name="HOL.eq"/><app><const name="nth" path="list.Nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><var name="i"><type name="Int.int"/></var><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="nth" path="list.Nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><var name="i"><type name="Int.int"/></var><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma><lemma name="nth_append_2" altname="nth_append_2" path="list.NthLengthAppend"><prems><app><const name="Orderings.ord_class.less_eq"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app><var name="i"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="nth" path="list.Nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><var name="i"><type name="Int.int"/></var><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="nth" path="list.Nth"><fun><type name="Int.int"/><type name="List.list"><tvar name="a"/></type><type name="Option.option"><tvar name="a"/></type></fun></const><app><const name="Groups.minus_class.minus"/><var name="i"><type name="Int.int"/></var><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app></app><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.NthNoOpt" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/></realized><lemma name="nth_cons_0" altname="nth_cons_0" path="list.NthNoOpt"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.nth"/><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="Int.nat"/><num val="0"><type name="Int.int"/></num></app></app><var name="x"><tvar name="a"/></var></app></concls></lemma><lemma name="nth_cons_n" altname="nth_cons_n" path="list.NthNoOpt"><prems><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="List.nth"/><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="List.nth"/><var name="r"><type name="List.list"><tvar name="a"/></type></var><app><const name="Int.nat"/><app><const name="Groups.minus_class.minus"/><var name="n"><type name="Int.int"/></var><num val="1"><type name="Int.int"/></num></app></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.NumOcc" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/><require name="list.Length"/><require name="list.Mem"/><require name="list.Append"/><require name="list.Reverse"/></realized><function><eqn altname="num_occ" path="list.NumOcc"><app><const name="HOL.eq"/><app><var name="num_occ"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></var><var name="x"><tvar name="a"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><case><var name="l"><type name="List.list"><tvar name="a"/></type></var><pat><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const><num val="0"><type name="Int.int"/></num></pat><pat><app><const name="List.list.Cons"/><var name="y"><tvar name="a"/></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="Groups.plus_class.plus"/><app><const name="HOL.If"/><app><const name="HOL.eq"/><var name="x"><tvar name="a"/></var><var name="y"><tvar name="a"/></var></app><num val="1"><type name="Int.int"/></num><num val="0"><type name="Int.int"/></num></app><app><var name="num_occ"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></var><var name="x"><tvar name="a"/></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app></app></pat></case></app></eqn></function><lemma name="Num_Occ_NonNeg" altname="Num_Occ_NonNeg" path="list.NumOcc"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><app><const name="num_occ" local="true"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></const><var name="x"><tvar name="a"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma><lemma name="Mem_Num_Occ" altname="Mem_Num_Occ" path="list.NumOcc"><prems/><concls><app><const name="HOL.eq"/><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Int.int"/></num><app><const name="num_occ" local="true"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></const><var name="x"><tvar name="a"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma><lemma name="Append_Num_Occ" altname="Append_Num_Occ" path="list.NumOcc"><prems/><concls><app><const name="HOL.eq"/><app><const name="num_occ" local="true"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></const><var name="x"><tvar name="a"/></var><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="Groups.plus_class.plus"/><app><const name="num_occ" local="true"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></const><var name="x"><tvar name="a"/></var><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="num_occ" local="true"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></const><var name="x"><tvar name="a"/></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma><lemma name="reverse_num_occ" altname="reverse_num_occ" path="list.NumOcc"><prems/><concls><app><const name="HOL.eq"/><app><const name="num_occ" local="true"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></const><var name="x"><tvar name="a"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="num_occ" local="true"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></const><var name="x"><tvar name="a"/></var><app><const name="List.rev"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.Permut" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/><require name="list.Length"/><require name="list.Mem"/><require name="list.Append"/><require name="list.Reverse"/><require name="list.NumOcc"/></realized><definition altname="permut" path="list.Permut"><app><const name="HOL.eq"/><app><var name="permut"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></var><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="HOL.All"/><abs name="x"><tvar name="a"/><app><const name="HOL.eq"/><app><const name="num_occ" path="list.NumOcc"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></const><var name="x"><tvar name="a"/></var><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="num_occ" path="list.NumOcc"><fun><tvar name="a"/><type name="List.list"><tvar name="a"/></type><type name="Int.int"/></fun></const><var name="x"><tvar name="a"/></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></abs></app></app></definition><lemma name="Permut_refl" altname="Permut_refl" path="list.Permut"><prems/><concls><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l"><type name="List.list"><tvar name="a"/></type></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></concls></lemma><lemma name="Permut_sym" altname="Permut_sym" path="list.Permut"><prems><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></prems><concls><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l2"><type name="List.list"><tvar name="a"/></type></var><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></concls></lemma><lemma name="Permut_trans" altname="Permut_trans" path="list.Permut"><prems><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l2"><type name="List.list"><tvar name="a"/></type></var><var name="l3"><type name="List.list"><tvar name="a"/></type></var></app></prems><concls><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l3"><type name="List.list"><tvar name="a"/></type></var></app></concls></lemma><lemma name="Permut_cons" altname="Permut_cons" path="list.Permut"><prems><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></prems><concls><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma><lemma name="Permut_swap" altname="Permut_swap" path="list.Permut"><prems/><concls><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><app><const name="List.list.Cons"/><var name="y"><tvar name="a"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="List.list.Cons"/><var name="y"><tvar name="a"/></var><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma><lemma name="Permut_cons_append" altname="Permut_cons_append" path="list.Permut"><prems/><concls><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><app><const name="List.append"/><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma><lemma name="Permut_assoc" altname="Permut_assoc" path="list.Permut"><prems/><concls><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><app><const name="List.append"/><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><var name="l3"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><app><const name="List.append"/><var name="l2"><type name="List.list"><tvar name="a"/></type></var><var name="l3"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma><lemma name="Permut_append" altname="Permut_append" path="list.Permut"><prems><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="k1"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l2"><type name="List.list"><tvar name="a"/></type></var><var name="k2"><type name="List.list"><tvar name="a"/></type></var></app></prems><concls><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.append"/><var name="k1"><type name="List.list"><tvar name="a"/></type></var><var name="k2"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma><lemma name="Permut_append_swap" altname="Permut_append_swap" path="list.Permut"><prems/><concls><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><app><const name="List.append"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.append"/><var name="l2"><type name="List.list"><tvar name="a"/></type></var><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma><lemma name="Permut_mem" altname="Permut_mem" path="list.Permut"><prems><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app></prems><concls><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma><lemma name="Permut_length" altname="Permut_length" path="list.Permut"><prems><app><const name="permut" local="true"><pred><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></pred></const><var name="l1"><type name="List.list"><tvar name="a"/></type></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.RevAppend" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/><require name="list.Length"/><require name="list.Mem"/><require name="list.Append"/><require name="list.Reverse"/></realized><function><eqn altname="rev_append" path="list.RevAppend"><app><const name="HOL.eq"/><app><var name="rev_append"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></fun></var><var name="s"><type name="List.list"><tvar name="a"/></type></var><var name="t"><type name="List.list"><tvar name="a"/></type></var></app><case><var name="s"><type name="List.list"><tvar name="a"/></type></var><pat><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><app><var name="rev_append"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></fun></var><var name="r"><type name="List.list"><tvar name="a"/></type></var><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="t"><type name="List.list"><tvar name="a"/></type></var></app></app></pat><pat><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const><var name="t"><type name="List.list"><tvar name="a"/></type></var></pat></case></app></eqn></function><lemma name="rev_append_append_l" altname="rev_append_append_l" path="list.RevAppend"><prems/><concls><app><const name="HOL.eq"/><app><const name="rev_append" local="true"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></fun></const><app><const name="List.append"/><var name="r"><type name="List.list"><tvar name="a"/></type></var><var name="s"><type name="List.list"><tvar name="a"/></type></var></app><var name="t"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="rev_append" local="true"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></fun></const><var name="s"><type name="List.list"><tvar name="a"/></type></var><app><const name="rev_append" local="true"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></fun></const><var name="r"><type name="List.list"><tvar name="a"/></type></var><var name="t"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma><lemma name="rev_append_length" altname="rev_append_length" path="list.RevAppend"><prems/><concls><app><const name="HOL.eq"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><app><const name="rev_append" local="true"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></fun></const><var name="s"><type name="List.list"><tvar name="a"/></type></var><var name="t"><type name="List.list"><tvar name="a"/></type></var></app></app></app><app><const name="Groups.plus_class.plus"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="s"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="t"><type name="List.list"><tvar name="a"/></type></var></app></app></app></app></concls></lemma><lemma name="rev_append_def" altname="rev_append_def" path="list.RevAppend"><prems/><concls><app><const name="HOL.eq"/><app><const name="rev_append" local="true"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></fun></const><var name="r"><type name="List.list"><tvar name="a"/></type></var><var name="s"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.append"/><app><const name="List.rev"/><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><var name="s"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma><lemma name="rev_append_append_r" altname="rev_append_append_r" path="list.RevAppend"><prems/><concls><app><const name="HOL.eq"/><app><const name="rev_append" local="true"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></fun></const><var name="r"><type name="List.list"><tvar name="a"/></type></var><app><const name="List.append"/><var name="s"><type name="List.list"><tvar name="a"/></type></var><var name="t"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="rev_append" local="true"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></fun></const><app><const name="rev_append" local="true"><fun><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type><type name="List.list"><tvar name="a"/></type></fun></const><var name="s"><type name="List.list"><tvar name="a"/></type></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><var name="t"><type name="List.list"><tvar name="a"/></type></var></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="list.Reverse" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="list.List"/><require name="list.Length"/><require name="list.Mem"/><require name="list.Append"/></realized><lemma name="reverse_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.rev"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><case><var name="l"><type name="List.list"><tvar name="a"/></type></var><pat><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const></pat><pat><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.append"/><app><const name="List.rev"/><var name="r"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const></app></app></pat></case></app></concls></lemma><lemma name="reverse_append" altname="reverse_append" path="list.Reverse"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.append"/><app><const name="List.rev"/><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app></app><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.append"/><app><const name="List.rev"/><var name="l1"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="l2"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma><lemma name="reverse_cons" altname="reverse_cons" path="list.Reverse"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.rev"/><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="List.append"/><app><const name="List.rev"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const></app></app></app></concls></lemma><lemma name="cons_reverse" altname="cons_reverse" path="list.Reverse"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><app><const name="List.rev"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="List.rev"/><app><const name="List.append"/><var name="l"><type name="List.list"><tvar name="a"/></type></var><app><const name="List.list.Cons"/><var name="x"><tvar name="a"/></var><const name="List.list.Nil"><type name="List.list"><tvar name="a"/></type></const></app></app></app></app></concls></lemma><lemma name="reverse_reverse" altname="reverse_reverse" path="list.Reverse"><prems/><concls><app><const name="HOL.eq"/><app><const name="List.rev"/><app><const name="List.rev"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></concls></lemma><lemma name="reverse_mem" altname="reverse_mem" path="list.Reverse"><prems/><concls><app><const name="HOL.eq"/><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app><app><const name="Set.member"/><var name="x"><tvar name="a"/></var><app><const name="List.list.set"/><app><const name="List.rev"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></app></app></concls></lemma><lemma name="Reverse_length" altname="Reverse_length" path="list.Reverse"><prems/><concls><app><const name="HOL.eq"/><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><app><const name="List.rev"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></app><app><const name="Nat.semiring_1_class.of_nat"><fun><type name="Nat.nat"/><type name="Int.int"/></fun></const><app><const name="List.length"/><var name="l"><type name="List.list"><tvar name="a"/></type></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="map.Const" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="map.Map"/></realized><lemma name="Const" altname="Const" path="map.Const"><prems/><concls><app><const name="HOL.eq"/><app><app><const name="_type_constraint_"><fun><fun><tvar name="a"/><tvar name="b"/></fun><fun><tvar name="a"/><tvar name="b"/></fun></fun></const><abs name=""><type name="dummy"/><var name="b"><tvar name="b"/></var></abs></app><var name="a"><tvar name="a"/></var></app><var name="b"><tvar name="b"/></var></app></concls></lemma></theory>
\ No newline at end of file
<theory name="map.Map" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/></realized><lemma name="Select_eq" altname="Select_eq" path="map.Map"><prems><app><const name="HOL.eq"/><var name="a1"><tvar name="a"/></var><var name="a2"><tvar name="a"/></var></app></prems><concls><app><const name="HOL.eq"/><app><app><const name="Fun.fun_upd"/><var name="m"><fun><tvar name="a"/><tvar name="b"/></fun></var><var name="a1"><tvar name="a"/></var><var name="b"><tvar name="b"/></var></app><var name="a2"><tvar name="a"/></var></app><var name="b"><tvar name="b"/></var></app></concls></lemma><lemma name="Select_neq" altname="Select_neq" path="map.Map"><prems><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="a1"><tvar name="a"/></var><var name="a2"><tvar name="a"/></var></app></app></prems><concls><app><const name="HOL.eq"/><app><app><const name="Fun.fun_upd"/><var name="m"><fun><tvar name="a"/><tvar name="b"/></fun></var><var name="a1"><tvar name="a"/></var><var name="b"><tvar name="b"/></var></app><var name="a2"><tvar name="a"/></var></app><app><var name="m"><fun><tvar name="a"/><tvar name="b"/></fun></var><var name="a2"><tvar name="a"/></var></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="map.MapInjection" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="map.Map"/><require name="map.Occ"/></realized><definition altname="injective" path="map.MapInjection"><app><const name="HOL.eq"/><app><var name="injective"><pred><fun><type name="Int.int"/><type name="Int.int"/></fun><type name="Int.int"/></pred></var><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="n"><type name="Int.int"/></var></app><app><const name="HOL.All"/><abs name="i"><type name="Int.int"/><app><const name="HOL.All"/><abs name="j"><type name="Int.int"/><app><const name="HOL.implies"/><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="i"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><var name="i"><type name="Int.int"/></var><var name="n"><type name="Int.int"/></var></app></app><app><const name="HOL.implies"/><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="j"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><var name="j"><type name="Int.int"/></var><var name="n"><type name="Int.int"/></var></app></app><app><const name="HOL.implies"/><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="i"><type name="Int.int"/></var><var name="j"><type name="Int.int"/></var></app></app><app><const name="HOL.Not"/><app><const name="HOL.eq"/><app><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="i"><type name="Int.int"/></var></app><app><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="j"><type name="Int.int"/></var></app></app></app></app></app></app></abs></app></abs></app></app></definition><definition altname="surjective" path="map.MapInjection"><app><const name="HOL.eq"/><app><var name="surjective"><pred><fun><type name="Int.int"/><type name="Int.int"/></fun><type name="Int.int"/></pred></var><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="n"><type name="Int.int"/></var></app><app><const name="HOL.All"/><abs name="i"><type name="Int.int"/><app><const name="HOL.implies"/><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="i"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><var name="i"><type name="Int.int"/></var><var name="n"><type name="Int.int"/></var></app></app><app><const name="HOL.Ex"/><abs name="j"><type name="Int.int"/><app><const name="HOL.conj"/><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="j"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><var name="j"><type name="Int.int"/></var><var name="n"><type name="Int.int"/></var></app></app><app><const name="HOL.eq"/><app><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="j"><type name="Int.int"/></var></app><var name="i"><type name="Int.int"/></var></app></app></abs></app></app></abs></app></app></definition><definition altname="range" path="map.MapInjection"><app><const name="HOL.eq"/><app><var name="range"><pred><fun><type name="Int.int"/><type name="Int.int"/></fun><type name="Int.int"/></pred></var><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="n"><type name="Int.int"/></var></app><app><const name="HOL.All"/><abs name="i"><type name="Int.int"/><app><const name="HOL.implies"/><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="i"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><var name="i"><type name="Int.int"/></var><var name="n"><type name="Int.int"/></var></app></app><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><app><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="i"><type name="Int.int"/></var></app></app><app><const name="Orderings.ord_class.less"/><app><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="i"><type name="Int.int"/></var></app><var name="n"><type name="Int.int"/></var></app></app></app></abs></app></app></definition><lemma name="injective_surjective" altname="injective_surjective" path="map.MapInjection"><prems><app><const name="injective" local="true"><pred><fun><type name="Int.int"/><type name="Int.int"/></fun><type name="Int.int"/></pred></const><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="n"><type name="Int.int"/></var></app><app><const name="range" local="true"><pred><fun><type name="Int.int"/><type name="Int.int"/></fun><type name="Int.int"/></pred></const><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="surjective" local="true"><pred><fun><type name="Int.int"/><type name="Int.int"/></fun><type name="Int.int"/></pred></const><var name="a"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="n"><type name="Int.int"/></var></app></concls></lemma><lemma name="injection_occ" altname="injection_occ" path="map.MapInjection"><prems/><concls><app><const name="HOL.eq"/><app><const name="injective" local="true"><pred><fun><type name="Int.int"/><type name="Int.int"/></fun><type name="Int.int"/></pred></const><var name="m"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><var name="n"><type name="Int.int"/></var></app><app><const name="HOL.All"/><abs name="v"><type name="Int.int"/><app><const name="Orderings.ord_class.less_eq"/><app><const name="occ" path="map.Occ"><fun><type name="Int.int"/><fun><type name="Int.int"/><type name="Int.int"/></fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="v"><type name="Int.int"/></var><var name="m"><fun><type name="Int.int"/><type name="Int.int"/></fun></var><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app><num val="1"><type name="Int.int"/></num></app></abs></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="map.MapPermut" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="map.Map"/><require name="map.Occ"/></realized><definition altname="permut" path="map.MapPermut"><app><const name="HOL.eq"/><app><var name="permut"><pred><fun><type name="Int.int"/><tvar name="a"/></fun><fun><type name="Int.int"/><tvar name="a"/></fun><type name="Int.int"/><type name="Int.int"/></pred></var><var name="m1"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="m2"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="l"><type name="Int.int"/></var><var name="u"><type name="Int.int"/></var></app><app><const name="HOL.All"/><abs name="v"><tvar name="a"/><app><const name="HOL.eq"/><app><const name="occ" path="map.Occ"><fun><tvar name="a"/><fun><type name="Int.int"/><tvar name="a"/></fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="v"><tvar name="a"/></var><var name="m1"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="l"><type name="Int.int"/></var><var name="u"><type name="Int.int"/></var></app><app><const name="occ" path="map.Occ"><fun><tvar name="a"/><fun><type name="Int.int"/><tvar name="a"/></fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="v"><tvar name="a"/></var><var name="m2"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="l"><type name="Int.int"/></var><var name="u"><type name="Int.int"/></var></app></app></abs></app></app></definition><lemma name="permut_trans" altname="permut_trans" path="map.MapPermut"><prems><app><const name="permut" local="true"><pred><fun><type name="Int.int"/><tvar name="a"/></fun><fun><type name="Int.int"/><tvar name="a"/></fun><type name="Int.int"/><type name="Int.int"/></pred></const><var name="a1"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="a2"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="l"><type name="Int.int"/></var><var name="u"><type name="Int.int"/></var></app><app><const name="permut" local="true"><pred><fun><type name="Int.int"/><tvar name="a"/></fun><fun><type name="Int.int"/><tvar name="a"/></fun><type name="Int.int"/><type name="Int.int"/></pred></const><var name="a2"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="a3"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="l"><type name="Int.int"/></var><var name="u"><type name="Int.int"/></var></app></prems><concls><app><const name="permut" local="true"><pred><fun><type name="Int.int"/><tvar name="a"/></fun><fun><type name="Int.int"/><tvar name="a"/></fun><type name="Int.int"/><type name="Int.int"/></pred></const><var name="a1"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="a3"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="l"><type name="Int.int"/></var><var name="u"><type name="Int.int"/></var></app></concls></lemma><lemma name="permut_exists" altname="permut_exists" path="map.MapPermut"><prems><app><const name="permut" local="true"><pred><fun><type name="Int.int"/><tvar name="a"/></fun><fun><type name="Int.int"/><tvar name="a"/></fun><type name="Int.int"/><type name="Int.int"/></pred></const><var name="a1"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="a2"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="l"><type name="Int.int"/></var><var name="u"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><var name="l"><type name="Int.int"/></var><var name="i"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><var name="i"><type name="Int.int"/></var><var name="u"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.Ex"/><abs name="j"><type name="Int.int"/><app><const name="HOL.conj"/><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><var name="l"><type name="Int.int"/></var><var name="j"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><var name="j"><type name="Int.int"/></var><var name="u"><type name="Int.int"/></var></app></app><app><const name="HOL.eq"/><app><var name="a1"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="j"><type name="Int.int"/></var></app><app><var name="a2"><fun><type name="Int.int"/><tvar name="a"/></fun></var><var name="i"><type name="Int.int"/></var></app></app></app></abs></app></concls></lemma></theory>
\ No newline at end of file
This diff is collapsed.
<theory name="number.Coprime" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="int.ComputerDivision"/><require name="number.Parity"/><require name="number.Divisibility"/><require name="number.Gcd"/><require name="number.Prime"/></realized><lemma name="coprime_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.coprime"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app><num val="1"><type name="Int.int"/></num></app></app></concls></lemma><lemma name="prime_coprime" altname="prime_coprime" path="number.Coprime"><prems/><concls><app><const name="HOL.eq"/><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><var name="p"><type name="Int.int"/></var></app><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><num val="2"><type name="Int.int"/></num><var name="p"><type name="Int.int"/></var></app><app><const name="HOL.All"/><abs name="n"><type name="Int.int"/><app><const name="HOL.implies"/><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><num val="1"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><var name="n"><type name="Int.int"/></var><var name="p"><type name="Int.int"/></var></app></app><app><const name="GCD.gcd_class.coprime"/><var name="n"><type name="Int.int"/></var><var name="p"><type name="Int.int"/></var></app></app></abs></app></app></app></concls></lemma><lemma name="Gauss" altname="Gauss" path="number.Coprime"><prems><app><const name="Rings.dvd_class.dvd"/><var name="a"><type name="Int.int"/></var><app><const name="Groups.times_class.times"/><var name="b"><type name="Int.int"/></var><var name="c"><type name="Int.int"/></var></app></app><app><const name="GCD.gcd_class.coprime"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></prems><concls><app><const name="Rings.dvd_class.dvd"/><var name="a"><type name="Int.int"/></var><var name="c"><type name="Int.int"/></var></app></concls></lemma><lemma name="Euclid" altname="Euclid" path="number.Coprime"><prems><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><var name="p"><type name="Int.int"/></var></app><app><const name="Rings.dvd_class.dvd"/><var name="p"><type name="Int.int"/></var><app><const name="Groups.times_class.times"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app></prems><concls><app><const name="HOL.disj"/><app><const name="Rings.dvd_class.dvd"/><var name="p"><type name="Int.int"/></var><var name="a"><type name="Int.int"/></var></app><app><const name="Rings.dvd_class.dvd"/><var name="p"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="gcd_coprime" altname="gcd_coprime" path="number.Coprime"><prems><app><const name="GCD.gcd_class.coprime"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><app><const name="Groups.times_class.times"/><var name="b"><type name="Int.int"/></var><var name="c"><type name="Int.int"/></var></app></app><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="c"><type name="Int.int"/></var></app></app></concls></lemma></theory>
\ No newline at end of file
This diff is collapsed.
<theory name="number.Gcd" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="int.ComputerDivision"/><require name="number.Parity"/><require name="number.Divisibility"/></realized><lemma name="gcd_nonneg" altname="gcd_nonneg" path="number.Gcd"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="gcd_def1" altname="gcd_def1" path="number.Gcd"><prems/><concls><app><const name="Rings.dvd_class.dvd"/><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app><var name="a"><type name="Int.int"/></var></app></concls></lemma><lemma name="gcd_def2" altname="gcd_def2" path="number.Gcd"><prems/><concls><app><const name="Rings.dvd_class.dvd"/><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app><var name="b"><type name="Int.int"/></var></app></concls></lemma><lemma name="gcd_def3" altname="gcd_def3" path="number.Gcd"><prems><app><const name="Rings.dvd_class.dvd"/><var name="x"><type name="Int.int"/></var><var name="a"><type name="Int.int"/></var></app><app><const name="Rings.dvd_class.dvd"/><var name="x"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></prems><concls><app><const name="Rings.dvd_class.dvd"/><var name="x"><type name="Int.int"/></var><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="gcd_unique" altname="gcd_unique" path="number.Gcd"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="d"><type name="Int.int"/></var></app><app><const name="Rings.dvd_class.dvd"/><var name="d"><type name="Int.int"/></var><var name="a"><type name="Int.int"/></var></app><app><const name="Rings.dvd_class.dvd"/><var name="d"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app><app><const name="HOL.All"/><abs name="x"><type name="Int.int"/><app><const name="HOL.implies"/><app><const name="Rings.dvd_class.dvd"/><var name="x"><type name="Int.int"/></var><var name="a"><type name="Int.int"/></var></app><app><const name="HOL.implies"/><app><const name="Rings.dvd_class.dvd"/><var name="x"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app><app><const name="Rings.dvd_class.dvd"/><var name="x"><type name="Int.int"/></var><var name="d"><type name="Int.int"/></var></app></app></app></abs></app></prems><concls><app><const name="HOL.eq"/><var name="d"><type name="Int.int"/></var><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="Assoc" altname="Assoc" path="number.Gcd"><prems/><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><app><const name="GCD.gcd_class.gcd"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><var name="z"><type name="Int.int"/></var></app><app><const name="GCD.gcd_class.gcd"/><var name="x"><type name="Int.int"/></var><app><const name="GCD.gcd_class.gcd"/><var name="y"><type name="Int.int"/></var><var name="z"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Comm" altname="Comm" path="number.Gcd"><prems/><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="GCD.gcd_class.gcd"/><var name="y"><type name="Int.int"/></var><var name="x"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="gcd_0_pos" altname="gcd_0_pos" path="number.Gcd"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="a"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app><var name="a"><type name="Int.int"/></var></app></concls></lemma><lemma name="gcd_0_neg" altname="gcd_0_neg" path="number.Gcd"><prems><app><const name="Orderings.ord_class.less"/><var name="a"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app><app><const name="Groups.uminus_class.uminus"/><var name="a"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="gcd_opp" altname="gcd_opp" path="number.Gcd"><prems/><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app><app><const name="GCD.gcd_class.gcd"/><app><const name="Groups.uminus_class.uminus"/><var name="a"><type name="Int.int"/></var></app><var name="b"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="gcd_euclid" altname="gcd_euclid" path="number.Gcd"><prems/><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><app><const name="Groups.minus_class.minus"/><var name="b"><type name="Int.int"/></var><app><const name="Groups.times_class.times"/><var name="q"><type name="Int.int"/></var><var name="a"><type name="Int.int"/></var></app></app></app></app></concls></lemma><lemma name="Gcd_computer_mod" altname="Gcd_computer_mod" path="number.Gcd"><prems><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="b"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app></app></prems><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><var name="b"><type name="Int.int"/></var><app><const name="mod" path="int.ComputerDivision"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="Gcd_euclidean_mod" altname="Gcd_euclidean_mod" path="number.Gcd"><prems><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="b"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app></app></prems><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><var name="b"><type name="Int.int"/></var><app><const name="mod" path="int.EuclideanDivision"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="gcd_mult" altname="gcd_mult" path="number.Gcd"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="c"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="GCD.gcd_class.gcd"/><app><const name="Groups.times_class.times"/><var name="c"><type name="Int.int"/></var><var name="a"><type name="Int.int"/></var></app><app><const name="Groups.times_class.times"/><var name="c"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app><app><const name="Groups.times_class.times"/><var name="c"><type name="Int.int"/></var><app><const name="GCD.gcd_class.gcd"/><var name="a"><type name="Int.int"/></var><var name="b"><type name="Int.int"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="number.Parity" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/></realized><lemma name="even_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Parity.semiring_parity_class.even"/><var name="n"><type name="Int.int"/></var></app><app><const name="HOL.Ex"/><abs name="k"><type name="Int.int"/><app><const name="HOL.eq"/><var name="n"><type name="Int.int"/></var><app><const name="Groups.times_class.times"/><num val="2"><type name="Int.int"/></num><var name="k"><type name="Int.int"/></var></app></app></abs></app></app></concls></lemma><lemma name="odd_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Parity.semiring_parity_class.odd"/><var name="n"><type name="Int.int"/></var></app><app><const name="HOL.Ex"/><abs name="k"><type name="Int.int"/><app><const name="HOL.eq"/><var name="n"><type name="Int.int"/></var><app><const name="Groups.plus_class.plus"/><app><const name="Groups.times_class.times"/><num val="2"><type name="Int.int"/></num><var name="k"><type name="Int.int"/></var></app><num val="1"><type name="Int.int"/></num></app></app></abs></app></app></concls></lemma><lemma name="even_or_odd" altname="even_or_odd" path="number.Parity"><prems/><concls><app><const name="HOL.disj"/><app><const name="Parity.semiring_parity_class.even"/><var name="n"><type name="Int.int"/></var></app><app><const name="Parity.semiring_parity_class.odd"/><var name="n"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="even_not_odd" altname="even_not_odd" path="number.Parity"><prems><app><const name="Parity.semiring_parity_class.even"/><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.Not"/><app><const name="Parity.semiring_parity_class.odd"/><var name="n"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="odd_not_even" altname="odd_not_even" path="number.Parity"><prems><app><const name="Parity.semiring_parity_class.odd"/><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.Not"/><app><const name="Parity.semiring_parity_class.even"/><var name="n"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="even_odd" altname="even_odd" path="number.Parity"><prems><app><const name="Parity.semiring_parity_class.even"/><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="Parity.semiring_parity_class.odd"/><app><const name="Groups.plus_class.plus"/><var name="n"><type name="Int.int"/></var><num val="1"><type name="Int.int"/></num></app></app></concls></lemma><lemma name="odd_even" altname="odd_even" path="number.Parity"><prems><app><const name="Parity.semiring_parity_class.odd"/><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="Parity.semiring_parity_class.even"/><app><const name="Groups.plus_class.plus"/><var name="n"><type name="Int.int"/></var><num val="1"><type name="Int.int"/></num></app></app></concls></lemma><lemma name="even_even" altname="even_even" path="number.Parity"><prems><app><const name="Parity.semiring_parity_class.even"/><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="Parity.semiring_parity_class.even"/><app><const name="Groups.plus_class.plus"/><var name="n"><type name="Int.int"/></var><num val="2"><type name="Int.int"/></num></app></app></concls></lemma><lemma name="odd_odd" altname="odd_odd" path="number.Parity"><prems><app><const name="Parity.semiring_parity_class.odd"/><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="Parity.semiring_parity_class.odd"/><app><const name="Groups.plus_class.plus"/><var name="n"><type name="Int.int"/></var><num val="2"><type name="Int.int"/></num></app></app></concls></lemma><lemma name="even_2k" altname="even_2k" path="number.Parity"><prems/><concls><app><const name="Parity.semiring_parity_class.even"/><app><const name="Groups.times_class.times"/><num val="2"><type name="Int.int"/></num><var name="k"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="odd_2k1" altname="odd_2k1" path="number.Parity"><prems/><concls><app><const name="Parity.semiring_parity_class.odd"/><app><const name="Groups.plus_class.plus"/><app><const name="Groups.times_class.times"/><num val="2"><type name="Int.int"/></num><var name="k"><type name="Int.int"/></var></app><num val="1"><type name="Int.int"/></num></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="number.Prime" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="int.ComputerDivision"/><require name="number.Parity"/><require name="number.Divisibility"/></realized><lemma name="prime_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><var name="p"><type name="Int.int"/></var></app><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><num val="2"><type name="Int.int"/></num><var name="p"><type name="Int.int"/></var></app><app><const name="HOL.All"/><abs name="n"><type name="Int.int"/><app><const name="HOL.implies"/><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less"/><num val="1"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><var name="n"><type name="Int.int"/></var><var name="p"><type name="Int.int"/></var></app></app><app><const name="HOL.Not"/><app><const name="Rings.dvd_class.dvd"/><var name="n"><type name="Int.int"/></var><var name="p"><type name="Int.int"/></var></app></app></app></abs></app></app></app></concls></lemma><lemma name="not_prime_1" altname="not_prime_1" path="number.Prime"><prems/><concls><app><const name="HOL.Not"/><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><num val="1"><type name="Int.int"/></num></app></app></concls></lemma><lemma name="prime_2" altname="prime_2" path="number.Prime"><prems/><concls><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><num val="2"><type name="Int.int"/></num></app></concls></lemma><lemma name="prime_3" altname="prime_3" path="number.Prime"><prems/><concls><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><num val="3"><type name="Int.int"/></num></app></concls></lemma><lemma name="prime_divisors" altname="prime_divisors" path="number.Prime"><prems><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><var name="p"><type name="Int.int"/></var></app><app><const name="Rings.dvd_class.dvd"/><var name="d"><type name="Int.int"/></var><var name="p"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="d"><type name="Int.int"/></var><num val="1"><type name="Int.int"/></num></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="d"><type name="Int.int"/></var><app><const name="Groups.uminus_class.uminus"/><num val="1"><type name="Int.int"/></num></app></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="d"><type name="Int.int"/></var><var name="p"><type name="Int.int"/></var></app><app><const name="HOL.eq"/><var name="d"><type name="Int.int"/></var><app><const name="Groups.uminus_class.uminus"/><var name="p"><type name="Int.int"/></var></app></app></app></app></app></concls></lemma><lemma name="small_divisors" altname="small_divisors" path="number.Prime"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="2"><type name="Int.int"/></num><var name="p"><type name="Int.int"/></var></app><app><const name="HOL.All"/><abs name="d"><type name="Int.int"/><app><const name="HOL.implies"/><app><const name="Orderings.ord_class.less_eq"/><num val="2"><type name="Int.int"/></num><var name="d"><type name="Int.int"/></var></app><app><const name="HOL.implies"/><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><var name="d"><type name="Int.int"/></var></app><app><const name="HOL.implies"/><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less"/><num val="1"><type name="Int.int"/></num><app><const name="Groups.times_class.times"/><var name="d"><type name="Int.int"/></var><var name="d"><type name="Int.int"/></var></app></app><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.times_class.times"/><var name="d"><type name="Int.int"/></var><var name="d"><type name="Int.int"/></var></app><var name="p"><type name="Int.int"/></var></app></app><app><const name="HOL.Not"/><app><const name="Rings.dvd_class.dvd"/><var name="d"><type name="Int.int"/></var><var name="p"><type name="Int.int"/></var></app></app></app></app></app></abs></app></prems><concls><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><var name="p"><type name="Int.int"/></var></app></concls></lemma><lemma name="even_prime" altname="even_prime" path="number.Prime"><prems><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><var name="p"><type name="Int.int"/></var></app><app><const name="Parity.semiring_parity_class.even"/><var name="p"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><var name="p"><type name="Int.int"/></var><num val="2"><type name="Int.int"/></num></app></concls></lemma><lemma name="odd_prime" altname="odd_prime" path="number.Prime"><prems><app><const name="Factorial_Ring.normalization_semidom_class.prime"/><var name="p"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><num val="3"><type name="Int.int"/></num><var name="p"><type name="Int.int"/></var></app></prems><concls><app><const name="Parity.semiring_parity_class.odd"/><var name="p"><type name="Int.int"/></var></app></concls></lemma></theory>
\ No newline at end of file
<theory name="real.Abs" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="real.Real"/></realized><lemma name="abs_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Real.real"/></var></app><app><const name="HOL.If"/><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Real.real"/></num><var name="x"><type name="Real.real"/></var></app><var name="x"><type name="Real.real"/></var><app><const name="Groups.uminus_class.uminus"/><var name="x"><type name="Real.real"/></var></app></app></app></concls></lemma><lemma name="Abs_le" altname="Abs_le" path="real.Abs"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Real.real"/></var></app><var name="y"><type name="Real.real"/></var></app><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.uminus_class.uminus"/><var name="y"><type name="Real.real"/></var></app><var name="x"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app></app></app></concls></lemma><lemma name="Abs_pos" altname="Abs_pos" path="real.Abs"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Real.real"/></num><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Real.real"/></var></app></app></concls></lemma><lemma name="Abs_sum" altname="Abs_sum" path="real.Abs"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.abs_class.abs"/><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app></app><app><const name="Groups.plus_class.plus"/><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Real.real"/></var></app><app><const name="Groups.abs_class.abs"/><var name="y"><type name="Real.real"/></var></app></app></app></concls></lemma><lemma name="Abs_prod" altname="Abs_prod" path="real.Abs"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.abs_class.abs"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app></app><app><const name="Groups.times_class.times"/><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Real.real"/></var></app><app><const name="Groups.abs_class.abs"/><var name="y"><type name="Real.real"/></var></app></app></app></concls></lemma><lemma name="triangular_inequality" altname="triangular_inequality" path="real.Abs"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.abs_class.abs"/><app><const name="Groups.minus_class.minus"/><var name="x"><type name="Real.real"/></var><var name="z"><type name="Real.real"/></var></app></app><app><const name="Groups.plus_class.plus"/><app><const name="Groups.abs_class.abs"/><app><const name="Groups.minus_class.minus"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app></app><app><const name="Groups.abs_class.abs"/><app><const name="Groups.minus_class.minus"/><var name="y"><type name="Real.real"/></var><var name="z"><type name="Real.real"/></var></app></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="real.ExpLog" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="real.Real"/></realized><param name="exp" altname="exp" path="real.ExpLog"><fun><type name="Real.real"/><type name="Real.real"/></fun></param><lemma name="Exp_zero" altname="Exp_zero" path="real.ExpLog"><prems/><concls><app><const name="HOL.eq"/><app><const name="exp" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><num val="0"><type name="Real.real"/></num></app><num val="1"><type name="Real.real"/></num></app></concls></lemma><lemma name="Exp_sum" altname="Exp_sum" path="real.ExpLog"><prems/><concls><app><const name="HOL.eq"/><app><const name="exp" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app></app><app><const name="Groups.times_class.times"/><app><const name="exp" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="x"><type name="Real.real"/></var></app><app><const name="exp" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="y"><type name="Real.real"/></var></app></app></app></concls></lemma><param name="log" altname="log" path="real.ExpLog"><fun><type name="Real.real"/><type name="Real.real"/></fun></param><lemma name="Log_one" altname="Log_one" path="real.ExpLog"><prems/><concls><app><const name="HOL.eq"/><app><const name="log" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><num val="1"><type name="Real.real"/></num></app><num val="0"><type name="Real.real"/></num></app></concls></lemma><lemma name="Log_mul" altname="Log_mul" path="real.ExpLog"><prems><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Real.real"/></num><var name="x"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Real.real"/></num><var name="y"><type name="Real.real"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="log" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><app><const name="Groups.times_class.times"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app></app><app><const name="Groups.plus_class.plus"/><app><const name="log" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="x"><type name="Real.real"/></var></app><app><const name="log" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="y"><type name="Real.real"/></var></app></app></app></concls></lemma><lemma name="Log_exp" altname="Log_exp" path="real.ExpLog"><prems/><concls><app><const name="HOL.eq"/><app><const name="log" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><app><const name="exp" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="x"><type name="Real.real"/></var></app></app><var name="x"><type name="Real.real"/></var></app></concls></lemma><lemma name="Exp_log" altname="Exp_log" path="real.ExpLog"><prems><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Real.real"/></num><var name="x"><type name="Real.real"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="exp" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><app><const name="log" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="x"><type name="Real.real"/></var></app></app><var name="x"><type name="Real.real"/></var></app></concls></lemma><definition altname="log2" path="real.ExpLog"><app><const name="HOL.eq"/><app><var name="log2"><fun><type name="Real.real"/><type name="Real.real"/></fun></var><var name="x"><type name="Real.real"/></var></app><app><const name="Rings.divide_class.divide"/><app><const name="log" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="x"><type name="Real.real"/></var></app><app><const name="log" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><num val="2"><type name="Real.real"/></num></app></app></app></definition><definition altname="log10" path="real.ExpLog"><app><const name="HOL.eq"/><app><var name="log10"><fun><type name="Real.real"/><type name="Real.real"/></fun></var><var name="x"><type name="Real.real"/></var></app><app><const name="Rings.divide_class.divide"/><app><const name="log" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="x"><type name="Real.real"/></var></app><app><const name="log" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><num val="10"><type name="Real.real"/></num></app></app></app></definition></theory>
\ No newline at end of file
<theory name="real.FromInt" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="real.Real"/></realized><param name="from_int" altname="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></param><lemma name="Zero" altname="Zero" path="real.FromInt"><prems/><concls><app><const name="HOL.eq"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><num val="0"><type name="Int.int"/></num></app><num val="0"><type name="Real.real"/></num></app></concls></lemma><lemma name="One" altname="One" path="real.FromInt"><prems/><concls><app><const name="HOL.eq"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><num val="1"><type name="Int.int"/></num></app><num val="1"><type name="Real.real"/></num></app></concls></lemma><lemma name="Add" altname="Add" path="real.FromInt"><prems/><concls><app><const name="HOL.eq"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app><app><const name="Groups.plus_class.plus"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="x"><type name="Int.int"/></var></app><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="y"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Sub" altname="Sub" path="real.FromInt"><prems/><concls><app><const name="HOL.eq"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="Groups.minus_class.minus"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app><app><const name="Groups.minus_class.minus"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="x"><type name="Int.int"/></var></app><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="y"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Mul" altname="Mul" path="real.FromInt"><prems/><concls><app><const name="HOL.eq"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="Groups.times_class.times"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app><app><const name="Groups.times_class.times"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="x"><type name="Int.int"/></var></app><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="y"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Neg" altname="Neg" path="real.FromInt"><prems/><concls><app><const name="HOL.eq"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="Groups.uminus_class.uminus"/><var name="x"><type name="Int.int"/></var></app></app><app><const name="Groups.uminus_class.uminus"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="x"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Monotonic" altname="Monotonic" path="real.FromInt"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="x"><type name="Int.int"/></var></app><app><const name="from_int" local="true"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="y"><type name="Int.int"/></var></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="real.MinMax" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="real.Real"/></realized><lemma name="min_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.min"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><app><const name="HOL.If"/><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app></app></concls></lemma><lemma name="max_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.max"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><app><const name="HOL.If"/><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><var name="y"><type name="Real.real"/></var><var name="x"><type name="Real.real"/></var></app></app></concls></lemma><lemma name="Min_r" altname="Min_r" path="real.MinMax"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="y"><type name="Real.real"/></var><var name="x"><type name="Real.real"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.min"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><var name="y"><type name="Real.real"/></var></app></concls></lemma><lemma name="Max_l" altname="Max_l" path="real.MinMax"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="y"><type name="Real.real"/></var><var name="x"><type name="Real.real"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.max"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><var name="x"><type name="Real.real"/></var></app></concls></lemma><lemma name="Min_comm" altname="Min_comm" path="real.MinMax"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.min"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.min"/><var name="y"><type name="Real.real"/></var><var name="x"><type name="Real.real"/></var></app></app></concls></lemma><lemma name="Max_comm" altname="Max_comm" path="real.MinMax"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.max"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.max"/><var name="y"><type name="Real.real"/></var><var name="x"><type name="Real.real"/></var></app></app></concls></lemma><lemma name="Min_assoc" altname="Min_assoc" path="real.MinMax"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.min"/><app><const name="Orderings.ord_class.min"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><var name="z"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.min"/><var name="x"><type name="Real.real"/></var><app><const name="Orderings.ord_class.min"/><var name="y"><type name="Real.real"/></var><var name="z"><type name="Real.real"/></var></app></app></app></concls></lemma><lemma name="Max_assoc" altname="Max_assoc" path="real.MinMax"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.max"/><app><const name="Orderings.ord_class.max"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><var name="z"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.max"/><var name="x"><type name="Real.real"/></var><app><const name="Orderings.ord_class.max"/><var name="y"><type name="Real.real"/></var><var name="z"><type name="Real.real"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="real.PowerInt" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="real.Real"/><require name="real.RealInfix"/></realized><lemma name="Power_0" altname="Power_0" path="real.PowerInt"><prems/><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><num val="0"><type name="Int.int"/></num></app></app><num val="1"><type name="Real.real"/></num></app></concls></lemma><lemma name="Power_s" altname="Power_s" path="real.PowerInt"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><app><const name="Groups.plus_class.plus"/><var name="n"><type name="Int.int"/></var><num val="1"><type name="Int.int"/></num></app></app></app><app><const name="Groups.times_class.times"/><var name="x"><type name="Real.real"/></var><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app></app></app></concls></lemma><lemma name="Power_s_alt" altname="Power_s_alt" path="real.PowerInt"><prems><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Groups.times_class.times"/><var name="x"><type name="Real.real"/></var><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><app><const name="Groups.minus_class.minus"/><var name="n"><type name="Int.int"/></var><num val="1"><type name="Int.int"/></num></app></app></app></app></app></concls></lemma><lemma name="Power_1" altname="Power_1" path="real.PowerInt"><prems/><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><num val="1"><type name="Int.int"/></num></app></app><var name="x"><type name="Real.real"/></var></app></concls></lemma><lemma name="Power_sum" altname="Power_sum" path="real.PowerInt"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="m"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><app><const name="Groups.plus_class.plus"/><var name="n"><type name="Int.int"/></var><var name="m"><type name="Int.int"/></var></app></app></app><app><const name="Groups.times_class.times"/><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><var name="m"><type name="Int.int"/></var></app></app></app></app></concls></lemma><lemma name="Power_mult" altname="Power_mult" path="real.PowerInt"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="m"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><app><const name="Groups.times_class.times"/><var name="n"><type name="Int.int"/></var><var name="m"><type name="Int.int"/></var></app></app></app><app><const name="Power.power_class.power"/><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Int.nat"/><var name="m"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Power_comm1" altname="Power_comm1" path="real.PowerInt"><prems><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><app><const name="Groups.times_class.times"/><var name="y"><type name="Real.real"/></var><var name="x"><type name="Real.real"/></var></app></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><var name="y"><type name="Real.real"/></var></app><app><const name="Groups.times_class.times"/><var name="y"><type name="Real.real"/></var><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app></app></app></concls></lemma><lemma name="Power_comm2" altname="Power_comm2" path="real.PowerInt"><prems><app><const name="HOL.eq"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><app><const name="Groups.times_class.times"/><var name="y"><type name="Real.real"/></var><var name="x"><type name="Real.real"/></var></app></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="Power.power_class.power"/><app><const name="Groups.times_class.times"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Groups.times_class.times"/><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app><app><const name="Power.power_class.power"/><var name="y"><type name="Real.real"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app></app></app></concls></lemma><lemma name="Pow_ge_one" altname="Pow_ge_one" path="real.PowerInt"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="n"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><num val="1"><type name="Real.real"/></num><var name="x"><type name="Real.real"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><num val="1"><type name="Real.real"/></num><app><const name="Power.power_class.power"/><var name="x"><type name="Real.real"/></var><app><const name="Int.nat"/><var name="n"><type name="Int.int"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
This diff is collapsed.
<theory name="real.RealInfix" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="real.Real"/></realized></theory>
\ No newline at end of file
<theory name="real.Square" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="real.Real"/></realized><definition altname="sqr" path="real.Square"><app><const name="HOL.eq"/><app><var name="sqr"><fun><type name="Real.real"/><type name="Real.real"/></fun></var><var name="x"><type name="Real.real"/></var></app><app><const name="Groups.times_class.times"/><var name="x"><type name="Real.real"/></var><var name="x"><type name="Real.real"/></var></app></app></definition><param name="sqrt" altname="sqrt" path="real.Square"><fun><type name="Real.real"/><type name="Real.real"/></fun></param><lemma name="Sqrt_positive" altname="Sqrt_positive" path="real.Square"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Real.real"/></num><var name="x"><type name="Real.real"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Real.real"/></num><app><const name="sqrt" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="x"><type name="Real.real"/></var></app></app></concls></lemma><lemma name="Sqrt_square" altname="Sqrt_square" path="real.Square"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Real.real"/></num><var name="x"><type name="Real.real"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="sqr" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><app><const name="sqrt" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="x"><type name="Real.real"/></var></app></app><var name="x"><type name="Real.real"/></var></app></concls></lemma><lemma name="Square_sqrt" altname="Square_sqrt" path="real.Square"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Real.real"/></num><var name="x"><type name="Real.real"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="sqrt" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><app><const name="Groups.times_class.times"/><var name="x"><type name="Real.real"/></var><var name="x"><type name="Real.real"/></var></app></app><var name="x"><type name="Real.real"/></var></app></concls></lemma><lemma name="Sqrt_mul" altname="Sqrt_mul" path="real.Square"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Real.real"/></num><var name="x"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Real.real"/></num><var name="y"><type name="Real.real"/></var></app></prems><concls><app><const name="HOL.eq"/><app><const name="sqrt" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><app><const name="Groups.times_class.times"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app></app><app><const name="Groups.times_class.times"/><app><const name="sqrt" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="x"><type name="Real.real"/></var></app><app><const name="sqrt" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="y"><type name="Real.real"/></var></app></app></app></concls></lemma><lemma name="Sqrt_le" altname="Sqrt_le" path="real.Square"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Real.real"/></num><var name="x"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="sqrt" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="x"><type name="Real.real"/></var></app><app><const name="sqrt" local="true"><fun><type name="Real.real"/><type name="Real.real"/></fun></const><var name="y"><type name="Real.real"/></var></app></app></concls></lemma></theory>
\ No newline at end of file
This diff is collapsed.
<theory name="real.Truncate" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="real.Real"/><require name="real.FromInt"/></realized><param name="truncate" altname="truncate" path="real.Truncate"><fun><type name="Real.real"/><type name="Int.int"/></fun></param><lemma name="Truncate_int" altname="Truncate_int" path="real.Truncate"><prems/><concls><app><const name="HOL.eq"/><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="i"><type name="Int.int"/></var></app></app><var name="i"><type name="Int.int"/></var></app></concls></lemma><lemma name="Truncate_down_pos" altname="Truncate_down_pos" path="real.Truncate"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Real.real"/></num><var name="x"><type name="Real.real"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app></app><var name="x"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.less"/><var name="x"><type name="Real.real"/></var><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="Groups.plus_class.plus"/><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app><num val="1"><type name="Int.int"/></num></app></app></app></concls></lemma><lemma name="Truncate_up_neg" altname="Truncate_up_neg" path="real.Truncate"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Real.real"/></var><num val="0"><type name="Real.real"/></num></app></prems><concls><app><const name="Orderings.ord_class.less"/><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="Groups.minus_class.minus"/><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app><num val="1"><type name="Int.int"/></num></app></app><var name="x"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Real.real"/></var><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app></app></app></concls></lemma><lemma name="Real_of_truncate" altname="Real_of_truncate" path="real.Truncate"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.minus_class.minus"/><var name="x"><type name="Real.real"/></var><num val="1"><type name="Real.real"/></num></app><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app></app></app><app><const name="Orderings.ord_class.less_eq"/><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app></app><app><const name="Groups.plus_class.plus"/><var name="x"><type name="Real.real"/></var><num val="1"><type name="Real.real"/></num></app></app></concls></lemma><lemma name="Truncate_monotonic" altname="Truncate_monotonic" path="real.Truncate"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Real.real"/></var><var name="y"><type name="Real.real"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="y"><type name="Real.real"/></var></app></app></concls></lemma><lemma name="Truncate_monotonic_int1" altname="Truncate_monotonic_int1" path="real.Truncate"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Real.real"/></var><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="i"><type name="Int.int"/></var></app></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app><var name="i"><type name="Int.int"/></var></app></concls></lemma><lemma name="Truncate_monotonic_int2" altname="Truncate_monotonic_int2" path="real.Truncate"><prems><app><const name="Orderings.ord_class.less_eq"/><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="i"><type name="Int.int"/></var></app><var name="x"><type name="Real.real"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><var name="i"><type name="Int.int"/></var><app><const name="truncate" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app></app></concls></lemma><param name="floor" altname="floor" path="real.Truncate"><fun><type name="Real.real"/><type name="Int.int"/></fun></param><param name="ceil" altname="ceil" path="real.Truncate"><fun><type name="Real.real"/><type name="Int.int"/></fun></param><lemma name="Floor_int" altname="Floor_int" path="real.Truncate"><prems/><concls><app><const name="HOL.eq"/><app><const name="floor" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="i"><type name="Int.int"/></var></app></app><var name="i"><type name="Int.int"/></var></app></concls></lemma><lemma name="Ceil_int" altname="Ceil_int" path="real.Truncate"><prems/><concls><app><const name="HOL.eq"/><app><const name="ceil" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><var name="i"><type name="Int.int"/></var></app></app><var name="i"><type name="Int.int"/></var></app></concls></lemma><lemma name="Floor_down" altname="Floor_down" path="real.Truncate"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="floor" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app></app><var name="x"><type name="Real.real"/></var></app><app><const name="Orderings.ord_class.less"/><var name="x"><type name="Real.real"/></var><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="Groups.plus_class.plus"/><app><const name="floor" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app><num val="1"><type name="Int.int"/></num></app></app></app></concls></lemma><lemma name="Ceil_up" altname="Ceil_up" path="real.Truncate"><prems/><concls><app><const name="Orderings.ord_class.less"/><app><const name="from_int" path="real.FromInt"><fun><type name="Int.int"/><type name="Real.real"/></fun></const><app><const name="Groups.minus_class.minus"/><app><const name="ceil" local="true"><fun><type name="Real.real"/><type name="Int.int"/></fun></const><var name="x"><type name="Real.real"/></var></app><num val="1">&l