Global Index

Q

Y

_

(681 entries)

Projection Index

B

D

E

F

I

J

K

M

N

O

P

Q

S

U

W

X

Y

Z

_

other

(32 entries)

Record Index

B

D

E

F

I

J

K

L

M

N

O

P

Q

S

U

W

X

Y

Z

_

other

(12 entries)

Lemma Index

H

J

M

Q

X

Y

_

other

(198 entries)

Section Index

B

C

D

E

F

H

I

N

O

P

Q

S

T

V

W

X

Y

Z

_

other

(15 entries)

Constructor Index

F

H

Q

W

Y

Z

_

other

(63 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

N

O

P

Q

R

S

T

U

W

X

Y

Z

_

(28 entries)

Inductive Index

D

E

F

G

H

I

J

L

M

N

O

Q

R

U

W

X

Y

Z

_

other

(13 entries)

Definition Index

Q

X

Y

_

other

(166 entries)

Axiom Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

W

X

Y

Z

_

other

(19 entries)

Module Index

A

B

D

E

F

H

I

J

L

M

N

O

P

Q

R

S

T

U

W

X

Y

Z

_

other

(6 entries)

Variable Index

B

C

D

E

F

H

I

N

O

P

Q

S

T

V

W

X

Y

Z

_

other

(111 entries)

Library Index

D

F

H

I

J

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(18 entries)

Global Index

A

aadd [definition, in Scat.Assertions]
aadd_aebounds [lemma, in Scat.Assertions]
abound [definition, in Scat.Assertions]
abounds [definition, in Scat.Assertions]
abounds_Zle [lemma, in Scat.Assertions]
abound_abounds [lemma, in Scat.Assertions]
abound_monotonic [lemma, in Scat.Assertions]
abranch [projection, in Scat.Assertions]
abstract [projection, in Scat.Certificate]
AbstractionExample [section, in Scat.BasicExamples]
AbstractionExample.annotated [variable, in Scat.BasicExamples]
AbstractionExample.source [variable, in Scat.BasicExamples]
AbstractionExample.x [variable, in Scat.BasicExamples]
AbstractionExample.y [variable, in Scat.BasicExamples]
absurd [definition, in Scat.Conditions]
abs_rewrite [definition, in Scat.NaiveTermAbstractions]
abs_simplify_pre [definition, in Scat.NaiveTermAbstractions]
abs_rename [definition, in Scat.NaiveTermAbstractions]
abs_conj [definition, in Scat.NaiveTermAbstractions]
abs_coerce [definition, in Scat.NaiveTermAbstractions]
abs_assign [definition, in Scat.NaiveTermAbstractions]
abs_term [record, in Scat.NaiveTermAbstractions]
abs_not [definition, in Scat.NaiveGuardAbstractions]
abs_notx [definition, in Scat.NaiveGuardAbstractions]
abs_cut [definition, in Scat.NaiveGuardAbstractions]
abs_atom [definition, in Scat.NaiveGuardAbstractions]
abs_or [definition, in Scat.NaiveGuardAbstractions]
abs_and [definition, in Scat.NaiveGuardAbstractions]
abs_embed [definition, in Scat.NaiveGuardAbstractions]
abs_ensure [definition, in Scat.NaiveGuardAbstractions]
abs_guard [record, in Scat.NaiveGuardAbstractions]
acond [projection, in Scat.Assertions]
add [definition, in Scat.Conditions]
add_id [lemma, in Scat.Conditions]
add_out2 [lemma, in Scat.Conditions]
add_out [lemma, in Scat.Conditions]
add_in [lemma, in Scat.Conditions]
add_tech2 [lemma, in Scat.Guassign]
add_tech1 [lemma, in Scat.Guassign]
add_frameeq_out_2 [lemma, in Scat.Renaming]
add_frameeq_out_1 [lemma, in Scat.Renaming]
add_morphism [lemma, in Scat.Renaming]
adefault [definition, in Scat.Assertions]
aebounds [definition, in Scat.Assertions]
aebounds_Zle [lemma, in Scat.Assertions]
aempty [definition, in Scat.Assertions]
aempty_aebounds [lemma, in Scat.Assertions]
aentry [record, in Scat.Assertions]
aenvironment [definition, in Scat.Assertions]
aeval [definition, in Scat.Assertions]
aeval_bounds [lemma, in Scat.Assertions]
afind [definition, in Scat.Assertions]
alabel [record, in Scat.Assertions]
AND [constructor, in Scat.Conditions]
angel_awlp_duality [lemma, in Scat.Atoms]
angel_awlp_monotonic [lemma, in Scat.Atoms]
angel_awlp [definition, in Scat.Atoms]
annotated1_proof [lemma, in Scat.BasicExamples]
annotated2_proof [lemma, in Scat.BasicExamples]
asem [inductive, in Scat.Atoms]
asem_assign [constructor, in Scat.Atoms]
asem_ensure [constructor, in Scat.Atoms]
asem_req_ko [constructor, in Scat.Atoms]
asem_req_ok [constructor, in Scat.Atoms]
asem_skip [constructor, in Scat.Atoms]
asem_guassign [constructor, in Scat.Atoms]
assertion [inductive, in Scat.Assertions]
Assertions [library]
assign [constructor, in Scat.Atoms]
atbound [definition, in Scat.KernelVCG]
atbounds [definition, in Scat.KernelVCG]
atbounds_Zle [lemma, in Scat.KernelVCG]
atbound_atbounds [lemma, in Scat.KernelVCG]
atbound_monotonic [lemma, in Scat.KernelVCG]
atom [inductive, in Scat.Atoms]
atom [constructor, in Scat.Conditions]
Atoms [library]
atom_eq_awlp [lemma, in Scat.Atoms]
atom_eq [definition, in Scat.Atoms]
atpostfinder_awlp [lemma, in Scat.KernelProof]
atpostfinder_cbounds_post [lemma, in Scat.KernelProof]
atpostfinder_increases_bound [lemma, in Scat.KernelProof]
atpostfinder_renforce_vc [lemma, in Scat.KernelProof]
awlp [definition, in Scat.Atoms]
awlp_complete [lemma, in Scat.Atoms]
awlp_correctness [lemma, in Scat.Atoms]
awlp_monotonic [lemma, in Scat.Atoms]

B

basic [constructor, in Scat.Conditions]
BasicExamples [library]
bin [constructor, in Scat.Conditions]
bincmp [inductive, in Scat.Conditions]
bincmp_eq_refl [lemma, in Scat.Conditions]
bincmp_eq_eq [lemma, in Scat.Conditions]
bincmp_eq [definition, in Scat.Conditions]
binlog [inductive, in Scat.Conditions]
binlog_eq_refl [lemma, in Scat.Conditions]
binlog_eq_eq [lemma, in Scat.Conditions]
binlog_eq [definition, in Scat.Conditions]
binop [inductive, in Scat.Conditions]
binop_eq_refl [lemma, in Scat.Conditions]
binop_eq_eq [lemma, in Scat.Conditions]
binop_eq [definition, in Scat.Conditions]
biter [definition, in Scat.BoundedIteration]
biter_succ [lemma, in Scat.BoundedIteration]
biter_one [lemma, in Scat.BoundedIteration]
biter_zero [lemma, in Scat.BoundedIteration]
biter_spec [lemma, in Scat.BoundedIteration]
biter_nat_aux [lemma, in Scat.BoundedIteration]
biter_nat_spec_1 [lemma, in Scat.BoundedIteration]
biter_nat [definition, in Scat.BoundedIteration]
bound [definition, in Scat.KernelVCG]
BoundedIteration [library]
bounder_iter_nat_spec [lemma, in Scat.BoundedIteration]
bound_Kbounds [lemma, in Scat.KernelVCG]
branch [constructor, in Scat.Assertions]
branch2 [constructor, in Scat.Assertions]

C

casescmp [definition, in Scat.NaiveAbstractionLib]
cbound [definition, in Scat.Renaming]
cbounds [definition, in Scat.Renaming]
cbounds_orsubst [lemma, in Scat.Renaming]
cbounds_rsubst [lemma, in Scat.Renaming]
cbounds_rename [lemma, in Scat.Renaming]
cbounds_Zle [lemma, in Scat.Renaming]
cbound_cbounds [lemma, in Scat.Renaming]
cbound_monotonic [lemma, in Scat.Renaming]
cbranch [definition, in Scat.Certificate]
cbranch2 [definition, in Scat.Certificate]
ceq [definition, in Scat.Conditions]
certif [record, in Scat.Certificate]
Certificate [library]
certif_correctness [projection, in Scat.Certificate]
cjoin [definition, in Scat.Certificate]
concrete [projection, in Scat.Certificate]
Concrete [library]
ConcreteCondWrapper [module, in Scat.KernelVCG]
ConcreteCondWrapper.absurd [definition, in Scat.KernelVCG]
ConcreteCondWrapper.bind [definition, in Scat.KernelVCG]
ConcreteCondWrapper.ceq [definition, in Scat.KernelVCG]
ConcreteCondWrapper.check_entails [definition, in Scat.KernelVCG]
ConcreteCondWrapper.goal [projection, in Scat.KernelVCG]
ConcreteCondWrapper.hard_and [definition, in Scat.KernelVCG]
ConcreteCondWrapper.hyp [projection, in Scat.KernelVCG]
ConcreteCondWrapper.mesg [projection, in Scat.KernelVCG]
ConcreteCondWrapper.monad [definition, in Scat.KernelVCG]
ConcreteCondWrapper.rename [definition, in Scat.KernelVCG]
ConcreteCondWrapper.result [record, in Scat.KernelVCG]
ConcreteCondWrapper.ret [definition, in Scat.KernelVCG]
ConcreteCondWrapper.soft_or [definition, in Scat.KernelVCG]
ConcreteCondWrapper.tauto [definition, in Scat.KernelVCG]
ConcreteCondWrapper.tbnd [projection, in Scat.KernelVCG]
ConcreteCondWrapper.trename [definition, in Scat.KernelVCG]
ConcreteCondWrapper.value [projection, in Scat.KernelVCG]
ConcreteCondWrapper.VC [record, in Scat.KernelVCG]
ConcreteCondWrapper.vcl [projection, in Scat.KernelVCG]
cond [inductive, in Scat.Conditions]
Conditions [library]
cond_eq_oeval [lemma, in Scat.Conditions]
cond_eq_eval [lemma, in Scat.Conditions]
cond_eq [definition, in Scat.Conditions]
conj [constructor, in Scat.Assertions]
coq_abs_conj [definition, in Scat.NaiveTermAbstractions]
ctefun [axiom, in Scat.Conditions]
ctefun_Zof [lemma, in Scat.Conditions]

D

dbiter_nat_spec [lemma, in Scat.BoundedIteration]
dbiter_natx_spec [lemma, in Scat.BoundedIteration]
dbiter_nat [definition, in Scat.BoundedIteration]
dbiter_natx [definition, in Scat.BoundedIteration]
dead [definition, in Scat.Certificate]
DIV [constructor, in Scat.Conditions]

E

ensure [constructor, in Scat.Atoms]
EQ [constructor, in Scat.Conditions]
eval [definition, in Scat.Conditions]
evalcmp [definition, in Scat.Conditions]
evallog [definition, in Scat.Conditions]
evalop [definition, in Scat.Conditions]
eval_orsubst [lemma, in Scat.Guassign]
eval_orsubst_lfreshx [lemma, in Scat.Guassign]
eval_rsubst [lemma, in Scat.Guassign]
eval_rsubst_lfreshx [lemma, in Scat.Guassign]
Examples [library]
explore [definition, in Scat.NaiveAbstractionLib]
ext [definition, in Scat.Conditions]
extend [definition, in Scat.Renaming]
extract [definition, in Scat.Certificate]
ext_eval [lemma, in Scat.Conditions]
ext_teval [lemma, in Scat.Conditions]
ex_monotonic [lemma, in Scat.MiscUtils]

F

frameeq [definition, in Scat.Renaming]
frameeq_oeval [lemma, in Scat.Renaming]
frameeq_oteval [lemma, in Scat.Renaming]
frameeq_eval_imp_s [lemma, in Scat.Renaming]
frameeq_eval_imp [lemma, in Scat.Renaming]
frameeq_eval [lemma, in Scat.Renaming]
frameeq_teval [lemma, in Scat.Renaming]
frameeq_glue [lemma, in Scat.Renaming]
frameeq_trans [lemma, in Scat.Renaming]
frameeq_sym [lemma, in Scat.Renaming]
frameeq_Zle [lemma, in Scat.Renaming]
fresh [definition, in Scat.Renaming]
fresh_rbounds [lemma, in Scat.Renaming]

G

gabs [projection, in Scat.NaiveGuardAbstractions]
gconc [projection, in Scat.NaiveGuardAbstractions]
GenericVCG [module, in Scat.KernelVCG]
GenericVCG.atpostfinder [definition, in Scat.KernelVCG]
GenericVCG.internal_error [definition, in Scat.KernelVCG]
GenericVCG.Kvcgen [definition, in Scat.KernelVCG]
GenericVCG.pbnd [projection, in Scat.KernelVCG]
GenericVCG.post [projection, in Scat.KernelVCG]
GenericVCG.postfinder [definition, in Scat.KernelVCG]
GenericVCG.postfinder_le_iter [definition, in Scat.KernelVCG]
GenericVCG.postfinder_result [record, in Scat.KernelVCG]
GenericVCG.VCGCode [section, in Scat.KernelVCG]
GenericVCG.VCGCode.void [variable, in Scat.KernelVCG]
GenericVCG.VCGCode.xret [variable, in Scat.KernelVCG]
gproof [projection, in Scat.NaiveGuardAbstractions]
guassign [constructor, in Scat.Atoms]
Guassign [library]
GuassignExample [section, in Scat.BasicExamples]
GuassignExample.essai [variable, in Scat.BasicExamples]
GuassignExample.list [variable, in Scat.BasicExamples]
GuassignExample.t [variable, in Scat.BasicExamples]
GuassignExample.u [variable, in Scat.BasicExamples]
GuassignExample.v [variable, in Scat.BasicExamples]
GuassignExample.x [variable, in Scat.BasicExamples]
GuassignExample.y [variable, in Scat.BasicExamples]
GuassignExample.z [variable, in Scat.BasicExamples]
guassign_vc [lemma, in Scat.Guassign]

H

hname [projection, in Scat.NaiveTermAbstractions]
hoare_abs [definition, in Scat.NaiveTermAbstractions]
hoare_term [record, in Scat.NaiveTermAbstractions]
htb2 [definition, in Scat.NaiveTermAbstractions]
htpost [projection, in Scat.NaiveTermAbstractions]
htpre [projection, in Scat.NaiveTermAbstractions]
htproof [projection, in Scat.NaiveTermAbstractions]
ht_branch [definition, in Scat.NaiveTermAbstractions]
ht_branch2 [definition, in Scat.NaiveTermAbstractions]

I

iat [definition, in Scat.Certificate]
iat [constructor, in Scat.Concrete]
inv [constructor, in Scat.Assertions]
isok_wlp [lemma, in Scat.Concrete]
is_ok [definition, in Scat.Concrete]
iter [definition, in Scat.LoopsUnrolling]
iter_Kwlp [lemma, in Scat.LoopsUnrolling]

J

join [constructor, in Scat.Concrete]
joinchseq [definition, in Scat.Certificate]
joinseq [definition, in Scat.Certificate]
JoinseqUnrollInvariant [section, in Scat.Examples]
JoinseqUnrollInvariant.annotated [variable, in Scat.Examples]
JoinseqUnrollInvariant.approx_convexhull [variable, in Scat.Examples]
JoinseqUnrollInvariant.i [variable, in Scat.Examples]
JoinseqUnrollInvariant.label [variable, in Scat.Examples]
JoinseqUnrollInvariant.r [variable, in Scat.Examples]
JoinseqUnrollInvariant.source [variable, in Scat.Examples]
JoinseqUnrollInvariant.x [variable, in Scat.Examples]
JoinseqUnrollInvariant.y [variable, in Scat.Examples]

K

Kangel_wlp_correctness [lemma, in Scat.Kernel]
Kangel_wlp_duality [lemma, in Scat.Kernel]
Kangel_wlp_monotonic [lemma, in Scat.Kernel]
Kangel_wlp [definition, in Scat.Kernel]
Kbound [definition, in Scat.KernelVCG]
Kbounds [definition, in Scat.KernelVCG]
Kbounds_Zle [lemma, in Scat.KernelVCG]
Kbound_Kbounds [lemma, in Scat.KernelVCG]
Kbound_monotonic [lemma, in Scat.KernelVCG]
Kbranch [constructor, in Scat.Kernel]
Kbranch2 [constructor, in Scat.Kernel]
Kclone [constructor, in Scat.Kernel]
Kdeflabel [constructor, in Scat.Kernel]
kernel [inductive, in Scat.Kernel]
Kernel [library]
KernelProof [library]
KernelVCG [library]
Kgjoin [constructor, in Scat.Kernel]
Kiat [constructor, in Scat.Kernel]
Kiter_monotonic [lemma, in Scat.Kernel]
Kiter_proofs.k_monotonic [variable, in Scat.Kernel]
Kiter_proofs.k [variable, in Scat.Kernel]
Kiter_proofs [section, in Scat.Kernel]
Kjoin [constructor, in Scat.Kernel]
Kjoinch [constructor, in Scat.Kernel]
Kle_iter_monotonic [lemma, in Scat.Kernel]
Kle_iter [constructor, in Scat.Kernel]
Kloop [constructor, in Scat.Kernel]
Kseq [constructor, in Scat.Kernel]
KVCG [module, in Scat.KernelVCG]
Kvcg [definition, in Scat.KernelProof]
Kvcg_correctness [lemma, in Scat.KernelProof]
Kwlp [definition, in Scat.Kernel]
Kwlp_monotonic [lemma, in Scat.Kernel]
Kwlp_le_iter [definition, in Scat.Kernel]
Kwlp_iter [definition, in Scat.Kernel]

L

labid [projection, in Scat.Assertions]
labmax [projection, in Scat.Assertions]
labmin [projection, in Scat.Assertions]
labsent [definition, in Scat.Conditions]
ladd [definition, in Scat.Guassign]
ladd_frameeq_2 [lemma, in Scat.Guassign]
ladd_frameeq_1 [lemma, in Scat.Guassign]
lbound [definition, in Scat.Guassign]
lbounds [definition, in Scat.Guassign]
lbounds_Zle [lemma, in Scat.Guassign]
lbound_lbounds [lemma, in Scat.Guassign]
lbound_monotonic [lemma, in Scat.Guassign]
LE [constructor, in Scat.Conditions]
LetTerm [section, in Scat.BasicExamples]
LetTerm.annotated [variable, in Scat.BasicExamples]
LetTerm.annotatedy [variable, in Scat.BasicExamples]
LetTerm.source [variable, in Scat.BasicExamples]
LetTerm.x [variable, in Scat.BasicExamples]
LetTerm.y [variable, in Scat.BasicExamples]
LetTerm.z [variable, in Scat.BasicExamples]
le_iter_Kwlp [lemma, in Scat.LoopsUnrolling]
le_iter_continue [lemma, in Scat.LoopsUnrolling]
le_iter_stop [lemma, in Scat.LoopsUnrolling]
le_iter [definition, in Scat.LoopsUnrolling]
le_iter_tech3 [lemma, in Scat.KernelProof]
le_iter_tech2 [lemma, in Scat.KernelProof]
le_iter_tech1 [lemma, in Scat.KernelProof]
<<< _ , _ , _ , _ >>> [notation, in Scat.KernelProof]
Le_iter_proofs.next_kn [variable, in Scat.KernelProof]
Le_iter_proofs.body_kb [variable, in Scat.KernelProof]
Le_iter_proofs.kn_monotonic [variable, in Scat.KernelProof]
Le_iter_proofs.kb_monotonic [variable, in Scat.KernelProof]
Le_iter_proofs.next_reswf [variable, in Scat.KernelProof]
Le_iter_proofs.body_reswf [variable, in Scat.KernelProof]
Le_iter_proofs.bound1_bound2 [variable, in Scat.KernelProof]
Le_iter_proofs.next_increases_bound [variable, in Scat.KernelProof]
Le_iter_proofs.body_increases_bound [variable, in Scat.KernelProof]
Le_iter_proofs.next_renforce_vc [variable, in Scat.KernelProof]
Le_iter_proofs.body_renforce_vc [variable, in Scat.KernelProof]
Le_iter_proofs.bound2 [variable, in Scat.KernelProof]
Le_iter_proofs.bound1 [variable, in Scat.KernelProof]
Le_iter_proofs.kn [variable, in Scat.KernelProof]
Le_iter_proofs.kb [variable, in Scat.KernelProof]
Le_iter_proofs.next [variable, in Scat.KernelProof]
Le_iter_proofs.body [variable, in Scat.KernelProof]
Le_iter_proofs [section, in Scat.KernelProof]
lframeeq [definition, in Scat.Conditions]
lframeeq_cons_invert [lemma, in Scat.Guassign]
lframeeq_nil_invert [lemma, in Scat.Guassign]
lfresh [definition, in Scat.Guassign]
lfreshx [definition, in Scat.Guassign]
lfreshx_rbound [lemma, in Scat.Guassign]
lfreshx_rbounds [lemma, in Scat.Guassign]
lfresh_rbound [lemma, in Scat.Guassign]
lfresh_rbounds [lemma, in Scat.Guassign]
loop [constructor, in Scat.Concrete]
LoopExample [section, in Scat.BasicExamples]
LoopExample.annotated1 [variable, in Scat.BasicExamples]
LoopExample.annotated2 [variable, in Scat.BasicExamples]
LoopExample.i [variable, in Scat.BasicExamples]
LoopExample.label [variable, in Scat.BasicExamples]
LoopExample.r [variable, in Scat.BasicExamples]
LoopExample.source [variable, in Scat.BasicExamples]
LoopExample.x [variable, in Scat.BasicExamples]
LoopExample.y [variable, in Scat.BasicExamples]
LoopPost [constructor, in Scat.KernelVCG]
LoopPre [constructor, in Scat.KernelVCG]
LoopsUnrolling [library]
lvar_eq_lframeeq [lemma, in Scat.Conditions]
lvar_eq_labsent [lemma, in Scat.Conditions]
lvar_eq [definition, in Scat.Conditions]

M

MauborgneRival_Barycentre.annotated [variable, in Scat.Examples]
MauborgneRival_Barycentre.label [variable, in Scat.Examples]
MauborgneRival_Barycentre.source [variable, in Scat.Examples]
MauborgneRival_Barycentre.r [variable, in Scat.Examples]
MauborgneRival_Barycentre.y [variable, in Scat.Examples]
MauborgneRival_Barycentre.x [variable, in Scat.Examples]
MauborgneRival_Barycentre [section, in Scat.Examples]
MauborgneRival_LinearInterpolation.annotated [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.label [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.source [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.i [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.y [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.x [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.ty [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.tx [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.tc [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.ty_3 [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.ty_2 [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.ty_1 [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.ty_0 [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.tx_3 [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.tx_2 [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.tx_1 [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.tc_3 [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.tc_2 [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.tc_1 [variable, in Scat.Examples]
MauborgneRival_LinearInterpolation.tc_0 [variable, in Scat.Examples]
#ty [notation, in Scat.Examples]
#tx [notation, in Scat.Examples]
#tc [notation, in Scat.Examples]
MauborgneRival_LinearInterpolation [section, in Scat.Examples]
MinetBarycentreExample [section, in Scat.Examples]
MinetBarycentreExample.annotated [variable, in Scat.Examples]
MinetBarycentreExample.r [variable, in Scat.Examples]
MinetBarycentreExample.source [variable, in Scat.Examples]
MinetBarycentreExample.x [variable, in Scat.Examples]
MinetBarycentreExample.y [variable, in Scat.Examples]
MinetBarycentreExample.z [variable, in Scat.Examples]
MinetBarycentreExample2 [section, in Scat.Examples]
MinetBarycentreExample2.annotated [variable, in Scat.Examples]
MinetBarycentreExample2.label [variable, in Scat.Examples]
MinetBarycentreExample2.r [variable, in Scat.Examples]
MinetBarycentreExample2.source [variable, in Scat.Examples]
MinetBarycentreExample2.x [variable, in Scat.Examples]
MinetBarycentreExample2.y [variable, in Scat.Examples]
MinetBarycentreExample2.z [variable, in Scat.Examples]
MINUS [constructor, in Scat.Conditions]
MiscUtils [library]
Misc1 [section, in Scat.BasicExamples]
Misc1.annotated [variable, in Scat.BasicExamples]
Misc1.r [variable, in Scat.BasicExamples]
Misc1.x [variable, in Scat.BasicExamples]
Misc1.y [variable, in Scat.BasicExamples]
mkjoinlabel [definition, in Scat.Assertions]
mklabel [constructor, in Scat.Assertions]
mkseqlabel [definition, in Scat.Assertions]
mkvar [constructor, in Scat.Conditions]
MULT [constructor, in Scat.Conditions]
mult_interv_pos [definition, in Scat.NaiveAbstractionLib]
mult_up_pos [definition, in Scat.NaiveAbstractionLib]
mult_low_pos [definition, in Scat.NaiveAbstractionLib]
mult_left_cte [definition, in Scat.NaiveAbstractionLib]
mult_neg_interv [definition, in Scat.NaiveAbstractionLib]
mult_neg_up [definition, in Scat.NaiveAbstractionLib]
mult_neg_low [definition, in Scat.NaiveAbstractionLib]
mult_pos_interv [definition, in Scat.NaiveAbstractionLib]
mult_pos_up [definition, in Scat.NaiveAbstractionLib]
mult_pos_low [definition, in Scat.NaiveAbstractionLib]
mult_right_cte [definition, in Scat.NaiveAbstractionLib]

N

NaiveAbstractionLib [library]
NaiveGuardAbstractions [library]
NaiveTermAbstractions [library]
neg_left_le [lemma, in Scat.NaiveAbstractionLib]
normalize [definition, in Scat.Concrete]
normalize_bck_correctness [lemma, in Scat.Concrete]
normalize_fwd_correctness [lemma, in Scat.Concrete]
normalize_rec [definition, in Scat.Concrete]
not [constructor, in Scat.Conditions]
not_EQ [definition, in Scat.NaiveGuardAbstractions]
not_LE [definition, in Scat.NaiveGuardAbstractions]

O

oadd [definition, in Scat.Assertions]
oadd_aebounds [lemma, in Scat.Assertions]
oeval [definition, in Scat.Conditions]
oeval_eval [lemma, in Scat.Conditions]
ok [definition, in Scat.MiscUtils]
ok_monotonic [lemma, in Scat.MiscUtils]
ok_def [lemma, in Scat.MiscUtils]
OR [constructor, in Scat.Conditions]
orsubst [definition, in Scat.Renaming]
orsubst_eval_rlift [lemma, in Scat.Renaming]
orsubst_rempty [lemma, in Scat.Renaming]
oteval [definition, in Scat.Conditions]
oteval_teval [lemma, in Scat.Conditions]
otrsubst [definition, in Scat.Renaming]
otrsubst_eval_rlift [lemma, in Scat.Renaming]
otrsubst_rempty [lemma, in Scat.Renaming]

P

PLUS [constructor, in Scat.Conditions]
postfinder_Kwlp [definition, in Scat.KernelProof]
postfinder_cbounds_reswf [lemma, in Scat.KernelProof]
postfinder_increases_bound [definition, in Scat.KernelProof]
postfinder_renforce_vc [definition, in Scat.KernelProof]
postfinder_le_iter_Kwlp_2 [lemma, in Scat.KernelProof]
postfinder_le_iter_Kwlp_1 [lemma, in Scat.KernelProof]
postfinder_le_iter_reswf [lemma, in Scat.KernelProof]
postfinder_le_iter_cbounds_1 [lemma, in Scat.KernelProof]
postfinder_le_iter_increases_bound_2 [lemma, in Scat.KernelProof]
postfinder_le_iter_increases_bound_1 [lemma, in Scat.KernelProof]
postfinder_le_iter_renforce_vc [lemma, in Scat.KernelProof]
prog [inductive, in Scat.Concrete]
prog_eq_isok [lemma, in Scat.Concrete]
prog_eq_normalize_wlp [lemma, in Scat.Concrete]
prog_eq_wlp [lemma, in Scat.Concrete]
prog_eq [definition, in Scat.Concrete]
Psucc_lift [lemma, in Scat.Renaming]

R

rbound [projection, in Scat.Renaming]
rbounds [definition, in Scat.Renaming]
rbounds_rfind_down [lemma, in Scat.Renaming]
rbounds_rfind_up [lemma, in Scat.Renaming]
rbounds_Zle [lemma, in Scat.Renaming]
rbounds_rbound [lemma, in Scat.Renaming]
rempty [definition, in Scat.Renaming]
rempty_rlift [lemma, in Scat.Renaming]
rempty_rfind [lemma, in Scat.Renaming]
rempty_rbounds [lemma, in Scat.Renaming]
rename [definition, in Scat.Renaming]
rename_cbounds [lemma, in Scat.Renaming]
renaming [record, in Scat.Renaming]
Renaming [library]
Req [constructor, in Scat.KernelVCG]
require [definition, in Scat.Atoms]
rewriting1 [definition, in Scat.Examples]
rfind [definition, in Scat.Renaming]
rfind_fresh [lemma, in Scat.Renaming]
rfind_fresh_in [lemma, in Scat.Renaming]
rlift [definition, in Scat.Renaming]
rlift_fresh_tech [lemma, in Scat.Renaming]
rlift_fresh [lemma, in Scat.Renaming]
rlift_add_out_2 [lemma, in Scat.Renaming]
rlift_frameeq [lemma, in Scat.Renaming]
rlift_rfind [lemma, in Scat.Renaming]
rmap [projection, in Scat.Renaming]
rsubst [definition, in Scat.Renaming]
rsubst_fresh_cbounds [lemma, in Scat.Renaming]
rsubst_eval_rlift [lemma, in Scat.Renaming]
rsubst_rempty [lemma, in Scat.Renaming]
RunningExample [section, in Scat.Examples]
RunningExample.annotated [variable, in Scat.Examples]
RunningExample.convexhull [variable, in Scat.Examples]
RunningExample.label [variable, in Scat.Examples]
RunningExample.r [variable, in Scat.Examples]
RunningExample.source [variable, in Scat.Examples]
RunningExample.x [variable, in Scat.Examples]
RunningExample.y [variable, in Scat.Examples]
rwin [projection, in Scat.NaiveTermAbstractions]
rwproof [projection, in Scat.NaiveTermAbstractions]

S

safe_branch_ind [lemma, in Scat.Assertions]
safe_branch [definition, in Scat.Assertions]
sem [inductive, in Scat.Concrete]
sem_loop_ko [constructor, in Scat.Concrete]
sem_loop_continue [constructor, in Scat.Concrete]
sem_loop_stop [constructor, in Scat.Concrete]
sem_join_r [constructor, in Scat.Concrete]
sem_join_l [constructor, in Scat.Concrete]
sem_seq_ko [constructor, in Scat.Concrete]
sem_seq [constructor, in Scat.Concrete]
sem_iat [constructor, in Scat.Concrete]
seq [definition, in Scat.Certificate]
seq [constructor, in Scat.Concrete]
seqlabel [definition, in Scat.Certificate]
seq_outskip [definition, in Scat.Concrete]
simple [constructor, in Scat.Assertions]
skip [constructor, in Scat.Atoms]
split_le [lemma, in Scat.BoundedIteration]
state [definition, in Scat.Conditions]
stdloop [definition, in Scat.Certificate]
swap [definition, in Scat.Renaming]
swap_rlift [lemma, in Scat.Renaming]
swap_rfind_3 [lemma, in Scat.Renaming]
swap_rfind_2 [lemma, in Scat.Renaming]
swap_rfind_1 [lemma, in Scat.Renaming]
swap_rfind [lemma, in Scat.Renaming]
swap_rbounds [lemma, in Scat.Renaming]

T

tabs [projection, in Scat.NaiveTermAbstractions]
tapp [constructor, in Scat.Conditions]
tauto [definition, in Scat.Conditions]
tbin [constructor, in Scat.Conditions]
tbind [definition, in Scat.NaiveTermAbstractions]
tbound [definition, in Scat.Renaming]
tbounds [definition, in Scat.Renaming]
tbounds_otrsubst [lemma, in Scat.Renaming]
tbounds_trsubst [lemma, in Scat.Renaming]
tbounds_trename [lemma, in Scat.Renaming]
tbounds_Zle [lemma, in Scat.Renaming]
tbound_tbounds [lemma, in Scat.Renaming]
tbound_monotonic [lemma, in Scat.Renaming]
tbranch2 [definition, in Scat.NaiveTermAbstractions]
tconc [projection, in Scat.NaiveTermAbstractions]
tcte [constructor, in Scat.Conditions]
term [inductive, in Scat.Conditions]
term_eq_oeval [lemma, in Scat.Conditions]
term_eq_eval [lemma, in Scat.Conditions]
term_eq [definition, in Scat.Conditions]
term_rewrite [record, in Scat.NaiveTermAbstractions]
teval [definition, in Scat.Conditions]
told [constructor, in Scat.Conditions]
tproof [projection, in Scat.NaiveTermAbstractions]
trace [inductive, in Scat.KernelVCG]
trename [definition, in Scat.Renaming]
trename_tbounds [lemma, in Scat.Renaming]
tret [definition, in Scat.NaiveTermAbstractions]
trsubst [definition, in Scat.Renaming]
trsubst_rempty [lemma, in Scat.Renaming]
trsubst_teval_rlift [lemma, in Scat.Renaming]
try [definition, in Scat.MiscUtils]
try_monotonic [lemma, in Scat.MiscUtils]
try_def [lemma, in Scat.MiscUtils]
tsubst [definition, in Scat.Conditions]
tsubst_teval [lemma, in Scat.Conditions]
tvar [constructor, in Scat.Conditions]

U

Unchecked_Union [constructor, in Scat.KernelVCG]
unrollfwd [definition, in Scat.LoopsUnrolling]
unroll_all [definition, in Scat.LoopsUnrolling]
unroll_fwd_sem [lemma, in Scat.LoopsUnrolling]
UnroolBasicExample [section, in Scat.BasicExamples]
UnroolBasicExample.annotated [variable, in Scat.BasicExamples]
UnroolBasicExample.i [variable, in Scat.BasicExamples]
UnroolBasicExample.r [variable, in Scat.BasicExamples]
UnroolBasicExample.source [variable, in Scat.BasicExamples]
UnroolBasicExample.x [variable, in Scat.BasicExamples]
UnroolBasicExample.y [variable, in Scat.BasicExamples]

V

Value [module, in Scat.Conditions]
ValueTypeAbstraction [module, in Scat.Conditions]
ValueTypeAbstraction.value [axiom, in Scat.Conditions]
ValueTypeAbstraction.vbin [axiom, in Scat.Conditions]
ValueTypeAbstraction.vcte [axiom, in Scat.Conditions]
ValueTypeAbstraction.vcte_Zof [axiom, in Scat.Conditions]
ValueTypeAbstraction.Zof [axiom, in Scat.Conditions]
ValueTypeAbstraction.Zof_vbin [axiom, in Scat.Conditions]
ValueTypeAbstraction.Zof_vcte [axiom, in Scat.Conditions]
Value.value [definition, in Scat.Conditions]
Value.vbin [definition, in Scat.Conditions]
Value.vcte [definition, in Scat.Conditions]
Value.vcte_Zof [lemma, in Scat.Conditions]
Value.Zof [definition, in Scat.Conditions]
Value.Zof_vbin [lemma, in Scat.Conditions]
Value.Zof_vcte [lemma, in Scat.Conditions]
var [record, in Scat.Conditions]
var_eq_eq [lemma, in Scat.Conditions]
var_eq [definition, in Scat.Conditions]
vcg [definition, in Scat.Certificate]
VCGparameters [module, in Scat.KernelVCG]
VCGparameters.absurd [axiom, in Scat.KernelVCG]
VCGparameters.bind [axiom, in Scat.KernelVCG]
VCGparameters.ceq [axiom, in Scat.KernelVCG]
VCGparameters.check_entails [axiom, in Scat.KernelVCG]
VCGparameters.hard_and [axiom, in Scat.KernelVCG]
VCGparameters.monad [axiom, in Scat.KernelVCG]
VCGparameters.rename [axiom, in Scat.KernelVCG]
VCGparameters.ret [axiom, in Scat.KernelVCG]
VCGparameters.soft_or [axiom, in Scat.KernelVCG]
VCGparameters.tauto [axiom, in Scat.KernelVCG]
VCGparameters.trename [axiom, in Scat.KernelVCG]
{ _ # _ # _ |= _ } _ (VCG_scope) [notation, in Scat.KernelVCG]
do _ <- _ ; _ (VCG_scope) [notation, in Scat.KernelVCG]
vcg_correctness [lemma, in Scat.Certificate]
vcg_simple_correctness [lemma, in Scat.Certificate]
vc_eval [definition, in Scat.KernelVCG]
vid [projection, in Scat.Conditions]
vid_rfind [lemma, in Scat.Renaming]
vle [inductive, in Scat.Conditions]
vlecons [constructor, in Scat.Conditions]
vtag [projection, in Scat.Conditions]

W

wlp [definition, in Scat.Concrete]
wlp_succ_iter [lemma, in Scat.LoopsUnrolling]
wlp_unroll_fwd_correctness [lemma, in Scat.LoopsUnrolling]
wlp_normalize_rec_bck [lemma, in Scat.Concrete]
wlp_seq_outskip_bck [lemma, in Scat.Concrete]
wlp_normalize_rec_fwd [lemma, in Scat.Concrete]
wlp_seq_outskip_fwd [lemma, in Scat.Concrete]
wlp_complete [lemma, in Scat.Concrete]
wlp_isok [lemma, in Scat.Concrete]
wlp_correctness [lemma, in Scat.Concrete]
wlp_monotonic [lemma, in Scat.Concrete]

X

xrequire [constructor, in Scat.Atoms]

Z

Zdiv_by_pos_cte [definition, in Scat.NaiveAbstractionLib]
Zexists [definition, in Scat.BoundedIteration]
zexists_monotonic [lemma, in Scat.BoundedIteration]
Zexists_spec_2 [lemma, in Scat.BoundedIteration]
Zexists_spec_1 [lemma, in Scat.BoundedIteration]
Zforall [definition, in Scat.BoundedIteration]
Zforall_spec_2 [lemma, in Scat.BoundedIteration]
Zforall_spec_1 [lemma, in Scat.BoundedIteration]
Zle_Pmax_r [lemma, in Scat.Renaming]
Zle_Pmax_l [lemma, in Scat.Renaming]
Zof_intro [lemma, in Scat.Conditions]
Zpos_Psucc_le [lemma, in Scat.Renaming]
Zpos_Psucc_lt [lemma, in Scat.Renaming]

other

_ & _ (assertion_scope) [notation, in Scat.BasicExamples]
let_term _ := _ in _ (certif_scope) [notation, in Scat.NaiveTermAbstractions]
bloop _ invariant _ done (certif_scope) [notation, in Scat.Certificate]
_ -;[ _ ] _ (certif_scope) [notation, in Scat.Certificate]
_ -; _ (certif_scope) [notation, in Scat.Certificate]
bloop split _ _ all _ then _ done (certif_scope) [notation, in Scat.LoopsUnrolling]
bloop _ fwd _ invariant _ then _ done (certif_scope) [notation, in Scat.LoopsUnrolling]
_ = _ (cond_scope) [notation, in Scat.NaiveAbstractionLib]
_ <= _ (cond_scope) [notation, in Scat.NaiveAbstractionLib]
_ \/ _ (cond_scope) [notation, in Scat.NaiveAbstractionLib]
_ /\ _ (cond_scope) [notation, in Scat.NaiveAbstractionLib]
[ _ ; .. ; _ ] (list_scope) [notation, in Scat.NaiveTermAbstractions]
bloop _ done (prog_scope) [notation, in Scat.BasicExamples]
while _ do _ done (prog_scope) [notation, in Scat.Concrete]
ifc _ then _ else _ fi (prog_scope) [notation, in Scat.Concrete]
_ -; _ (prog_scope) [notation, in Scat.Concrete]
_ ! _ (term_scope) [notation, in Scat.BasicExamples]
_ / _ (term_scope) [notation, in Scat.NaiveAbstractionLib]
_ * _ (term_scope) [notation, in Scat.NaiveAbstractionLib]
_ - _ (term_scope) [notation, in Scat.NaiveAbstractionLib]
_ + _ (term_scope) [notation, in Scat.NaiveAbstractionLib]
reswf _ [notation, in Scat.KernelProof]

Projection Index

A

abranch [in Scat.Assertions]
abstract [in Scat.Certificate]
acond [in Scat.Assertions]

C

certif_correctness [in Scat.Certificate]
concrete [in Scat.Certificate]
ConcreteCondWrapper.goal [in Scat.KernelVCG]
ConcreteCondWrapper.hyp [in Scat.KernelVCG]
ConcreteCondWrapper.mesg [in Scat.KernelVCG]
ConcreteCondWrapper.tbnd [in Scat.KernelVCG]
ConcreteCondWrapper.value [in Scat.KernelVCG]
ConcreteCondWrapper.vcl [in Scat.KernelVCG]

G

gabs [in Scat.NaiveGuardAbstractions]
gconc [in Scat.NaiveGuardAbstractions]
GenericVCG.pbnd [in Scat.KernelVCG]
GenericVCG.post [in Scat.KernelVCG]
gproof [in Scat.NaiveGuardAbstractions]

H

hname [in Scat.NaiveTermAbstractions]
htpost [in Scat.NaiveTermAbstractions]
htpre [in Scat.NaiveTermAbstractions]
htproof [in Scat.NaiveTermAbstractions]

L

labid [in Scat.Assertions]
labmax [in Scat.Assertions]
labmin [in Scat.Assertions]

R

rbound [in Scat.Renaming]
rmap [in Scat.Renaming]
rwin [in Scat.NaiveTermAbstractions]
rwproof [in Scat.NaiveTermAbstractions]

T

tabs [in Scat.NaiveTermAbstractions]
tconc [in Scat.NaiveTermAbstractions]
tproof [in Scat.NaiveTermAbstractions]

V

vid [in Scat.Conditions]
vtag [in Scat.Conditions]

Record Index

A

abs_term [in Scat.NaiveTermAbstractions]
abs_guard [in Scat.NaiveGuardAbstractions]
aentry [in Scat.Assertions]
alabel [in Scat.Assertions]

C

certif [in Scat.Certificate]
ConcreteCondWrapper.result [in Scat.KernelVCG]
ConcreteCondWrapper.VC [in Scat.KernelVCG]

G

GenericVCG.postfinder_result [in Scat.KernelVCG]

H

hoare_term [in Scat.NaiveTermAbstractions]

R

renaming [in Scat.Renaming]

T

term_rewrite [in Scat.NaiveTermAbstractions]

V

var [in Scat.Conditions]

Lemma Index

A

aadd_aebounds [in Scat.Assertions]
abounds_Zle [in Scat.Assertions]
abound_abounds [in Scat.Assertions]
abound_monotonic [in Scat.Assertions]
add_id [in Scat.Conditions]
add_out2 [in Scat.Conditions]
add_out [in Scat.Conditions]
add_in [in Scat.Conditions]
add_tech2 [in Scat.Guassign]
add_tech1 [in Scat.Guassign]
add_frameeq_out_2 [in Scat.Renaming]
add_frameeq_out_1 [in Scat.Renaming]
add_morphism [in Scat.Renaming]
aebounds_Zle [in Scat.Assertions]
aempty_aebounds [in Scat.Assertions]
aeval_bounds [in Scat.Assertions]
angel_awlp_duality [in Scat.Atoms]
angel_awlp_monotonic [in Scat.Atoms]
annotated1_proof [in Scat.BasicExamples]
annotated2_proof [in Scat.BasicExamples]
atbounds_Zle [in Scat.KernelVCG]
atbound_atbounds [in Scat.KernelVCG]
atbound_monotonic [in Scat.KernelVCG]
atom_eq_awlp [in Scat.Atoms]
atpostfinder_awlp [in Scat.KernelProof]
atpostfinder_cbounds_post [in Scat.KernelProof]
atpostfinder_increases_bound [in Scat.KernelProof]
atpostfinder_renforce_vc [in Scat.KernelProof]
awlp_complete [in Scat.Atoms]
awlp_correctness [in Scat.Atoms]
awlp_monotonic [in Scat.Atoms]

B

bincmp_eq_refl [in Scat.Conditions]
bincmp_eq_eq [in Scat.Conditions]
binlog_eq_refl [in Scat.Conditions]
binlog_eq_eq [in Scat.Conditions]
binop_eq_refl [in Scat.Conditions]
binop_eq_eq [in Scat.Conditions]
biter_succ [in Scat.BoundedIteration]
biter_one [in Scat.BoundedIteration]
biter_zero [in Scat.BoundedIteration]
biter_spec [in Scat.BoundedIteration]
biter_nat_aux [in Scat.BoundedIteration]
biter_nat_spec_1 [in Scat.BoundedIteration]
bounder_iter_nat_spec [in Scat.BoundedIteration]
bound_Kbounds [in Scat.KernelVCG]

C

cbounds_orsubst [in Scat.Renaming]
cbounds_rsubst [in Scat.Renaming]
cbounds_rename [in Scat.Renaming]
cbounds_Zle [in Scat.Renaming]
cbound_cbounds [in Scat.Renaming]
cbound_monotonic [in Scat.Renaming]
cond_eq_oeval [in Scat.Conditions]
cond_eq_eval [in Scat.Conditions]
ctefun_Zof [in Scat.Conditions]

D

dbiter_nat_spec [in Scat.BoundedIteration]
dbiter_natx_spec [in Scat.BoundedIteration]

E

eval_orsubst [in Scat.Guassign]
eval_orsubst_lfreshx [in Scat.Guassign]
eval_rsubst [in Scat.Guassign]
eval_rsubst_lfreshx [in Scat.Guassign]
ext_eval [in Scat.Conditions]
ext_teval [in Scat.Conditions]
ex_monotonic [in Scat.MiscUtils]

F

frameeq_oeval [in Scat.Renaming]
frameeq_oteval [in Scat.Renaming]
frameeq_eval_imp_s [in Scat.Renaming]
frameeq_eval_imp [in Scat.Renaming]
frameeq_eval [in Scat.Renaming]
frameeq_teval [in Scat.Renaming]
frameeq_glue [in Scat.Renaming]
frameeq_trans [in Scat.Renaming]
frameeq_sym [in Scat.Renaming]
frameeq_Zle [in Scat.Renaming]
fresh_rbounds [in Scat.Renaming]

G

guassign_vc [in Scat.Guassign]

I

isok_wlp [in Scat.Concrete]
iter_Kwlp [in Scat.LoopsUnrolling]

K

Kangel_wlp_correctness [in Scat.Kernel]
Kangel_wlp_duality [in Scat.Kernel]
Kangel_wlp_monotonic [in Scat.Kernel]
Kbounds_Zle [in Scat.KernelVCG]
Kbound_Kbounds [in Scat.KernelVCG]
Kbound_monotonic [in Scat.KernelVCG]
Kiter_monotonic [in Scat.Kernel]
Kle_iter_monotonic [in Scat.Kernel]
Kvcg_correctness [in Scat.KernelProof]
Kwlp_monotonic [in Scat.Kernel]

L

ladd_frameeq_2 [in Scat.Guassign]
ladd_frameeq_1 [in Scat.Guassign]
lbounds_Zle [in Scat.Guassign]
lbound_lbounds [in Scat.Guassign]
lbound_monotonic [in Scat.Guassign]
le_iter_Kwlp [in Scat.LoopsUnrolling]
le_iter_continue [in Scat.LoopsUnrolling]
le_iter_stop [in Scat.LoopsUnrolling]
le_iter_tech3 [in Scat.KernelProof]
le_iter_tech2 [in Scat.KernelProof]
le_iter_tech1 [in Scat.KernelProof]
lframeeq_cons_invert [in Scat.Guassign]
lframeeq_nil_invert [in Scat.Guassign]
lfreshx_rbound [in Scat.Guassign]
lfreshx_rbounds [in Scat.Guassign]
lfresh_rbound [in Scat.Guassign]
lfresh_rbounds [in Scat.Guassign]
lvar_eq_lframeeq [in Scat.Conditions]
lvar_eq_labsent [in Scat.Conditions]

N

neg_left_le [in Scat.NaiveAbstractionLib]
normalize_bck_correctness [in Scat.Concrete]
normalize_fwd_correctness [in Scat.Concrete]

O

oadd_aebounds [in Scat.Assertions]
oeval_eval [in Scat.Conditions]
ok_monotonic [in Scat.MiscUtils]
ok_def [in Scat.MiscUtils]
orsubst_eval_rlift [in Scat.Renaming]
orsubst_rempty [in Scat.Renaming]
oteval_teval [in Scat.Conditions]
otrsubst_eval_rlift [in Scat.Renaming]
otrsubst_rempty [in Scat.Renaming]

P

postfinder_cbounds_reswf [in Scat.KernelProof]
postfinder_le_iter_Kwlp_2 [in Scat.KernelProof]
postfinder_le_iter_Kwlp_1 [in Scat.KernelProof]
postfinder_le_iter_reswf [in Scat.KernelProof]
postfinder_le_iter_cbounds_1 [in Scat.KernelProof]
postfinder_le_iter_increases_bound_2 [in Scat.KernelProof]
postfinder_le_iter_increases_bound_1 [in Scat.KernelProof]
postfinder_le_iter_renforce_vc [in Scat.KernelProof]
prog_eq_isok [in Scat.Concrete]
prog_eq_normalize_wlp [in Scat.Concrete]
prog_eq_wlp [in Scat.Concrete]
Psucc_lift [in Scat.Renaming]

R

rbounds_rfind_down [in Scat.Renaming]
rbounds_rfind_up [in Scat.Renaming]
rbounds_Zle [in Scat.Renaming]
rbounds_rbound [in Scat.Renaming]
rempty_rlift [in Scat.Renaming]
rempty_rfind [in Scat.Renaming]
rempty_rbounds [in Scat.Renaming]
rename_cbounds [in Scat.Renaming]
rfind_fresh [in Scat.Renaming]
rfind_fresh_in [in Scat.Renaming]
rlift_fresh_tech [in Scat.Renaming]
rlift_fresh [in Scat.Renaming]
rlift_add_out_2 [in Scat.Renaming]
rlift_frameeq [in Scat.Renaming]
rlift_rfind [in Scat.Renaming]
rsubst_fresh_cbounds [in Scat.Renaming]
rsubst_eval_rlift [in Scat.Renaming]
rsubst_rempty [in Scat.Renaming]

S

safe_branch_ind [in Scat.Assertions]
split_le [in Scat.BoundedIteration]
swap_rlift [in Scat.Renaming]
swap_rfind_3 [in Scat.Renaming]
swap_rfind_2 [in Scat.Renaming]
swap_rfind_1 [in Scat.Renaming]
swap_rfind [in Scat.Renaming]
swap_rbounds [in Scat.Renaming]

T

tbounds_otrsubst [in Scat.Renaming]
tbounds_trsubst [in Scat.Renaming]
tbounds_trename [in Scat.Renaming]
tbounds_Zle [in Scat.Renaming]
tbound_tbounds [in Scat.Renaming]
tbound_monotonic [in Scat.Renaming]
term_eq_oeval [in Scat.Conditions]
term_eq_eval [in Scat.Conditions]
trename_tbounds [in Scat.Renaming]
trsubst_rempty [in Scat.Renaming]
trsubst_teval_rlift [in Scat.Renaming]
try_monotonic [in Scat.MiscUtils]
try_def [in Scat.MiscUtils]
tsubst_teval [in Scat.Conditions]

U

unroll_fwd_sem [in Scat.LoopsUnrolling]

V

Value.vcte_Zof [in Scat.Conditions]
Value.Zof_vbin [in Scat.Conditions]
Value.Zof_vcte [in Scat.Conditions]
var_eq_eq [in Scat.Conditions]
vcg_correctness [in Scat.Certificate]
vcg_simple_correctness [in Scat.Certificate]
vid_rfind [in Scat.Renaming]

W

wlp_succ_iter [in Scat.LoopsUnrolling]
wlp_unroll_fwd_correctness [in Scat.LoopsUnrolling]
wlp_normalize_rec_bck [in Scat.Concrete]
wlp_seq_outskip_bck [in Scat.Concrete]
wlp_normalize_rec_fwd [in Scat.Concrete]
wlp_seq_outskip_fwd [in Scat.Concrete]
wlp_complete [in Scat.Concrete]
wlp_isok [in Scat.Concrete]
wlp_correctness [in Scat.Concrete]
wlp_monotonic [in Scat.Concrete]

Z

zexists_monotonic [in Scat.BoundedIteration]
Zexists_spec_2 [in Scat.BoundedIteration]
Zexists_spec_1 [in Scat.BoundedIteration]
Zforall_spec_2 [in Scat.BoundedIteration]
Zforall_spec_1 [in Scat.BoundedIteration]
Zle_Pmax_r [in Scat.Renaming]
Zle_Pmax_l [in Scat.Renaming]
Zof_intro [in Scat.Conditions]
Zpos_Psucc_le [in Scat.Renaming]
Zpos_Psucc_lt [in Scat.Renaming]

Section Index

A

AbstractionExample [in Scat.BasicExamples]

G

GenericVCG.VCGCode [in Scat.KernelVCG]
GuassignExample [in Scat.BasicExamples]

J

JoinseqUnrollInvariant [in Scat.Examples]

K

Kiter_proofs [in Scat.Kernel]

L

LetTerm [in Scat.BasicExamples]
Le_iter_proofs [in Scat.KernelProof]
LoopExample [in Scat.BasicExamples]

M

MauborgneRival_Barycentre [in Scat.Examples]
MauborgneRival_LinearInterpolation [in Scat.Examples]
MinetBarycentreExample [in Scat.Examples]
MinetBarycentreExample2 [in Scat.Examples]
Misc1 [in Scat.BasicExamples]

R

RunningExample [in Scat.Examples]

U

UnroolBasicExample [in Scat.BasicExamples]

Constructor Index

A

AND [in Scat.Conditions]
asem_assign [in Scat.Atoms]
asem_ensure [in Scat.Atoms]
asem_req_ko [in Scat.Atoms]
asem_req_ok [in Scat.Atoms]
asem_skip [in Scat.Atoms]
asem_guassign [in Scat.Atoms]
assign [in Scat.Atoms]
atom [in Scat.Conditions]

B

basic [in Scat.Conditions]
bin [in Scat.Conditions]
branch [in Scat.Assertions]
branch2 [in Scat.Assertions]

C

conj [in Scat.Assertions]

D

DIV [in Scat.Conditions]

E

ensure [in Scat.Atoms]
EQ [in Scat.Conditions]

G

guassign [in Scat.Atoms]

I

iat [in Scat.Concrete]
inv [in Scat.Assertions]

J

join [in Scat.Concrete]

K

Kbranch [in Scat.Kernel]
Kbranch2 [in Scat.Kernel]
Kclone [in Scat.Kernel]
Kdeflabel [in Scat.Kernel]
Kgjoin [in Scat.Kernel]
Kiat [in Scat.Kernel]
Kjoin [in Scat.Kernel]
Kjoinch [in Scat.Kernel]
Kle_iter [in Scat.Kernel]
Kloop [in Scat.Kernel]
Kseq [in Scat.Kernel]

L

LE [in Scat.Conditions]
loop [in Scat.Concrete]
LoopPost [in Scat.KernelVCG]
LoopPre [in Scat.KernelVCG]

M

MINUS [in Scat.Conditions]
mklabel [in Scat.Assertions]
mkvar [in Scat.Conditions]
MULT [in Scat.Conditions]

N

not [in Scat.Conditions]

O

OR [in Scat.Conditions]

P

PLUS [in Scat.Conditions]

R

Req [in Scat.KernelVCG]

S

sem_loop_ko [in Scat.Concrete]
sem_loop_continue [in Scat.Concrete]
sem_loop_stop [in Scat.Concrete]
sem_join_r [in Scat.Concrete]
sem_join_l [in Scat.Concrete]
sem_seq_ko [in Scat.Concrete]
sem_seq [in Scat.Concrete]
sem_iat [in Scat.Concrete]
seq [in Scat.Concrete]
simple [in Scat.Assertions]
skip [in Scat.Atoms]

T

tapp [in Scat.Conditions]
tbin [in Scat.Conditions]
tcte [in Scat.Conditions]
told [in Scat.Conditions]
tvar [in Scat.Conditions]

U

Unchecked_Union [in Scat.KernelVCG]

V

vlecons [in Scat.Conditions]

X

xrequire [in Scat.Atoms]

Notation Index

L

<<< _ , _ , _ , _ >>> [in Scat.KernelProof]

M

#ty [in Scat.Examples]
#tx [in Scat.Examples]
#tc [in Scat.Examples]

V

{ _ # _ # _ |= _ } _ (VCG_scope) [in Scat.KernelVCG]
do _ <- _ ; _ (VCG_scope) [in Scat.KernelVCG]

other

_ & _ (assertion_scope) [in Scat.BasicExamples]
let_term _ := _ in _ (certif_scope) [in Scat.NaiveTermAbstractions]
bloop _ invariant _ done (certif_scope) [in Scat.Certificate]
_ -;[ _ ] _ (certif_scope) [in Scat.Certificate]
_ -; _ (certif_scope) [in Scat.Certificate]
bloop split _ _ all _ then _ done (certif_scope) [in Scat.LoopsUnrolling]
bloop _ fwd _ invariant _ then _ done (certif_scope) [in Scat.LoopsUnrolling]
_ = _ (cond_scope) [in Scat.NaiveAbstractionLib]
_ <= _ (cond_scope) [in Scat.NaiveAbstractionLib]
_ \/ _ (cond_scope) [in Scat.NaiveAbstractionLib]
_ /\ _ (cond_scope) [in Scat.NaiveAbstractionLib]
[ _ ; .. ; _ ] (list_scope) [in Scat.NaiveTermAbstractions]
bloop _ done (prog_scope) [in Scat.BasicExamples]
while _ do _ done (prog_scope) [in Scat.Concrete]
ifc _ then _ else _ fi (prog_scope) [in Scat.Concrete]
_ -; _ (prog_scope) [in Scat.Concrete]
_ ! _ (term_scope) [in Scat.BasicExamples]
_ / _ (term_scope) [in Scat.NaiveAbstractionLib]
_ * _ (term_scope) [in Scat.NaiveAbstractionLib]
_ - _ (term_scope) [in Scat.NaiveAbstractionLib]
_ + _ (term_scope) [in Scat.NaiveAbstractionLib]
reswf _ [in Scat.KernelProof]

Inductive Index

A

asem [in Scat.Atoms]
assertion [in Scat.Assertions]
atom [in Scat.Atoms]

B

bincmp [in Scat.Conditions]
binlog [in Scat.Conditions]
binop [in Scat.Conditions]

C

cond [in Scat.Conditions]

K

kernel [in Scat.Kernel]

P

prog [in Scat.Concrete]

S

sem [in Scat.Concrete]

T

term [in Scat.Conditions]
trace [in Scat.KernelVCG]

V

vle [in Scat.Conditions]

Definition Index

A

aadd [in Scat.Assertions]
abound [in Scat.Assertions]
abounds [in Scat.Assertions]
absurd [in Scat.Conditions]
abs_rewrite [in Scat.NaiveTermAbstractions]
abs_simplify_pre [in Scat.NaiveTermAbstractions]
abs_rename [in Scat.NaiveTermAbstractions]
abs_conj [in Scat.NaiveTermAbstractions]
abs_coerce [in Scat.NaiveTermAbstractions]
abs_assign [in Scat.NaiveTermAbstractions]
abs_not [in Scat.NaiveGuardAbstractions]
abs_notx [in Scat.NaiveGuardAbstractions]
abs_cut [in Scat.NaiveGuardAbstractions]
abs_atom [in Scat.NaiveGuardAbstractions]
abs_or [in Scat.NaiveGuardAbstractions]
abs_and [in Scat.NaiveGuardAbstractions]
abs_embed [in Scat.NaiveGuardAbstractions]
abs_ensure [in Scat.NaiveGuardAbstractions]
add [in Scat.Conditions]
adefault [in Scat.Assertions]
aebounds [in Scat.Assertions]
aempty [in Scat.Assertions]
aenvironment [in Scat.Assertions]
aeval [in Scat.Assertions]
afind [in Scat.Assertions]
angel_awlp [in Scat.Atoms]
atbound [in Scat.KernelVCG]
atbounds [in Scat.KernelVCG]
atom_eq [in Scat.Atoms]
awlp [in Scat.Atoms]

B

bincmp_eq [in Scat.Conditions]
binlog_eq [in Scat.Conditions]
binop_eq [in Scat.Conditions]
biter [in Scat.BoundedIteration]
biter_nat [in Scat.BoundedIteration]
bound [in Scat.KernelVCG]

C

casescmp [in Scat.NaiveAbstractionLib]
cbound [in Scat.Renaming]
cbounds [in Scat.Renaming]
cbranch [in Scat.Certificate]
cbranch2 [in Scat.Certificate]
ceq [in Scat.Conditions]
cjoin [in Scat.Certificate]
ConcreteCondWrapper.absurd [in Scat.KernelVCG]
ConcreteCondWrapper.bind [in Scat.KernelVCG]
ConcreteCondWrapper.ceq [in Scat.KernelVCG]
ConcreteCondWrapper.check_entails [in Scat.KernelVCG]
ConcreteCondWrapper.hard_and [in Scat.KernelVCG]
ConcreteCondWrapper.monad [in Scat.KernelVCG]
ConcreteCondWrapper.rename [in Scat.KernelVCG]
ConcreteCondWrapper.ret [in Scat.KernelVCG]
ConcreteCondWrapper.soft_or [in Scat.KernelVCG]
ConcreteCondWrapper.tauto [in Scat.KernelVCG]
ConcreteCondWrapper.trename [in Scat.KernelVCG]
cond_eq [in Scat.Conditions]
coq_abs_conj [in Scat.NaiveTermAbstractions]

D

dbiter_nat [in Scat.BoundedIteration]
dbiter_natx [in Scat.BoundedIteration]
dead [in Scat.Certificate]

E

eval [in Scat.Conditions]
evalcmp [in Scat.Conditions]
evallog [in Scat.Conditions]
evalop [in Scat.Conditions]
explore [in Scat.NaiveAbstractionLib]
ext [in Scat.Conditions]
extend [in Scat.Renaming]
extract [in Scat.Certificate]

F

frameeq [in Scat.Renaming]
fresh [in Scat.Renaming]

G

GenericVCG.atpostfinder [in Scat.KernelVCG]
GenericVCG.internal_error [in Scat.KernelVCG]
GenericVCG.Kvcgen [in Scat.KernelVCG]
GenericVCG.postfinder [in Scat.KernelVCG]
GenericVCG.postfinder_le_iter [in Scat.KernelVCG]

H

hoare_abs [in Scat.NaiveTermAbstractions]
htb2 [in Scat.NaiveTermAbstractions]
ht_branch [in Scat.NaiveTermAbstractions]
ht_branch2 [in Scat.NaiveTermAbstractions]

I

iat [in Scat.Certificate]
is_ok [in Scat.Concrete]
iter [in Scat.LoopsUnrolling]

J

joinchseq [in Scat.Certificate]
joinseq [in Scat.Certificate]

K

Kangel_wlp [in Scat.Kernel]
Kbound [in Scat.KernelVCG]
Kbounds [in Scat.KernelVCG]
Kvcg [in Scat.KernelProof]
Kwlp [in Scat.Kernel]
Kwlp_le_iter [in Scat.Kernel]
Kwlp_iter [in Scat.Kernel]

L

labsent [in Scat.Conditions]
ladd [in Scat.Guassign]
lbound [in Scat.Guassign]
lbounds [in Scat.Guassign]
le_iter [in Scat.LoopsUnrolling]
lframeeq [in Scat.Conditions]
lfresh [in Scat.Guassign]
lfreshx [in Scat.Guassign]
lvar_eq [in Scat.Conditions]

M

mkjoinlabel [in Scat.Assertions]
mkseqlabel [in Scat.Assertions]
mult_interv_pos [in Scat.NaiveAbstractionLib]
mult_up_pos [in Scat.NaiveAbstractionLib]
mult_low_pos [in Scat.NaiveAbstractionLib]
mult_left_cte [in Scat.NaiveAbstractionLib]
mult_neg_interv [in Scat.NaiveAbstractionLib]
mult_neg_up [in Scat.NaiveAbstractionLib]
mult_neg_low [in Scat.NaiveAbstractionLib]
mult_pos_interv [in Scat.NaiveAbstractionLib]
mult_pos_up [in Scat.NaiveAbstractionLib]
mult_pos_low [in Scat.NaiveAbstractionLib]
mult_right_cte [in Scat.NaiveAbstractionLib]

N

normalize [in Scat.Concrete]
normalize_rec [in Scat.Concrete]
not_EQ [in Scat.NaiveGuardAbstractions]
not_LE [in Scat.NaiveGuardAbstractions]

O

oadd [in Scat.Assertions]
oeval [in Scat.Conditions]
ok [in Scat.MiscUtils]
orsubst [in Scat.Renaming]
oteval [in Scat.Conditions]
otrsubst [in Scat.Renaming]

P

postfinder_Kwlp [in Scat.KernelProof]
postfinder_increases_bound [in Scat.KernelProof]
postfinder_renforce_vc [in Scat.KernelProof]
prog_eq [in Scat.Concrete]

R

rbounds [in Scat.Renaming]
rempty [in Scat.Renaming]
rename [in Scat.Renaming]
require [in Scat.Atoms]
rewriting1 [in Scat.Examples]
rfind [in Scat.Renaming]
rlift [in Scat.Renaming]
rsubst [in Scat.Renaming]

S

safe_branch [in Scat.Assertions]
seq [in Scat.Certificate]
seqlabel [in Scat.Certificate]
seq_outskip [in Scat.Concrete]
state [in Scat.Conditions]
stdloop [in Scat.Certificate]
swap [in Scat.Renaming]

T

tauto [in Scat.Conditions]
tbind [in Scat.NaiveTermAbstractions]
tbound [in Scat.Renaming]
tbounds [in Scat.Renaming]
tbranch2 [in Scat.NaiveTermAbstractions]
term_eq [in Scat.Conditions]
teval [in Scat.Conditions]
trename [in Scat.Renaming]
tret [in Scat.NaiveTermAbstractions]
trsubst [in Scat.Renaming]
try [in Scat.MiscUtils]
tsubst [in Scat.Conditions]

U

unrollfwd [in Scat.LoopsUnrolling]
unroll_all [in Scat.LoopsUnrolling]

V

Value.value [in Scat.Conditions]
Value.vbin [in Scat.Conditions]
Value.vcte [in Scat.Conditions]
Value.Zof [in Scat.Conditions]
var_eq [in Scat.Conditions]
vcg [in Scat.Certificate]
vc_eval [in Scat.KernelVCG]

W

wlp [in Scat.Concrete]

Z

Zdiv_by_pos_cte [in Scat.NaiveAbstractionLib]
Zexists [in Scat.BoundedIteration]
Zforall [in Scat.BoundedIteration]

Axiom Index

C

ctefun [in Scat.Conditions]

V

ValueTypeAbstraction.value [in Scat.Conditions]
ValueTypeAbstraction.vbin [in Scat.Conditions]
ValueTypeAbstraction.vcte [in Scat.Conditions]
ValueTypeAbstraction.vcte_Zof [in Scat.Conditions]
ValueTypeAbstraction.Zof [in Scat.Conditions]
ValueTypeAbstraction.Zof_vbin [in Scat.Conditions]
ValueTypeAbstraction.Zof_vcte [in Scat.Conditions]
VCGparameters.absurd [in Scat.KernelVCG]
VCGparameters.bind [in Scat.KernelVCG]
VCGparameters.ceq [in Scat.KernelVCG]
VCGparameters.check_entails [in Scat.KernelVCG]
VCGparameters.hard_and [in Scat.KernelVCG]
VCGparameters.monad [in Scat.KernelVCG]
VCGparameters.rename [in Scat.KernelVCG]
VCGparameters.ret [in Scat.KernelVCG]
VCGparameters.soft_or [in Scat.KernelVCG]
VCGparameters.tauto [in Scat.KernelVCG]
VCGparameters.trename [in Scat.KernelVCG]

Module Index

C

ConcreteCondWrapper [in Scat.KernelVCG]

G

GenericVCG [in Scat.KernelVCG]

K

KVCG [in Scat.KernelVCG]

V

Value [in Scat.Conditions]
ValueTypeAbstraction [in Scat.Conditions]
VCGparameters [in Scat.KernelVCG]

Variable Index

A

AbstractionExample.annotated [in Scat.BasicExamples]
AbstractionExample.source [in Scat.BasicExamples]
AbstractionExample.x [in Scat.BasicExamples]
AbstractionExample.y [in Scat.BasicExamples]

G

GenericVCG.VCGCode.void [in Scat.KernelVCG]
GenericVCG.VCGCode.xret [in Scat.KernelVCG]
GuassignExample.essai [in Scat.BasicExamples]
GuassignExample.list [in Scat.BasicExamples]
GuassignExample.t [in Scat.BasicExamples]
GuassignExample.u [in Scat.BasicExamples]
GuassignExample.v [in Scat.BasicExamples]
GuassignExample.x [in Scat.BasicExamples]
GuassignExample.y [in Scat.BasicExamples]
GuassignExample.z [in Scat.BasicExamples]

J

JoinseqUnrollInvariant.annotated [in Scat.Examples]
JoinseqUnrollInvariant.approx_convexhull [in Scat.Examples]
JoinseqUnrollInvariant.i [in Scat.Examples]
JoinseqUnrollInvariant.label [in Scat.Examples]
JoinseqUnrollInvariant.r [in Scat.Examples]
JoinseqUnrollInvariant.source [in Scat.Examples]
JoinseqUnrollInvariant.x [in Scat.Examples]
JoinseqUnrollInvariant.y [in Scat.Examples]

K

Kiter_proofs.k_monotonic [in Scat.Kernel]
Kiter_proofs.k [in Scat.Kernel]

L

LetTerm.annotated [in Scat.BasicExamples]
LetTerm.annotatedy [in Scat.BasicExamples]
LetTerm.source [in Scat.BasicExamples]
LetTerm.x [in Scat.BasicExamples]
LetTerm.y [in Scat.BasicExamples]
LetTerm.z [in Scat.BasicExamples]
Le_iter_proofs.next_kn [in Scat.KernelProof]
Le_iter_proofs.body_kb [in Scat.KernelProof]
Le_iter_proofs.kn_monotonic [in Scat.KernelProof]
Le_iter_proofs.kb_monotonic [in Scat.KernelProof]
Le_iter_proofs.next_reswf [in Scat.KernelProof]
Le_iter_proofs.body_reswf [in Scat.KernelProof]
Le_iter_proofs.bound1_bound2 [in Scat.KernelProof]
Le_iter_proofs.next_increases_bound [in Scat.KernelProof]
Le_iter_proofs.body_increases_bound [in Scat.KernelProof]
Le_iter_proofs.next_renforce_vc [in Scat.KernelProof]
Le_iter_proofs.body_renforce_vc [in Scat.KernelProof]
Le_iter_proofs.bound2 [in Scat.KernelProof]
Le_iter_proofs.bound1 [in Scat.KernelProof]
Le_iter_proofs.kn [in Scat.KernelProof]
Le_iter_proofs.kb [in Scat.KernelProof]
Le_iter_proofs.next [in Scat.KernelProof]
Le_iter_proofs.body [in Scat.KernelProof]
LoopExample.annotated1 [in Scat.BasicExamples]
LoopExample.annotated2 [in Scat.BasicExamples]
LoopExample.i [in Scat.BasicExamples]
LoopExample.label [in Scat.BasicExamples]
LoopExample.r [in Scat.BasicExamples]
LoopExample.source [in Scat.BasicExamples]
LoopExample.x [in Scat.BasicExamples]
LoopExample.y [in Scat.BasicExamples]

M

MauborgneRival_Barycentre.annotated [in Scat.Examples]
MauborgneRival_Barycentre.label [in Scat.Examples]
MauborgneRival_Barycentre.source [in Scat.Examples]
MauborgneRival_Barycentre.r [in Scat.Examples]
MauborgneRival_Barycentre.y [in Scat.Examples]
MauborgneRival_Barycentre.x [in Scat.Examples]
MauborgneRival_LinearInterpolation.annotated [in Scat.Examples]
MauborgneRival_LinearInterpolation.label [in Scat.Examples]
MauborgneRival_LinearInterpolation.source [in Scat.Examples]
MauborgneRival_LinearInterpolation.i [in Scat.Examples]
MauborgneRival_LinearInterpolation.y [in Scat.Examples]
MauborgneRival_LinearInterpolation.x [in Scat.Examples]
MauborgneRival_LinearInterpolation.ty [in Scat.Examples]
MauborgneRival_LinearInterpolation.tx [in Scat.Examples]
MauborgneRival_LinearInterpolation.tc [in Scat.Examples]
MauborgneRival_LinearInterpolation.ty_3 [in Scat.Examples]
MauborgneRival_LinearInterpolation.ty_2 [in Scat.Examples]
MauborgneRival_LinearInterpolation.ty_1 [in Scat.Examples]
MauborgneRival_LinearInterpolation.ty_0 [in Scat.Examples]
MauborgneRival_LinearInterpolation.tx_3 [in Scat.Examples]
MauborgneRival_LinearInterpolation.tx_2 [in Scat.Examples]
MauborgneRival_LinearInterpolation.tx_1 [in Scat.Examples]
MauborgneRival_LinearInterpolation.tc_3 [in Scat.Examples]
MauborgneRival_LinearInterpolation.tc_2 [in Scat.Examples]
MauborgneRival_LinearInterpolation.tc_1 [in Scat.Examples]
MauborgneRival_LinearInterpolation.tc_0 [in Scat.Examples]
MinetBarycentreExample.annotated [in Scat.Examples]
MinetBarycentreExample.r [in Scat.Examples]
MinetBarycentreExample.source [in Scat.Examples]
MinetBarycentreExample.x [in Scat.Examples]
MinetBarycentreExample.y [in Scat.Examples]
MinetBarycentreExample.z [in Scat.Examples]
MinetBarycentreExample2.annotated [in Scat.Examples]
MinetBarycentreExample2.label [in Scat.Examples]
MinetBarycentreExample2.r [in Scat.Examples]
MinetBarycentreExample2.source [in Scat.Examples]
MinetBarycentreExample2.x [in Scat.Examples]
MinetBarycentreExample2.y [in Scat.Examples]
MinetBarycentreExample2.z [in Scat.Examples]
Misc1.annotated [in Scat.BasicExamples]
Misc1.r [in Scat.BasicExamples]
Misc1.x [in Scat.BasicExamples]
Misc1.y [in Scat.BasicExamples]

R

RunningExample.annotated [in Scat.Examples]
RunningExample.convexhull [in Scat.Examples]
RunningExample.label [in Scat.Examples]
RunningExample.r [in Scat.Examples]
RunningExample.source [in Scat.Examples]
RunningExample.x [in Scat.Examples]
RunningExample.y [in Scat.Examples]

U

UnroolBasicExample.annotated [in Scat.BasicExamples]
UnroolBasicExample.i [in Scat.BasicExamples]
UnroolBasicExample.r [in Scat.BasicExamples]
UnroolBasicExample.source [in Scat.BasicExamples]
UnroolBasicExample.x [in Scat.BasicExamples]
UnroolBasicExample.y [in Scat.BasicExamples]

Library Index

A

Assertions
Atoms

B

BasicExamples
BoundedIteration

C

Certificate
Concrete
Conditions

E

G

K

Kernel
KernelProof
KernelVCG

L

M

N

NaiveAbstractionLib
NaiveGuardAbstractions
NaiveTermAbstractions

R

Global Index

Q

Y

_

(681 entries)

Projection Index

B

D

E

F

I

J

K

M

N

O

P

Q

S

U

W

X

Y

Z

_

other

(32 entries)

Record Index

B

D

E

F

I

J

K

L

M

N

O

P

Q

S

U

W

X

Y

Z

_

other

(12 entries)

Lemma Index

H

J

M

Q

X

Y

_

other

(198 entries)

Section Index

B

C

D

E

F

H

I

N

O

P

Q

S

T

V

W

X

Y

Z

_

other

(15 entries)

Constructor Index

F

H

Q

W

Y

Z

_

other

(63 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

N

O

P

Q

R

S

T

U

W

X

Y

Z

_

(28 entries)

Inductive Index

D

E

F

G

H

I

J

L

M

N

O

Q

R

U

W

X

Y

Z

_

other

(13 entries)

Definition Index

Q

X

Y

_

other

(166 entries)

Axiom Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

W

X

Y

Z

_

other

(19 entries)

Module Index

A

B

D

E

F

H

I

J

L

M

N

O

P

Q

R

S

T

U

W

X

Y

Z

_

other

(6 entries)

Variable Index

B

C

D

E

F

H

I

N

O

P

Q

S

T

V

W

X

Y

Z

_

other

(111 entries)

Library Index

D

F

H

I

J

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(18 entries)

This page has been generated by coqdoc