Commit 5827c5ab authored by MARCHE Claude's avatar MARCHE Claude

example files for issues 15, 16 and 19

parent 1b4e7b10
module Issue15
use import list.List
goal g: forall l:list 'a. l = Nil
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../15_destruct_alg.mlw">
<theory name="Issue15" sum="e66dc991ed1c7476749af7ab45982f63">
<goal name="g">
<transf name="destruct_alg" arg1="l">
<goal name="g.0">
</goal>
<goal name="g.1">
</goal>
</transf>
<transf name="destruct_alg_subst" arg1="l">
<goal name="g.0">
</goal>
<goal name="g.1">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
module Issue16
predicate p int
predicate q int
function f int : int
goal g2: forall x. p x -> forall y:int. x = 42 -> q x
goal g1: forall x. p x -> forall y. x = f y -> q x
constant x : int
axiom h1 : p x
constant y:int
axiom h2: x = f y
goal g: q x
use import int.Int
goal g3: forall x:int.
forall z. z = x+1 ->
forall y. y = z ->
x = f y -> y = f y + 1
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../16_subst.mlw">
<theory name="Issue16" sum="98ec62c13c62b5a2b1ea28f0b4c80135">
<goal name="g2">
<transf name="simplify_trivial_quantification_in_goal" >
<goal name="g2.0">
</goal>
</transf>
<transf name="subst" arg1="x">
<goal name="g2.0">
</goal>
</transf>
</goal>
<goal name="g1">
</goal>
<goal name="g">
</goal>
<goal name="g3">
<transf name="remove" arg1="h1,h2">
<goal name="g3.0">
<transf name="case" arg1="x=0">
<goal name="g3.0.0">
</goal>
<goal name="g3.0.1">
</goal>
</transf>
<transf name="induction" arg1="x" arg2="from" arg3="42">
<goal name="g3.0.0">
</goal>
<goal name="g3.0.1">
</goal>
</transf>
</goal>
</transf>
<transf name="subst" arg1="x,y,z">
<goal name="g3.0">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../19_apply_with.mlw">
<theory name="I19_simplint" sum="7bce20e61a5551a6af73d2355b15c709">
<goal name="g">
<transf name="apply_with" arg1="H" arg2="1">
<goal name="g.0">
</goal>
<goal name="g.1">
</goal>
</transf>
</goal>
</theory>
<theory name="I19_simplpoly" sum="a0862dae57e5acda121e6fa4f7b5e82d">
<goal name="test">
<transf name="apply_with" arg1="trans" arg2="b">
<goal name="test.0">
</goal>
<goal name="test.1">
</goal>
</transf>
</goal>
</theory>
<theory name="I19_simplpoly2" sum="5f0342147f8467ab584bf33b21a6a483">
<goal name="test">
<transf name="apply_with" arg1="trans" arg2="42,b">
<goal name="test.0">
</goal>
<goal name="test.1">
</goal>
</transf>
</goal>
</theory>
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment