Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1667 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (111 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (952 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (18 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (151 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (226 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (52 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (10 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (136 entries)

Global Index

A

aequiv [definition, in Equiv]
aequiv_example [lemma, in Equiv]
Aexp [definition, in Hoare]
Aexp_of_aexp [definition, in Hoare]
Aexp_of_nat [definition, in Hoare]
always_loop_hoare [lemma, in Hoare]
ap [definition, in Hoare]
ap2 [definition, in Hoare]
assert [abbreviation, in Hoare]
Assertion [definition, in Hoare]
assert_of_Prop [definition, in Hoare]
assert_implies [definition, in Hoare]
assign_aequiv [lemma, in Equiv]
assn_sub_ex2' [definition, in Hoare]
assn_sub_ex1' [definition, in Hoare]
assn_sub_example2'' [definition, in Hoare]
assn_sub_example2' [definition, in Hoare]
assn_sub_example2 [definition, in Hoare]
assn_sub_example [definition, in Hoare]
assn_sub [definition, in Hoare]
astep [inductive, in Smallstep]
AS_Mult [constructor, in Smallstep]
AS_Mult2 [constructor, in Smallstep]
AS_Mult1 [constructor, in Smallstep]
AS_Minus [constructor, in Smallstep]
AS_Minus2 [constructor, in Smallstep]
AS_Minus1 [constructor, in Smallstep]
AS_Plus [constructor, in Smallstep]
AS_Plus2 [constructor, in Smallstep]
AS_Plus1 [constructor, in Smallstep]
AS_Id [constructor, in Smallstep]
atrans_sound [definition, in Equiv]
atrans:91 [binder, in Equiv]
aval [inductive, in Smallstep]
av_num [constructor, in Smallstep]
a':64 [binder, in Equiv]
a1':193 [binder, in Smallstep]
a1':201 [binder, in Smallstep]
a1':209 [binder, in Smallstep]
a1':220 [binder, in Smallstep]
a1':228 [binder, in Smallstep]
a1':248 [binder, in Smallstep]
a1':280 [binder, in Smallstep]
a1:1 [binder, in Equiv]
a1:113 [binder, in Equiv]
a1:125 [binder, in Hoare]
a1:180 [binder, in Hoare]
a1:192 [binder, in Smallstep]
a1:200 [binder, in Smallstep]
a1:208 [binder, in Smallstep]
a1:219 [binder, in Smallstep]
a1:227 [binder, in Smallstep]
a1:247 [binder, in Smallstep]
a1:279 [binder, in Smallstep]
a1:45 [binder, in Equiv]
a1:47 [binder, in Equiv]
a2':197 [binder, in Smallstep]
a2':205 [binder, in Smallstep]
a2':213 [binder, in Smallstep]
a2':224 [binder, in Smallstep]
a2':232 [binder, in Smallstep]
a2:114 [binder, in Equiv]
a2:194 [binder, in Smallstep]
a2:196 [binder, in Smallstep]
a2:2 [binder, in Equiv]
a2:202 [binder, in Smallstep]
a2:204 [binder, in Smallstep]
a2:210 [binder, in Smallstep]
a2:212 [binder, in Smallstep]
a2:221 [binder, in Smallstep]
a2:223 [binder, in Smallstep]
a2:229 [binder, in Smallstep]
a2:231 [binder, in Smallstep]
a2:46 [binder, in Equiv]
a2:48 [binder, in Equiv]
a3:49 [binder, in Equiv]
a:10 [binder, in Hoare]
a:104 [binder, in Hoare]
a:108 [binder, in Equiv]
a:11 [binder, in HoareAsLogic]
a:232 [binder, in Hoare]
a:43 [binder, in Equiv]
a:44 [binder, in Equiv]
a:55 [binder, in Hoare]
a:57 [binder, in Hoare2]
a:59 [binder, in Hoare2]
a:60 [binder, in Hoare]
a:61 [binder, in Hoare2]
a:62 [binder, in Hoare]
a:63 [binder, in Equiv]
a:64 [binder, in Hoare2]
a:66 [binder, in Hoare]
a:7 [binder, in Hoare2]
a:92 [binder, in Equiv]
a:97 [binder, in Equiv]


B

bassn [definition, in Hoare]
bequiv [definition, in Equiv]
bequiv_example [lemma, in Equiv]
bexp_eval_false [lemma, in Hoare]
Bib [library]
bstep [inductive, in Smallstep]
BS_AndTrueFalse [constructor, in Smallstep]
BS_AndTrueTrue [constructor, in Smallstep]
BS_AndFalse [constructor, in Smallstep]
BS_AndTrueStep [constructor, in Smallstep]
BS_AndStep [constructor, in Smallstep]
BS_NotFalse [constructor, in Smallstep]
BS_NotTrue [constructor, in Smallstep]
BS_NotStep [constructor, in Smallstep]
BS_LtEq [constructor, in Smallstep]
BS_LtEq2 [constructor, in Smallstep]
BS_LtEq1 [constructor, in Smallstep]
BS_Eq [constructor, in Smallstep]
BS_Eq2 [constructor, in Smallstep]
BS_Eq1 [constructor, in Smallstep]
btrans_sound [definition, in Equiv]
btrans:93 [binder, in Equiv]
b':66 [binder, in Equiv]
b':70 [binder, in Equiv]
b':76 [binder, in Equiv]
b':86 [binder, in Equiv]
b1':236 [binder, in Smallstep]
b1':238 [binder, in Smallstep]
b1':261 [binder, in Smallstep]
b1':293 [binder, in Smallstep]
b1:235 [binder, in Smallstep]
b1:237 [binder, in Smallstep]
b1:260 [binder, in Smallstep]
b1:271 [binder, in Smallstep]
b1:292 [binder, in Smallstep]
b1:303 [binder, in Smallstep]
b1:4 [binder, in Equiv]
b1:51 [binder, in Equiv]
b1:53 [binder, in Equiv]
b2':241 [binder, in Smallstep]
b2:239 [binder, in Smallstep]
b2:240 [binder, in Smallstep]
b2:242 [binder, in Smallstep]
b2:5 [binder, in Equiv]
b2:52 [binder, in Equiv]
b2:54 [binder, in Equiv]
b3:55 [binder, in Equiv]
b:100 [binder, in Equiv]
b:106 [binder, in Hoare]
b:108 [binder, in Hoare]
b:112 [binder, in Hoare]
b:116 [binder, in Hoare]
b:135 [binder, in Hoare]
b:140 [binder, in Hoare]
b:143 [binder, in Hoare]
b:149 [binder, in Hoare]
b:15 [binder, in Hoare2]
b:19 [binder, in Equiv]
b:19 [binder, in HoareAsLogic]
b:193 [binder, in Hoare]
b:198 [binder, in Hoare]
b:201 [binder, in Hoare]
b:207 [binder, in Hoare]
b:210 [binder, in Hoare]
b:213 [binder, in Hoare]
b:215 [binder, in Hoare]
b:217 [binder, in Hoare]
b:22 [binder, in Equiv]
b:225 [binder, in Hoare]
b:228 [binder, in Hoare]
b:25 [binder, in Equiv]
b:25 [binder, in HoareAsLogic]
b:251 [binder, in Hoare]
b:255 [binder, in Hoare]
b:28 [binder, in Equiv]
b:30 [binder, in Equiv]
b:34 [binder, in Equiv]
b:36 [binder, in Equiv]
b:50 [binder, in Equiv]
b:58 [binder, in Hoare2]
b:60 [binder, in Hoare2]
b:62 [binder, in Hoare2]
b:65 [binder, in Equiv]
b:65 [binder, in Hoare2]
b:68 [binder, in HoareAsLogic]
b:69 [binder, in Equiv]
b:75 [binder, in Equiv]
b:85 [binder, in Equiv]
b:9 [binder, in Hoare2]
b:94 [binder, in Equiv]


C

C [constructor, in Smallstep]
CAsgn_congruence [lemma, in Equiv]
cequiv [definition, in Equiv]
CIf_congruence [lemma, in Equiv]
CImp [module, in Smallstep]
CImp.CAsgn [constructor, in Smallstep]
CImp.CIf [constructor, in Smallstep]
CImp.cmultistep [definition, in Smallstep]
CImp.com [inductive, in Smallstep]
CImp.CPar [constructor, in Smallstep]
CImp.CSeq [constructor, in Smallstep]
CImp.CSkip [constructor, in Smallstep]
CImp.cstep [inductive, in Smallstep]
CImp.CS_ParDone [constructor, in Smallstep]
CImp.CS_Par2 [constructor, in Smallstep]
CImp.CS_Par1 [constructor, in Smallstep]
CImp.CS_While [constructor, in Smallstep]
CImp.CS_IfFalse [constructor, in Smallstep]
CImp.CS_IfTrue [constructor, in Smallstep]
CImp.CS_IfStep [constructor, in Smallstep]
CImp.CS_SeqFinish [constructor, in Smallstep]
CImp.CS_SeqStep [constructor, in Smallstep]
CImp.CS_Asgn [constructor, in Smallstep]
CImp.CS_AsgnStep [constructor, in Smallstep]
CImp.CWhile [constructor, in Smallstep]
CImp.par_body_n__Sn [lemma, in Smallstep]
CImp.par_loop_example_2 [definition, in Smallstep]
CImp.par_loop_example_0 [definition, in Smallstep]
CImp.par_loop [definition, in Smallstep]
com:_ ; _ [notation, in Smallstep]
com:_ := _ [notation, in Smallstep]
com:_ || _ [notation, in Smallstep]
com:if _ then _ else _ end [notation, in Smallstep]
com:skip [notation, in Smallstep]
com:while _ do _ end [notation, in Smallstep]
_ / _ -->* _ / _ [notation, in Smallstep]
_ / _ --> _ / _ [notation, in Smallstep]
Combined [module, in Smallstep]
Combined.C [constructor, in Smallstep]
Combined.combined_strong_progress [lemma, in Smallstep]
Combined.combined_step_deterministic [lemma, in Smallstep]
Combined.fls [constructor, in Smallstep]
Combined.P [constructor, in Smallstep]
Combined.step [inductive, in Smallstep]
Combined.ST_If [constructor, in Smallstep]
Combined.ST_IfFalse [constructor, in Smallstep]
Combined.ST_IfTrue [constructor, in Smallstep]
Combined.ST_Plus2 [constructor, in Smallstep]
Combined.ST_Plus1 [constructor, in Smallstep]
Combined.ST_PlusConstConst [constructor, in Smallstep]
Combined.test [constructor, in Smallstep]
Combined.tm [inductive, in Smallstep]
Combined.tru [constructor, in Smallstep]
Combined.value [inductive, in Smallstep]
Combined.v_fls [constructor, in Smallstep]
Combined.v_tru [constructor, in Smallstep]
Combined.v_const [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
compiler_is_correct [lemma, in Smallstep]
compiler_is_correct_statement [definition, in Smallstep]
congruence_example [definition, in Equiv]
CSeq_congruence [lemma, in Equiv]
cstep [inductive, in Smallstep]
CS_While [constructor, in Smallstep]
CS_IfFalse [constructor, in Smallstep]
CS_IfTrue [constructor, in Smallstep]
CS_IfStep [constructor, in Smallstep]
CS_SeqFinish [constructor, in Smallstep]
CS_SeqStep [constructor, in Smallstep]
CS_Asgn [constructor, in Smallstep]
CS_AsgnStep [constructor, in Smallstep]
ctrans_sound [definition, in Equiv]
ctrans:95 [binder, in Equiv]
CWhile_congruence [lemma, in Equiv]
c':16 [binder, in Types]
c':68 [binder, in Equiv]
c':72 [binder, in Equiv]
c':78 [binder, in Equiv]
c1':254 [binder, in Smallstep]
c1':286 [binder, in Smallstep]
c1':307 [binder, in Smallstep]
c1':82 [binder, in Equiv]
c1':88 [binder, in Equiv]
c1:11 [binder, in Equiv]
c1:113 [binder, in Hoare]
c1:128 [binder, in Hoare]
c1:136 [binder, in Hoare]
c1:141 [binder, in Hoare]
c1:17 [binder, in Equiv]
c1:183 [binder, in Hoare]
c1:188 [binder, in Hoare]
c1:194 [binder, in Hoare]
c1:199 [binder, in Hoare]
c1:20 [binder, in Equiv]
c1:20 [binder, in HoareAsLogic]
c1:23 [binder, in Equiv]
c1:246 [binder, in Hoare]
c1:252 [binder, in Hoare]
c1:253 [binder, in Smallstep]
c1:26 [binder, in Equiv]
c1:262 [binder, in Smallstep]
c1:265 [binder, in Smallstep]
c1:268 [binder, in Smallstep]
c1:272 [binder, in Smallstep]
c1:285 [binder, in Smallstep]
c1:294 [binder, in Smallstep]
c1:297 [binder, in Smallstep]
c1:300 [binder, in Smallstep]
c1:304 [binder, in Smallstep]
c1:306 [binder, in Smallstep]
c1:311 [binder, in Smallstep]
c1:38 [binder, in Equiv]
c1:52 [binder, in Hoare]
c1:57 [binder, in Equiv]
c1:59 [binder, in Equiv]
c1:66 [binder, in HoareAsLogic]
c1:7 [binder, in Equiv]
c1:81 [binder, in Equiv]
c1:87 [binder, in Equiv]
c2':313 [binder, in Smallstep]
c2':84 [binder, in Equiv]
c2':90 [binder, in Equiv]
c2:114 [binder, in Hoare]
c2:12 [binder, in Equiv]
c2:129 [binder, in Hoare]
c2:137 [binder, in Hoare]
c2:142 [binder, in Hoare]
c2:18 [binder, in Equiv]
c2:184 [binder, in Hoare]
c2:189 [binder, in Hoare]
c2:195 [binder, in Hoare]
c2:200 [binder, in Hoare]
c2:21 [binder, in Equiv]
c2:21 [binder, in HoareAsLogic]
c2:24 [binder, in Equiv]
c2:247 [binder, in Hoare]
c2:253 [binder, in Hoare]
c2:256 [binder, in Smallstep]
c2:258 [binder, in Smallstep]
c2:263 [binder, in Smallstep]
c2:266 [binder, in Smallstep]
c2:269 [binder, in Smallstep]
c2:27 [binder, in Equiv]
c2:288 [binder, in Smallstep]
c2:290 [binder, in Smallstep]
c2:295 [binder, in Smallstep]
c2:298 [binder, in Smallstep]
c2:301 [binder, in Smallstep]
c2:308 [binder, in Smallstep]
c2:312 [binder, in Smallstep]
c2:39 [binder, in Equiv]
c2:53 [binder, in Hoare]
c2:58 [binder, in Equiv]
c2:60 [binder, in Equiv]
c2:67 [binder, in HoareAsLogic]
c2:8 [binder, in Equiv]
c2:83 [binder, in Equiv]
c2:89 [binder, in Equiv]
c3:40 [binder, in Equiv]
c3:61 [binder, in Equiv]
c:103 [binder, in Hoare]
c:103 [binder, in Equiv]
c:117 [binder, in Hoare]
c:13 [binder, in HoareAsLogic]
c:145 [binder, in Hoare]
c:15 [binder, in Equiv]
c:15 [binder, in Types]
c:150 [binder, in Hoare]
c:155 [binder, in Hoare]
c:16 [binder, in Equiv]
c:162 [binder, in Hoare]
c:2 [binder, in HoareAsLogic]
c:203 [binder, in Hoare]
c:208 [binder, in Hoare]
c:211 [binder, in Hoare]
c:219 [binder, in Hoare]
c:236 [binder, in Hoare]
c:240 [binder, in Hoare]
c:256 [binder, in Hoare]
c:26 [binder, in HoareAsLogic]
c:29 [binder, in Equiv]
c:31 [binder, in Equiv]
c:33 [binder, in HoareAsLogic]
c:35 [binder, in Equiv]
c:36 [binder, in Hoare]
c:37 [binder, in Equiv]
c:39 [binder, in HoareAsLogic]
c:42 [binder, in Hoare]
c:44 [binder, in HoareAsLogic]
c:46 [binder, in Hoare]
c:48 [binder, in HoareAsLogic]
c:50 [binder, in HoareAsLogic]
c:53 [binder, in HoareAsLogic]
c:55 [binder, in HoareAsLogic]
c:56 [binder, in Equiv]
c:59 [binder, in HoareAsLogic]
c:61 [binder, in HoareAsLogic]
c:63 [binder, in Hoare2]
c:66 [binder, in Hoare2]
c:67 [binder, in Equiv]
c:69 [binder, in HoareAsLogic]
c:71 [binder, in Equiv]
c:72 [binder, in HoareAsLogic]
c:74 [binder, in Hoare]
c:77 [binder, in Equiv]
c:78 [binder, in Hoare]
c:83 [binder, in Hoare]
c:87 [binder, in Hoare]
c:91 [binder, in Hoare]
c:95 [binder, in Hoare]
c:96 [binder, in Equiv]
c:99 [binder, in Hoare]


D

DCAsgn [constructor, in Hoare2]
DCIf [constructor, in Hoare2]
dcom [inductive, in Hoare2]
DCPost [constructor, in Hoare2]
DCPre [constructor, in Hoare2]
DCSeq [constructor, in Hoare2]
DCSkip [constructor, in Hoare2]
DCWhile [constructor, in Hoare2]
Decorated [constructor, in Hoare2]
decorated [inductive, in Hoare2]
dec_while_correct [lemma, in Hoare2]
dec_while_triple_correct [definition, in Hoare2]
dec_while [definition, in Hoare2]
dec0 [definition, in Hoare2]
dec1 [definition, in Hoare2]
dec:28 [binder, in Hoare2]
dec:30 [binder, in Hoare2]
dec:35 [binder, in Hoare2]
dec:37 [binder, in Hoare2]
dec:44 [binder, in Hoare2]
dec:46 [binder, in Hoare2]
derivable [inductive, in HoareAsLogic]
deterministic [definition, in Smallstep]
d1:11 [binder, in Hoare2]
d1:4 [binder, in Hoare2]
d2:13 [binder, in Hoare2]
d2:5 [binder, in Hoare2]
d:15 [binder, in HoareAsLogic]
d:17 [binder, in Hoare2]
d:20 [binder, in Hoare2]
d:21 [binder, in Hoare2]
d:25 [binder, in Hoare2]
d:32 [binder, in Hoare2]
d:39 [binder, in Hoare2]
d:42 [binder, in Hoare2]


E

Equiv [library]
eval [inductive, in Smallstep]
evalF [definition, in Smallstep]
eval__multistep [lemma, in Smallstep]
ExamplePrettyAssertions [module, in Hoare]
ExamplePrettyAssertions.assn1 [definition, in Hoare]
ExamplePrettyAssertions.assn2 [definition, in Hoare]
ExamplePrettyAssertions.assn3 [definition, in Hoare]
ExamplePrettyAssertions.assn4 [definition, in Hoare]
ExamplePrettyAssertions.ex1 [definition, in Hoare]
ExamplePrettyAssertions.ex2 [definition, in Hoare]
ExamplePrettyAssertions.ex3 [definition, in Hoare]
ExAssertions [module, in Hoare]
ExAssertions.assn1 [definition, in Hoare]
ExAssertions.assn2 [definition, in Hoare]
ExAssertions.assn3 [definition, in Hoare]
ExAssertions.assn4 [definition, in Hoare]
extract [definition, in Hoare2]
extract_while_ex [definition, in Hoare2]
extract_dec [definition, in Hoare2]
E_Plus [constructor, in Smallstep]
E_Const [constructor, in Smallstep]
e':343 [binder, in Smallstep]
e':344 [binder, in Smallstep]
e:40 [binder, in StlcProp]


F

FILL_IN_HERE [definition, in Smallstep]
FILL_IN_HERE [definition, in Hoare2]
fold_com_ex1 [definition, in Equiv]
fold_constants_com [definition, in Equiv]
fold_bexp_ex2 [definition, in Equiv]
fold_bexp_ex1 [definition, in Equiv]
fold_constants_bexp [definition, in Equiv]
fold_aexp_ex2 [definition, in Equiv]
fold_aexp_ex1 [definition, in Equiv]
fold_constants_aexp [definition, in Equiv]
f:27 [binder, in Hoare]
f:31 [binder, in Hoare]


G

Gamma':14 [binder, in StlcProp]
Gamma':72 [binder, in StlcProp]
Gamma':92 [binder, in StlcProp]
Gamma:13 [binder, in StlcProp]
Gamma:17 [binder, in StlcProp]
Gamma:20 [binder, in StlcProp]
Gamma:26 [binder, in StlcProp]
Gamma:39 [binder, in StlcProp]
Gamma:45 [binder, in Stlc]
Gamma:48 [binder, in Stlc]
Gamma:55 [binder, in Stlc]
Gamma:58 [binder, in Stlc]
Gamma:59 [binder, in Stlc]
Gamma:64 [binder, in Stlc]
Gamma:67 [binder, in StlcProp]
Gamma:71 [binder, in StlcProp]
Gamma:91 [binder, in StlcProp]


H

Himp [module, in Hoare]
Himp.CAsgn [constructor, in Hoare]
Himp.ceval [inductive, in Hoare]
Himp.CHavoc [constructor, in Hoare]
Himp.CIf [constructor, in Hoare]
Himp.com [inductive, in Hoare]
Himp.CSeq [constructor, in Hoare]
Himp.CSkip [constructor, in Hoare]
Himp.CWhile [constructor, in Hoare]
Himp.E_Havoc [constructor, in Hoare]
Himp.E_WhileTrue [constructor, in Hoare]
Himp.E_WhileFalse [constructor, in Hoare]
Himp.E_IfFalse [constructor, in Hoare]
Himp.E_IfTrue [constructor, in Hoare]
Himp.E_Seq [constructor, in Hoare]
Himp.E_Asgn [constructor, in Hoare]
Himp.E_Skip [constructor, in Hoare]
Himp.havoc_post [lemma, in Hoare]
Himp.havoc_pre [definition, in Hoare]
Himp.hoare_havoc [lemma, in Hoare]
Himp.hoare_consequence_pre [lemma, in Hoare]
Himp.hoare_triple [definition, in Hoare]
com:_ ; _ [notation, in Hoare]
com:_ := _ [notation, in Hoare]
com:havoc _ [notation, in Hoare]
com:if _ then _ else _ end [notation, in Hoare]
com:skip [notation, in Hoare]
com:while _ do _ end [notation, in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [notation, in Hoare]
_ =[ _ ]=> _ [notation, in Hoare]
Hoare [library]
HoareAsLogic [library]
HoareAssertAssume [module, in Hoare]
HoareAssertAssume.assert_assume_example [definition, in Hoare]
HoareAssertAssume.assert_implies_assume [lemma, in Hoare]
HoareAssertAssume.assert_assume_differ [lemma, in Hoare]
HoareAssertAssume.CAsgn [constructor, in Hoare]
HoareAssertAssume.CAssert [constructor, in Hoare]
HoareAssertAssume.CAssume [constructor, in Hoare]
HoareAssertAssume.ceval [inductive, in Hoare]
HoareAssertAssume.CIf [constructor, in Hoare]
HoareAssertAssume.com [inductive, in Hoare]
HoareAssertAssume.CSeq [constructor, in Hoare]
HoareAssertAssume.CSkip [constructor, in Hoare]
HoareAssertAssume.CWhile [constructor, in Hoare]
HoareAssertAssume.E_Assume [constructor, in Hoare]
HoareAssertAssume.E_AssertFalse [constructor, in Hoare]
HoareAssertAssume.E_AssertTrue [constructor, in Hoare]
HoareAssertAssume.E_WhileTrueError [constructor, in Hoare]
HoareAssertAssume.E_WhileTrueNormal [constructor, in Hoare]
HoareAssertAssume.E_WhileFalse [constructor, in Hoare]
HoareAssertAssume.E_IfFalse [constructor, in Hoare]
HoareAssertAssume.E_IfTrue [constructor, in Hoare]
HoareAssertAssume.E_SeqError [constructor, in Hoare]
HoareAssertAssume.E_SeqNormal [constructor, in Hoare]
HoareAssertAssume.E_Asgn [constructor, in Hoare]
HoareAssertAssume.E_Skip [constructor, in Hoare]
HoareAssertAssume.hoare_while [lemma, in Hoare]
HoareAssertAssume.hoare_if [lemma, in Hoare]
HoareAssertAssume.hoare_skip [lemma, in Hoare]
HoareAssertAssume.hoare_seq [lemma, in Hoare]
HoareAssertAssume.hoare_consequence_post [lemma, in Hoare]
HoareAssertAssume.hoare_consequence_pre [lemma, in Hoare]
HoareAssertAssume.hoare_asgn [lemma, in Hoare]
HoareAssertAssume.hoare_triple [definition, in Hoare]
HoareAssertAssume.RError [constructor, in Hoare]
HoareAssertAssume.result [inductive, in Hoare]
HoareAssertAssume.RNormal [constructor, in Hoare]
com:_ ; _ [notation, in Hoare]
com:_ := _ [notation, in Hoare]
com:assert _ [notation, in Hoare]
com:assume _ [notation, in Hoare]
com:if _ then _ else _ end [notation, in Hoare]
com:skip [notation, in Hoare]
com:while _ do _ end [notation, in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [notation, in Hoare]
_ =[ _ ]=> _ [notation, in Hoare]
hoare_while [lemma, in Hoare]
hoare_if [lemma, in Hoare]
hoare_asgn_example4 [definition, in Hoare]
hoare_asgn_example3 [definition, in Hoare]
hoare_asgn_example1''' [definition, in Hoare]
hoare_asgn_example1'' [definition, in Hoare]
hoare_asgn_example1' [definition, in Hoare]
hoare_consequence_post' [lemma, in Hoare]
hoare_consequence_pre'''' [lemma, in Hoare]
hoare_consequence_pre''' [lemma, in Hoare]
hoare_consequence_pre'' [lemma, in Hoare]
hoare_consequence_pre' [lemma, in Hoare]
hoare_consequence [lemma, in Hoare]
hoare_asgn_example1 [definition, in Hoare]
hoare_consequence_post [lemma, in Hoare]
hoare_consequence_pre [lemma, in Hoare]
hoare_asgn_fwd_exists [lemma, in Hoare]
hoare_asgn_fwd [lemma, in Hoare]
hoare_asgn [lemma, in Hoare]
hoare_seq [lemma, in Hoare]
hoare_skip [lemma, in Hoare]
hoare_pre_false [lemma, in Hoare]
hoare_post_true [lemma, in Hoare]
hoare_triple [definition, in Hoare]
hoare_complete [lemma, in HoareAsLogic]
hoare_sound [lemma, in HoareAsLogic]
Hoare2 [library]
H_Consequence_post [lemma, in HoareAsLogic]
H_Consequence_pre [lemma, in HoareAsLogic]
H_Consequence [constructor, in HoareAsLogic]
H_While [constructor, in HoareAsLogic]
H_If [constructor, in HoareAsLogic]
H_Seq [constructor, in HoareAsLogic]
H_Asgn [constructor, in HoareAsLogic]
H_Skip [constructor, in HoareAsLogic]


I

identity_assignment [lemma, in Equiv]
if_minus_plus [lemma, in Hoare]
if_example''' [definition, in Hoare]
if_example'' [definition, in Hoare]
if_example [definition, in Hoare]
if_false [lemma, in Equiv]
if_true [lemma, in Equiv]
if_true_simple [lemma, in Equiv]
if_minus_plus_correct [lemma, in Hoare2]
if_minus_plus_dec [definition, in Hoare2]
inequiv_exercise [lemma, in Equiv]
i:191 [binder, in Smallstep]
i:246 [binder, in Smallstep]
i:250 [binder, in Smallstep]
i:278 [binder, in Smallstep]
i:282 [binder, in Smallstep]
i:327 [binder, in Smallstep]


L

loop_unrolling [lemma, in Equiv]


M

minimum_correct [lemma, in Hoare2]
minimum_dec [definition, in Hoare2]
mkAexp [abbreviation, in Hoare]
multi [inductive, in Smallstep]
multistep__eval [lemma, in Smallstep]
multistep_congr_2 [lemma, in Smallstep]
multistep_congr_1 [lemma, in Smallstep]
multi_trans [lemma, in Smallstep]
multi_R [lemma, in Smallstep]
multi_step [constructor, in Smallstep]
multi_refl [constructor, in Smallstep]
m:331 [binder, in Smallstep]
m:335 [binder, in Smallstep]
m:339 [binder, in Smallstep]
m:47 [binder, in Hoare2]
m:49 [binder, in Hoare2]
m:51 [binder, in Hoare2]
m:53 [binder, in Hoare2]
m:55 [binder, in Hoare2]
m:56 [binder, in Hoare2]
m:61 [binder, in Hoare]
m:70 [binder, in Hoare]


N

nf_same_as_value [lemma, in Smallstep]
nf_is_value [lemma, in Smallstep]
normalize_ex [lemma, in Smallstep]
normalizing [definition, in Smallstep]
normal_form_of [definition, in Smallstep]
normal_form [definition, in Smallstep]
n:105 [binder, in Hoare]
n:126 [binder, in Hoare]
n:151 [binder, in Smallstep]
n:153 [binder, in Hoare]
n:154 [binder, in Smallstep]
n:157 [binder, in Smallstep]
n:162 [binder, in Smallstep]
n:171 [binder, in Hoare]
n:181 [binder, in Hoare]
n:187 [binder, in Smallstep]
n:251 [binder, in Smallstep]
n:283 [binder, in Smallstep]
n:31 [binder, in Smallstep]
n:318 [binder, in Smallstep]
n:324 [binder, in Smallstep]
n:330 [binder, in Smallstep]
n:334 [binder, in Smallstep]
n:338 [binder, in Smallstep]
n:48 [binder, in Hoare2]
n:50 [binder, in Hoare2]
n:55 [binder, in Smallstep]
n:71 [binder, in Smallstep]
n:74 [binder, in Smallstep]
n:8 [binder, in Smallstep]
n:86 [binder, in Smallstep]
n:9 [binder, in Hoare]


O

outer_triple_valid [definition, in Hoare2]


P

P [constructor, in Smallstep]
positive_difference_correct [lemma, in Hoare2]
positive_difference_dec [definition, in Hoare2]
post [definition, in Hoare2]
Postscript [library]
post_dec_while [definition, in Hoare2]
post_dec [definition, in Hoare2]
Preface [library]
pre_dec_while [definition, in Hoare2]
pre_dec [definition, in Hoare2]
prog [definition, in Smallstep]
provable_false_pre [lemma, in HoareAsLogic]
provable_true_post [lemma, in HoareAsLogic]
P':160 [binder, in Hoare]
P':234 [binder, in Hoare]
P':31 [binder, in HoareAsLogic]
P':38 [binder, in HoareAsLogic]
P':63 [binder, in HoareAsLogic]
P':72 [binder, in Hoare]
P':80 [binder, in Hoare]
P':85 [binder, in Hoare]
P':89 [binder, in Hoare]
P':93 [binder, in Hoare]
P':97 [binder, in Hoare]
P1:10 [binder, in Hoare2]
P2:12 [binder, in Hoare2]
P:1 [binder, in HoareAsLogic]
P:100 [binder, in Hoare]
P:110 [binder, in Hoare]
P:115 [binder, in Hoare]
P:12 [binder, in HoareAsLogic]
P:154 [binder, in Hoare]
P:159 [binder, in Hoare]
P:16 [binder, in Hoare2]
P:168 [binder, in Hoare]
P:17 [binder, in HoareAsLogic]
P:19 [binder, in Hoare2]
P:218 [binder, in Hoare]
P:224 [binder, in Hoare]
P:227 [binder, in Hoare]
P:233 [binder, in Hoare]
P:237 [binder, in Hoare]
P:24 [binder, in HoareAsLogic]
P:243 [binder, in Hoare]
P:248 [binder, in Hoare]
P:249 [binder, in Hoare]
P:254 [binder, in Hoare]
P:29 [binder, in HoareAsLogic]
p:325 [binder, in Smallstep]
p:328 [binder, in Smallstep]
p:332 [binder, in Smallstep]
p:336 [binder, in Smallstep]
p:340 [binder, in Smallstep]
P:35 [binder, in Hoare]
P:36 [binder, in HoareAsLogic]
P:38 [binder, in Hoare2]
P:40 [binder, in Hoare]
P:41 [binder, in HoareAsLogic]
P:43 [binder, in Hoare2]
P:44 [binder, in Hoare]
P:48 [binder, in Hoare]
P:49 [binder, in Hoare]
P:49 [binder, in HoareAsLogic]
P:5 [binder, in Hoare]
P:52 [binder, in HoareAsLogic]
p:52 [binder, in Hoare2]
p:54 [binder, in Hoare2]
P:56 [binder, in Hoare]
P:63 [binder, in Hoare]
P:64 [binder, in HoareAsLogic]
P:67 [binder, in Hoare]
P:71 [binder, in Hoare]
P:71 [binder, in HoareAsLogic]
P:75 [binder, in Hoare]
P:79 [binder, in Hoare]
P:8 [binder, in Hoare]
P:8 [binder, in HoareAsLogic]
P:84 [binder, in Hoare]
P:88 [binder, in Hoare]
P:92 [binder, in Hoare]
P:96 [binder, in Hoare]


Q

Q':102 [binder, in Hoare]
Q':239 [binder, in Hoare]
Q':32 [binder, in HoareAsLogic]
Q':43 [binder, in HoareAsLogic]
Q':77 [binder, in Hoare]
Q':82 [binder, in Hoare]
Q:101 [binder, in Hoare]
Q:111 [binder, in Hoare]
Q:118 [binder, in Hoare]
Q:14 [binder, in HoareAsLogic]
Q:14 [binder, in Hoare2]
Q:156 [binder, in Hoare]
Q:161 [binder, in Hoare]
Q:164 [binder, in Hoare]
Q:166 [binder, in Hoare]
Q:18 [binder, in HoareAsLogic]
Q:18 [binder, in Hoare2]
Q:22 [binder, in Hoare2]
Q:220 [binder, in Hoare]
Q:226 [binder, in Hoare]
Q:229 [binder, in Hoare]
Q:230 [binder, in Hoare]
Q:235 [binder, in Hoare]
Q:238 [binder, in Hoare]
Q:244 [binder, in Hoare]
Q:250 [binder, in Hoare]
Q:3 [binder, in HoareAsLogic]
Q:3 [binder, in Hoare2]
Q:30 [binder, in HoareAsLogic]
Q:37 [binder, in Hoare]
Q:37 [binder, in HoareAsLogic]
Q:41 [binder, in Hoare]
Q:42 [binder, in HoareAsLogic]
Q:45 [binder, in Hoare]
Q:50 [binder, in Hoare]
Q:51 [binder, in HoareAsLogic]
Q:54 [binder, in HoareAsLogic]
Q:56 [binder, in HoareAsLogic]
Q:58 [binder, in Hoare]
Q:6 [binder, in Hoare]
Q:60 [binder, in HoareAsLogic]
Q:62 [binder, in HoareAsLogic]
Q:65 [binder, in HoareAsLogic]
Q:70 [binder, in HoareAsLogic]
Q:73 [binder, in Hoare]
Q:73 [binder, in HoareAsLogic]
Q:76 [binder, in Hoare]
Q:8 [binder, in Hoare2]
Q:81 [binder, in Hoare]
Q:86 [binder, in Hoare]
Q:9 [binder, in HoareAsLogic]
Q:90 [binder, in Hoare]
Q:94 [binder, in Hoare]
Q:98 [binder, in Hoare]


R

reduce_to_zero_correct''' [lemma, in Hoare2]
reduce_to_zero_correct' [lemma, in Hoare2]
reduce_to_zero' [definition, in Hoare2]
refines [definition, in Equiv]
refl_cequiv [lemma, in Equiv]
refl_bequiv [lemma, in Equiv]
refl_aequiv [lemma, in Equiv]
relation [definition, in Smallstep]
R:122 [binder, in Smallstep]
R:130 [binder, in Smallstep]
R:134 [binder, in Smallstep]
R:141 [binder, in Smallstep]
R:16 [binder, in HoareAsLogic]
r:187 [binder, in Hoare]
r:192 [binder, in Hoare]
r:197 [binder, in Hoare]
r:206 [binder, in Hoare]
r:222 [binder, in Hoare]
R:245 [binder, in Hoare]
R:25 [binder, in Smallstep]
R:45 [binder, in Smallstep]
R:51 [binder, in Hoare]


S

sample_proof [definition, in HoareAsLogic]
seq_assoc [lemma, in Equiv]
SimpleArith1 [module, in Smallstep]
SimpleArith1.step [inductive, in Smallstep]
SimpleArith1.ST_Plus2 [constructor, in Smallstep]
SimpleArith1.ST_Plus1 [constructor, in Smallstep]
SimpleArith1.ST_PlusConstConst [constructor, in Smallstep]
SimpleArith1.test_step_2 [definition, in Smallstep]
SimpleArith1.test_step_1 [definition, in Smallstep]
_ --> _ [notation, in Smallstep]
SimpleArith2 [module, in Smallstep]
SimpleArith2.step_deterministic [lemma, in Smallstep]
SimpleArith3 [module, in Smallstep]
SimpleArith3.step_deterministic_alt [lemma, in Smallstep]
skip_right [lemma, in Equiv]
skip_left [lemma, in Equiv]
slow_assignment [lemma, in Hoare2]
slow_assignment_dec [definition, in Hoare2]
Smallstep [library]
SS_Mult [constructor, in Smallstep]
SS_Minus [constructor, in Smallstep]
SS_Plus [constructor, in Smallstep]
SS_Load [constructor, in Smallstep]
SS_Push [constructor, in Smallstep]
stack [definition, in Smallstep]
stack_multistep [definition, in Smallstep]
stack_step_deterministic [lemma, in Smallstep]
stack_step [inductive, in Smallstep]
step [inductive, in Smallstep]
step_example1''' [definition, in Smallstep]
step_example1'' [definition, in Smallstep]
step_example1' [definition, in Smallstep]
step_example1 [definition, in Smallstep]
step__eval [lemma, in Smallstep]
step_normalizing [lemma, in Smallstep]
step_normal_form [definition, in Smallstep]
step_deterministic [lemma, in Smallstep]
stk:323 [binder, in Smallstep]
stk:326 [binder, in Smallstep]
stk:329 [binder, in Smallstep]
stk:333 [binder, in Smallstep]
stk:337 [binder, in Smallstep]
STLC [module, in Stlc]
Stlc [library]
STLCArith [module, in StlcProp]
STLCArith.context [definition, in StlcProp]
STLCArith.has_type [inductive, in StlcProp]
STLCArith.multistep [abbreviation, in StlcProp]
STLCArith.Nat_typing_example [definition, in StlcProp]
STLCArith.Nat_step_example [definition, in StlcProp]
STLCArith.preservation [lemma, in StlcProp]
STLCArith.progress [lemma, in StlcProp]
STLCArith.step [inductive, in StlcProp]
STLCArith.subst [definition, in StlcProp]
STLCArith.tm [inductive, in StlcProp]
STLCArith.tm_if0 [constructor, in StlcProp]
STLCArith.tm_mult [constructor, in StlcProp]
STLCArith.tm_pred [constructor, in StlcProp]
STLCArith.tm_succ [constructor, in StlcProp]
STLCArith.tm_const [constructor, in StlcProp]
STLCArith.tm_abs [constructor, in StlcProp]
STLCArith.tm_app [constructor, in StlcProp]
STLCArith.tm_var [constructor, in StlcProp]
STLCArith.ty [inductive, in StlcProp]
STLCArith.Ty_Nat [constructor, in StlcProp]
STLCArith.Ty_Arrow [constructor, in StlcProp]
STLCArith.value [inductive, in StlcProp]
STLCArith.weakening [lemma, in StlcProp]
stlc:_ [notation, in StlcProp]
stlc:_ * _ [notation, in StlcProp]
stlc:_ _ [notation, in StlcProp]
stlc:_ -> _ [notation, in StlcProp]
stlc:if0 _ then _ else _ [notation, in StlcProp]
stlc:Nat [notation, in StlcProp]
stlc:pred _ [notation, in StlcProp]
stlc:succ _ [notation, in StlcProp]
stlc:( _ ) [notation, in StlcProp]
stlc:\ _ : _ , _ [notation, in StlcProp]
stlc:{ _ } [notation, in StlcProp]
_ |-- _ ∈ _ [notation, in StlcProp]
_ -->* _ [notation, in StlcProp]
_ --> _ [notation, in StlcProp]
<{ _ }> [notation, in StlcProp]
STLCProp [module, in StlcProp]
StlcProp [library]
STLCProp.afi_if3 [constructor, in StlcProp]
STLCProp.afi_if2 [constructor, in StlcProp]
STLCProp.afi_if1 [constructor, in StlcProp]
STLCProp.afi_abs [constructor, in StlcProp]
STLCProp.afi_app2 [constructor, in StlcProp]
STLCProp.afi_app1 [constructor, in StlcProp]
STLCProp.afi_var [constructor, in StlcProp]
STLCProp.appears_free_in [inductive, in StlcProp]
STLCProp.canonical_forms_fun [lemma, in StlcProp]
STLCProp.canonical_forms_bool [lemma, in StlcProp]
STLCProp.closed [definition, in StlcProp]
STLCProp.context_invariance [lemma, in StlcProp]
STLCProp.free_in_context [lemma, in StlcProp]
STLCProp.preservation [lemma, in StlcProp]
STLCProp.progress [lemma, in StlcProp]
STLCProp.progress' [lemma, in StlcProp]
STLCProp.stuck [definition, in StlcProp]
STLCProp.substitution_preserves_typing_from_typing_ind [lemma, in StlcProp]
STLCProp.substitution_preserves_typing [lemma, in StlcProp]
STLCProp.typable_empty__closed [lemma, in StlcProp]
STLCProp.type_soundness [lemma, in StlcProp]
STLCProp.unique_types [lemma, in StlcProp]
STLCProp.weakening [lemma, in StlcProp]
STLCProp.weakening_empty [lemma, in StlcProp]
STLC.context [definition, in Stlc]
STLC.has_type [inductive, in Stlc]
STLC.idB [abbreviation, in Stlc]
STLC.idBB [abbreviation, in Stlc]
STLC.idBBBB [abbreviation, in Stlc]
STLC.k [abbreviation, in Stlc]
STLC.multistep [abbreviation, in Stlc]
STLC.notB [abbreviation, in Stlc]
STLC.step [inductive, in Stlc]
STLC.step_example5_with_normalize [lemma, in Stlc]
STLC.step_example5 [lemma, in Stlc]
STLC.step_example4' [lemma, in Stlc]
STLC.step_example3' [lemma, in Stlc]
STLC.step_example2' [lemma, in Stlc]
STLC.step_example1' [lemma, in Stlc]
STLC.step_example4 [lemma, in Stlc]
STLC.step_example3 [lemma, in Stlc]
STLC.step_example2 [lemma, in Stlc]
STLC.step_example1 [lemma, in Stlc]
STLC.ST_If [constructor, in Stlc]
STLC.ST_IfFalse [constructor, in Stlc]
STLC.ST_IfTrue [constructor, in Stlc]
STLC.ST_App2 [constructor, in Stlc]
STLC.ST_App1 [constructor, in Stlc]
STLC.ST_AppAbs [constructor, in Stlc]
STLC.subst [definition, in Stlc]
STLC.substi [inductive, in Stlc]
STLC.substi_correct [lemma, in Stlc]
STLC.s_var1 [constructor, in Stlc]
STLC.tm [inductive, in Stlc]
STLC.tm_if [constructor, in Stlc]
STLC.tm_false [constructor, in Stlc]
STLC.tm_true [constructor, in Stlc]
STLC.tm_abs [constructor, in Stlc]
STLC.tm_app [constructor, in Stlc]
STLC.tm_var [constructor, in Stlc]
STLC.ty [inductive, in Stlc]
STLC.typing_nonexample_1 [definition, in Stlc]
STLC.typing_example_3 [definition, in Stlc]
STLC.typing_example_2 [definition, in Stlc]
STLC.typing_example_1' [definition, in Stlc]
STLC.typing_example_1 [definition, in Stlc]
STLC.Ty_Arrow [constructor, in Stlc]
STLC.Ty_Bool [constructor, in Stlc]
STLC.T_If [constructor, in Stlc]
STLC.T_False [constructor, in Stlc]
STLC.T_True [constructor, in Stlc]
STLC.T_App [constructor, in Stlc]
STLC.T_Abs [constructor, in Stlc]
STLC.T_Var [constructor, in Stlc]
STLC.value [inductive, in Stlc]
STLC.v_false [constructor, in Stlc]
STLC.v_true [constructor, in Stlc]
STLC.v_abs [constructor, in Stlc]
STLC.x [definition, in Stlc]
STLC.y [definition, in Stlc]
STLC.z [definition, in Stlc]
stlc:_ [notation, in Stlc]
stlc:_ _ [notation, in Stlc]
stlc:_ -> _ [notation, in Stlc]
stlc:Bool [notation, in Stlc]
stlc:false [notation, in Stlc]
stlc:if _ then _ else _ [notation, in Stlc]
stlc:true [notation, in Stlc]
stlc:( _ ) [notation, in Stlc]
stlc:[ _ := _ ] _ [notation, in Stlc]
stlc:\ _ : _ , _ [notation, in Stlc]
_ |-- _ ∈ _ [notation, in Stlc]
_ -->* _ [notation, in Stlc]
_ --> _ [notation, in Stlc]
false [notation, in Stlc]
true [notation, in Stlc]
<{ _ }> [notation, in Stlc]
strong_progress [lemma, in Smallstep]
ST_Plus2 [constructor, in Smallstep]
ST_Plus1 [constructor, in Smallstep]
ST_PlusConstConst [constructor, in Smallstep]
st'':132 [binder, in Hoare]
st'':148 [binder, in Hoare]
st':10 [binder, in Equiv]
st':131 [binder, in Hoare]
st':134 [binder, in Hoare]
st':139 [binder, in Hoare]
st':14 [binder, in Equiv]
st':147 [binder, in Hoare]
st':158 [binder, in Hoare]
st':186 [binder, in Hoare]
st':205 [binder, in Hoare]
st':223 [binder, in Hoare]
st':241 [binder, in Hoare]
st':242 [binder, in Hoare]
st':255 [binder, in Smallstep]
st':287 [binder, in Smallstep]
st':309 [binder, in Smallstep]
st':314 [binder, in Smallstep]
st':316 [binder, in Smallstep]
st':317 [binder, in Smallstep]
st':33 [binder, in Equiv]
st':39 [binder, in Hoare]
st':5 [binder, in HoareAsLogic]
st':74 [binder, in Equiv]
st':80 [binder, in Equiv]
st:1 [binder, in Hoare]
st:107 [binder, in Hoare]
st:109 [binder, in Hoare]
st:11 [binder, in Hoare]
st:12 [binder, in Hoare]
st:123 [binder, in Hoare]
st:124 [binder, in Hoare]
st:13 [binder, in Hoare]
st:13 [binder, in Equiv]
st:130 [binder, in Hoare]
st:133 [binder, in Hoare]
st:138 [binder, in Hoare]
st:14 [binder, in Hoare]
st:144 [binder, in Hoare]
st:146 [binder, in Hoare]
st:15 [binder, in Hoare]
st:151 [binder, in Hoare]
st:157 [binder, in Hoare]
st:16 [binder, in Hoare]
st:165 [binder, in Hoare]
st:17 [binder, in Hoare]
st:170 [binder, in Hoare]
st:178 [binder, in Hoare]
st:179 [binder, in Hoare]
st:18 [binder, in Hoare]
st:185 [binder, in Hoare]
st:188 [binder, in Smallstep]
st:19 [binder, in Hoare]
st:190 [binder, in Hoare]
st:191 [binder, in Hoare]
st:196 [binder, in Hoare]
st:2 [binder, in Hoare]
st:20 [binder, in Hoare]
st:202 [binder, in Hoare]
st:204 [binder, in Hoare]
st:209 [binder, in Hoare]
st:21 [binder, in Hoare]
st:212 [binder, in Hoare]
st:214 [binder, in Hoare]
st:216 [binder, in Hoare]
st:216 [binder, in Smallstep]
st:22 [binder, in Hoare]
st:22 [binder, in HoareAsLogic]
st:221 [binder, in Hoare]
st:23 [binder, in Hoare]
st:23 [binder, in HoareAsLogic]
st:24 [binder, in Hoare]
st:245 [binder, in Smallstep]
st:249 [binder, in Smallstep]
st:25 [binder, in Hoare]
st:252 [binder, in Smallstep]
st:257 [binder, in Smallstep]
st:259 [binder, in Smallstep]
st:264 [binder, in Smallstep]
st:267 [binder, in Smallstep]
st:27 [binder, in HoareAsLogic]
st:270 [binder, in Smallstep]
st:277 [binder, in Smallstep]
st:28 [binder, in HoareAsLogic]
st:281 [binder, in Smallstep]
st:284 [binder, in Smallstep]
st:289 [binder, in Smallstep]
st:29 [binder, in Hoare]
st:291 [binder, in Smallstep]
st:296 [binder, in Smallstep]
st:299 [binder, in Smallstep]
st:3 [binder, in Hoare]
st:3 [binder, in Equiv]
st:302 [binder, in Smallstep]
st:305 [binder, in Smallstep]
st:310 [binder, in Smallstep]
st:315 [binder, in Smallstep]
st:319 [binder, in Smallstep]
st:32 [binder, in Equiv]
st:320 [binder, in Smallstep]
st:34 [binder, in Hoare]
st:34 [binder, in HoareAsLogic]
st:341 [binder, in Smallstep]
st:342 [binder, in Smallstep]
st:35 [binder, in HoareAsLogic]
st:38 [binder, in Hoare]
st:4 [binder, in Hoare]
st:4 [binder, in HoareAsLogic]
st:40 [binder, in HoareAsLogic]
st:43 [binder, in Hoare]
st:45 [binder, in HoareAsLogic]
st:46 [binder, in HoareAsLogic]
st:47 [binder, in Hoare]
st:47 [binder, in HoareAsLogic]
st:57 [binder, in Hoare]
st:6 [binder, in Equiv]
st:64 [binder, in Hoare]
st:65 [binder, in Hoare]
st:68 [binder, in Hoare]
st:69 [binder, in Hoare]
st:7 [binder, in Hoare]
st:73 [binder, in Equiv]
st:79 [binder, in Equiv]
st:9 [binder, in Equiv]
subst_inequiv [lemma, in Equiv]
subst_equiv_property [definition, in Equiv]
subst_aexp_ex [definition, in Equiv]
subst_aexp [definition, in Equiv]
subtract_slowly_outer_triple_valid [lemma, in Hoare2]
subtract_slowly_dec [definition, in Hoare2]
swap_exercise [lemma, in Hoare]
swap_program [definition, in Hoare]
swap_if_branches [lemma, in Equiv]
swap_correct [lemma, in Hoare2]
swap_dec [definition, in Hoare2]
sym_cequiv [lemma, in Equiv]
sym_bequiv [lemma, in Equiv]
sym_aequiv [lemma, in Equiv]
s':58 [binder, in HoareAsLogic]
s:11 [binder, in Stlc]
s:15 [binder, in Stlc]
s:19 [binder, in Stlc]
s:57 [binder, in HoareAsLogic]
s:81 [binder, in StlcProp]


T

Temp1 [module, in Smallstep]
Temp1.step [inductive, in Smallstep]
Temp1.ST_Plus2 [constructor, in Smallstep]
Temp1.ST_Plus1 [constructor, in Smallstep]
Temp1.ST_PlusConstConst [constructor, in Smallstep]
Temp1.value [inductive, in Smallstep]
Temp1.value_not_same_as_normal_form [lemma, in Smallstep]
Temp1.v_funny [constructor, in Smallstep]
Temp1.v_const [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
Temp2 [module, in Smallstep]
Temp2.step [inductive, in Smallstep]
Temp2.ST_Plus2 [constructor, in Smallstep]
Temp2.ST_Plus1 [constructor, in Smallstep]
Temp2.ST_PlusConstConst [constructor, in Smallstep]
Temp2.ST_Funny [constructor, in Smallstep]
Temp2.value [inductive, in Smallstep]
Temp2.value_not_same_as_normal_form [lemma, in Smallstep]
Temp2.v_const [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
Temp3 [module, in Smallstep]
Temp3.step [inductive, in Smallstep]
Temp3.ST_Plus1 [constructor, in Smallstep]
Temp3.ST_PlusConstConst [constructor, in Smallstep]
Temp3.value [inductive, in Smallstep]
Temp3.value_not_same_as_normal_form [lemma, in Smallstep]
Temp3.v_const [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
Temp4 [module, in Smallstep]
Temp4.fls [constructor, in Smallstep]
Temp4.step [inductive, in Smallstep]
Temp4.step_deterministic [lemma, in Smallstep]
Temp4.strong_progress_bool [lemma, in Smallstep]
Temp4.ST_If [constructor, in Smallstep]
Temp4.ST_IfFalse [constructor, in Smallstep]
Temp4.ST_IfTrue [constructor, in Smallstep]
Temp4.Temp5 [module, in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [definition, in Smallstep]
Temp4.Temp5.bool_step_prop4 [definition, in Smallstep]
Temp4.Temp5.step [inductive, in Smallstep]
Temp4.Temp5.ST_If [constructor, in Smallstep]
Temp4.Temp5.ST_IfFalse [constructor, in Smallstep]
Temp4.Temp5.ST_IfTrue [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
Temp4.test [constructor, in Smallstep]
Temp4.tm [inductive, in Smallstep]
Temp4.tru [constructor, in Smallstep]
Temp4.value [inductive, in Smallstep]
Temp4.v_fls [constructor, in Smallstep]
Temp4.v_tru [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
test_multistep_4 [lemma, in Smallstep]
test_multistep_1' [lemma, in Smallstep]
test_multistep_1 [lemma, in Smallstep]
tm [inductive, in Smallstep]
TM [module, in Types]
TM.Bool [constructor, in Types]
TM.bool_canonical [lemma, in Types]
TM.bvalue [inductive, in Types]
TM.bv_false [constructor, in Types]
TM.bv_True [constructor, in Types]
TM.fls [constructor, in Types]
TM.has_type_not [definition, in Types]
TM.has_type_1 [definition, in Types]
TM.has_type [inductive, in Types]
TM.iszro [constructor, in Types]
TM.ite [constructor, in Types]
TM.multistep [definition, in Types]
TM.Nat [constructor, in Types]
TM.nat_canonical [lemma, in Types]
TM.nvalue [inductive, in Types]
TM.nv_succ [constructor, in Types]
TM.nv_0 [constructor, in Types]
TM.prd [constructor, in Types]
TM.preservation [lemma, in Types]
TM.preservation' [lemma, in Types]
TM.progress [lemma, in Types]
TM.scc [constructor, in Types]
TM.some_term_is_stuck [definition, in Types]
TM.soundness [lemma, in Types]
TM.step [inductive, in Types]
TM.step_deterministic [lemma, in Types]
TM.step_normal_form [abbreviation, in Types]
TM.stuck [definition, in Types]
TM.ST_Iszero [constructor, in Types]
TM.ST_IszeroSucc [constructor, in Types]
TM.ST_Iszero0 [constructor, in Types]
TM.ST_Pred [constructor, in Types]
TM.ST_PredSucc [constructor, in Types]
TM.ST_Pred0 [constructor, in Types]
TM.ST_Succ [constructor, in Types]
TM.ST_If [constructor, in Types]
TM.ST_IfFalse [constructor, in Types]
TM.ST_IfTrue [constructor, in Types]
TM.subject_expansion [lemma, in Types]
TM.tm [inductive, in Types]
TM.tru [constructor, in Types]
TM.ty [inductive, in Types]
TM.T_Iszero [constructor, in Types]
TM.T_Pred [constructor, in Types]
TM.T_Succ [constructor, in Types]
TM.T_0 [constructor, in Types]
TM.T_If [constructor, in Types]
TM.T_False [constructor, in Types]
TM.T_True [constructor, in Types]
TM.value [definition, in Types]
TM.value_is_nf [lemma, in Types]
TM.zro [constructor, in Types]
tm:if _ then _ else _ (tm_scope) [notation, in Types]
tm:iszero _ (tm_scope) [notation, in Types]
tm:pred _ (tm_scope) [notation, in Types]
tm:succ _ (tm_scope) [notation, in Types]
tm:0 (tm_scope) [notation, in Types]
tm:_ (tm_scope) [notation, in Types]
tm:( _ ) (tm_scope) [notation, in Types]
tm:false (tm_scope) [notation, in Types]
tm:true (tm_scope) [notation, in Types]
0 (tm_scope) [notation, in Types]
<{ _ }> (tm_scope) [notation, in Types]
false (tm_scope) [notation, in Types]
true (tm_scope) [notation, in Types]
_ -->* _ [notation, in Types]
_ --> _ [notation, in Types]
|-- _ ∈ _ [notation, in Types]
trans_cequiv [lemma, in Equiv]
trans_bequiv [lemma, in Equiv]
trans_aequiv [lemma, in Equiv]
two_loops [lemma, in Hoare2]
two_loops_dec [definition, in Hoare2]
Types [library]
t':100 [binder, in StlcProp]
t':110 [binder, in Smallstep]
t':12 [binder, in StlcProp]
t':139 [binder, in Smallstep]
t':143 [binder, in Smallstep]
t':153 [binder, in Smallstep]
t':156 [binder, in Smallstep]
t':182 [binder, in Smallstep]
t':184 [binder, in Smallstep]
t':22 [binder, in Stlc]
t':33 [binder, in StlcProp]
t':37 [binder, in StlcProp]
T':42 [binder, in StlcProp]
t':43 [binder, in Smallstep]
t':45 [binder, in Types]
t':47 [binder, in Smallstep]
t':47 [binder, in Types]
t':50 [binder, in Smallstep]
t':50 [binder, in Types]
t':51 [binder, in Smallstep]
t':53 [binder, in Types]
t':56 [binder, in Types]
t':59 [binder, in Types]
T':68 [binder, in StlcProp]
t':9 [binder, in StlcProp]
t':96 [binder, in StlcProp]
t1':106 [binder, in Smallstep]
t1':118 [binder, in Smallstep]
t1':145 [binder, in Smallstep]
t1':168 [binder, in Smallstep]
t1':178 [binder, in Smallstep]
t1':18 [binder, in Smallstep]
t1':20 [binder, in Types]
t1':23 [binder, in Types]
t1':26 [binder, in Types]
t1':30 [binder, in Stlc]
t1':37 [binder, in Smallstep]
t1':40 [binder, in Stlc]
t1':63 [binder, in Smallstep]
t1':78 [binder, in Smallstep]
t1':92 [binder, in Smallstep]
t1:101 [binder, in Smallstep]
t1:103 [binder, in Smallstep]
t1:105 [binder, in Smallstep]
t1:11 [binder, in Types]
t1:113 [binder, in Smallstep]
t1:115 [binder, in Smallstep]
t1:117 [binder, in Smallstep]
t1:13 [binder, in Types]
t1:144 [binder, in Smallstep]
t1:167 [binder, in Smallstep]
t1:17 [binder, in Smallstep]
t1:173 [binder, in Smallstep]
t1:175 [binder, in Smallstep]
t1:177 [binder, in Smallstep]
t1:19 [binder, in Types]
t1:22 [binder, in Types]
t1:25 [binder, in Types]
t1:27 [binder, in Stlc]
t1:29 [binder, in Stlc]
T1:3 [binder, in StlcProp]
t1:34 [binder, in Types]
t1:35 [binder, in Stlc]
t1:36 [binder, in Smallstep]
t1:37 [binder, in Stlc]
t1:38 [binder, in Types]
t1:39 [binder, in Stlc]
t1:39 [binder, in Types]
t1:40 [binder, in Types]
t1:46 [binder, in StlcProp]
T1:47 [binder, in Stlc]
t1:48 [binder, in StlcProp]
T1:50 [binder, in Stlc]
T1:51 [binder, in StlcProp]
t1:52 [binder, in StlcProp]
t1:52 [binder, in Stlc]
t1:53 [binder, in StlcProp]
T1:53 [binder, in Stlc]
t1:56 [binder, in Smallstep]
t1:56 [binder, in StlcProp]
t1:56 [binder, in Stlc]
t1:59 [binder, in StlcProp]
t1:60 [binder, in Stlc]
t1:62 [binder, in Smallstep]
T1:63 [binder, in Stlc]
t1:77 [binder, in Smallstep]
t1:9 [binder, in Smallstep]
t1:9 [binder, in Stlc]
t1:91 [binder, in Smallstep]
t2':149 [binder, in Smallstep]
t2':172 [binder, in Smallstep]
t2':22 [binder, in Smallstep]
t2':34 [binder, in Stlc]
t2':41 [binder, in Smallstep]
t2':67 [binder, in Smallstep]
t2':82 [binder, in Smallstep]
t2:10 [binder, in Smallstep]
t2:102 [binder, in Smallstep]
t2:104 [binder, in Smallstep]
t2:107 [binder, in Smallstep]
t2:114 [binder, in Smallstep]
t2:116 [binder, in Smallstep]
t2:119 [binder, in Smallstep]
t2:12 [binder, in Types]
t2:14 [binder, in Types]
t2:146 [binder, in Smallstep]
t2:148 [binder, in Smallstep]
t2:169 [binder, in Smallstep]
t2:17 [binder, in Types]
t2:171 [binder, in Smallstep]
t2:174 [binder, in Smallstep]
t2:176 [binder, in Smallstep]
t2:179 [binder, in Smallstep]
t2:19 [binder, in Smallstep]
t2:21 [binder, in Smallstep]
T2:26 [binder, in Stlc]
t2:31 [binder, in Stlc]
t2:33 [binder, in Stlc]
t2:35 [binder, in Types]
t2:36 [binder, in Stlc]
t2:38 [binder, in Smallstep]
t2:38 [binder, in Stlc]
T2:4 [binder, in StlcProp]
t2:40 [binder, in Smallstep]
t2:41 [binder, in Stlc]
t2:47 [binder, in StlcProp]
t2:49 [binder, in StlcProp]
T2:51 [binder, in Stlc]
t2:54 [binder, in StlcProp]
T2:54 [binder, in Stlc]
t2:57 [binder, in StlcProp]
t2:57 [binder, in Stlc]
t2:60 [binder, in StlcProp]
t2:61 [binder, in Stlc]
t2:64 [binder, in Smallstep]
t2:66 [binder, in Smallstep]
t2:79 [binder, in Smallstep]
T2:8 [binder, in Stlc]
t2:81 [binder, in Smallstep]
t2:93 [binder, in Smallstep]
t3:108 [binder, in Smallstep]
t3:120 [binder, in Smallstep]
t3:18 [binder, in Types]
t3:180 [binder, in Smallstep]
t3:36 [binder, in Types]
t3:42 [binder, in Stlc]
t3:55 [binder, in StlcProp]
t3:58 [binder, in StlcProp]
t3:61 [binder, in StlcProp]
t3:62 [binder, in Stlc]
t:1 [binder, in StlcProp]
t:10 [binder, in StlcProp]
t:109 [binder, in Smallstep]
T:11 [binder, in StlcProp]
t:12 [binder, in Stlc]
t:138 [binder, in Smallstep]
t:142 [binder, in Smallstep]
t:15 [binder, in StlcProp]
t:150 [binder, in Smallstep]
t:152 [binder, in Smallstep]
t:155 [binder, in Smallstep]
T:16 [binder, in StlcProp]
t:18 [binder, in StlcProp]
t:181 [binder, in Smallstep]
t:183 [binder, in Smallstep]
T:19 [binder, in StlcProp]
t:2 [binder, in StlcProp]
t:21 [binder, in Stlc]
t:23 [binder, in StlcProp]
T:25 [binder, in StlcProp]
t:27 [binder, in Types]
t:28 [binder, in Types]
t:29 [binder, in StlcProp]
t:29 [binder, in Types]
t:3 [binder, in Smallstep]
T:31 [binder, in StlcProp]
t:32 [binder, in StlcProp]
T:34 [binder, in StlcProp]
t:35 [binder, in StlcProp]
t:36 [binder, in StlcProp]
T:37 [binder, in Types]
T:38 [binder, in StlcProp]
T:41 [binder, in StlcProp]
t:41 [binder, in Types]
t:42 [binder, in Smallstep]
t:42 [binder, in Types]
t:43 [binder, in Types]
T:44 [binder, in Types]
t:46 [binder, in Smallstep]
t:46 [binder, in Types]
T:48 [binder, in Types]
t:49 [binder, in Smallstep]
t:49 [binder, in Types]
T:51 [binder, in Types]
t:52 [binder, in Smallstep]
t:52 [binder, in Types]
T:54 [binder, in Types]
t:55 [binder, in Types]
T:57 [binder, in Types]
t:58 [binder, in Types]
T:60 [binder, in Types]
t:62 [binder, in StlcProp]
t:65 [binder, in StlcProp]
T:65 [binder, in Stlc]
T:66 [binder, in StlcProp]
T:66 [binder, in Stlc]
t:69 [binder, in StlcProp]
t:7 [binder, in StlcProp]
t:7 [binder, in Types]
T:70 [binder, in StlcProp]
t:73 [binder, in StlcProp]
T:74 [binder, in StlcProp]
T:8 [binder, in StlcProp]
t:8 [binder, in Types]
t:82 [binder, in StlcProp]
t:88 [binder, in StlcProp]
t:93 [binder, in StlcProp]
t:94 [binder, in Smallstep]
T:94 [binder, in StlcProp]
t:95 [binder, in StlcProp]
T:97 [binder, in StlcProp]
t:98 [binder, in StlcProp]
T:99 [binder, in StlcProp]


U

u:107 [binder, in Equiv]
U:22 [binder, in StlcProp]
U:28 [binder, in StlcProp]
u:6 [binder, in StlcProp]


V

valid [definition, in HoareAsLogic]
value [inductive, in Smallstep]
value_is_nf [lemma, in Smallstep]
vc_dec_while [definition, in Hoare2]
verification_correct_dec [lemma, in Hoare2]
verification_conditions_dec [definition, in Hoare2]
verification_correct [lemma, in Hoare2]
verification_conditions [definition, in Hoare2]
v_const [constructor, in Smallstep]
v1:11 [binder, in Smallstep]
v1:147 [binder, in Smallstep]
v1:15 [binder, in Smallstep]
v1:165 [binder, in Smallstep]
v1:170 [binder, in Smallstep]
v1:195 [binder, in Smallstep]
v1:198 [binder, in Smallstep]
v1:20 [binder, in Smallstep]
v1:203 [binder, in Smallstep]
v1:206 [binder, in Smallstep]
v1:211 [binder, in Smallstep]
v1:214 [binder, in Smallstep]
v1:222 [binder, in Smallstep]
v1:225 [binder, in Smallstep]
v1:230 [binder, in Smallstep]
v1:233 [binder, in Smallstep]
v1:32 [binder, in Stlc]
v1:34 [binder, in Smallstep]
v1:39 [binder, in Smallstep]
v1:60 [binder, in Smallstep]
v1:65 [binder, in Smallstep]
v1:75 [binder, in Smallstep]
v1:80 [binder, in Smallstep]
v1:89 [binder, in Smallstep]
v2:12 [binder, in Smallstep]
v2:16 [binder, in Smallstep]
v2:166 [binder, in Smallstep]
v2:199 [binder, in Smallstep]
v2:207 [binder, in Smallstep]
v2:215 [binder, in Smallstep]
v2:226 [binder, in Smallstep]
v2:234 [binder, in Smallstep]
v2:28 [binder, in Stlc]
v2:35 [binder, in Smallstep]
v2:57 [binder, in Smallstep]
v2:61 [binder, in Smallstep]
v2:76 [binder, in Smallstep]
v2:90 [binder, in Smallstep]
V:10 [binder, in HoareAsLogic]
v:21 [binder, in Types]
v:24 [binder, in StlcProp]
v:24 [binder, in Types]
v:30 [binder, in StlcProp]
v:48 [binder, in Smallstep]
v:68 [binder, in Smallstep]
v:83 [binder, in Smallstep]


W

while_example [definition, in Hoare]
while_true [lemma, in Equiv]
while_true_nonterm [lemma, in Equiv]
while_false [lemma, in Equiv]
wp [definition, in HoareAsLogic]
wp_invariant [lemma, in HoareAsLogic]
wp_seq [lemma, in HoareAsLogic]
wp_is_weakest [lemma, in HoareAsLogic]
wp_is_precondition [lemma, in HoareAsLogic]


X

x1:111 [binder, in Equiv]
x2:112 [binder, in Equiv]
x:10 [binder, in Stlc]
x:106 [binder, in Equiv]
X:121 [binder, in Smallstep]
x:125 [binder, in Smallstep]
x:126 [binder, in Smallstep]
x:127 [binder, in Hoare]
X:129 [binder, in Smallstep]
x:131 [binder, in Smallstep]
X:133 [binder, in Smallstep]
x:135 [binder, in Smallstep]
X:140 [binder, in Smallstep]
x:152 [binder, in Hoare]
x:16 [binder, in Stlc]
X:163 [binder, in Hoare]
X:167 [binder, in Hoare]
X:169 [binder, in Hoare]
x:182 [binder, in Hoare]
x:20 [binder, in Stlc]
x:21 [binder, in StlcProp]
X:23 [binder, in Smallstep]
X:231 [binder, in Hoare]
X:24 [binder, in Smallstep]
x:25 [binder, in Stlc]
X:26 [binder, in Hoare]
x:26 [binder, in Smallstep]
x:27 [binder, in StlcProp]
x:28 [binder, in Hoare]
X:30 [binder, in Hoare]
x:32 [binder, in Hoare]
x:41 [binder, in Equiv]
X:42 [binder, in Equiv]
x:43 [binder, in StlcProp]
X:44 [binder, in Smallstep]
x:46 [binder, in Stlc]
x:49 [binder, in Stlc]
x:5 [binder, in StlcProp]
X:54 [binder, in Hoare]
X:59 [binder, in Hoare]
X:6 [binder, in Hoare2]
x:62 [binder, in Equiv]
x:63 [binder, in StlcProp]
x:64 [binder, in StlcProp]
x:7 [binder, in Stlc]
x:75 [binder, in StlcProp]
x:80 [binder, in StlcProp]


Y

y1:27 [binder, in Smallstep]
y2:28 [binder, in Smallstep]
y:127 [binder, in Smallstep]
y:132 [binder, in Smallstep]
y:136 [binder, in Smallstep]
y:33 [binder, in Hoare]
y:50 [binder, in StlcProp]


Z

z:128 [binder, in Smallstep]
z:137 [binder, in Smallstep]


other

com:{{ _ }} _ (dcom_scope) [notation, in Hoare2]
com:_ ; _ (dcom_scope) [notation, in Hoare2]
com:_ ->> {{ _ }} (dcom_scope) [notation, in Hoare2]
com:->> {{ _ }} _ (dcom_scope) [notation, in Hoare2]
com:if _ then {{ _ }} _ else {{ _ }} _ end {{ _ }} (dcom_scope) [notation, in Hoare2]
com:while _ do {{ _ }} _ end {{ _ }} (dcom_scope) [notation, in Hoare2]
com:_ := _ {{ _ }} (dcom_scope) [notation, in Hoare2]
com:skip {{ _ }} (dcom_scope) [notation, in Hoare2]
_ * _ (assertion_scope) [notation, in Hoare]
_ - _ (assertion_scope) [notation, in Hoare]
_ + _ (assertion_scope) [notation, in Hoare]
_ > _ (assertion_scope) [notation, in Hoare]
_ >= _ (assertion_scope) [notation, in Hoare]
_ < _ (assertion_scope) [notation, in Hoare]
_ <= _ (assertion_scope) [notation, in Hoare]
_ <> _ (assertion_scope) [notation, in Hoare]
_ = _ (assertion_scope) [notation, in Hoare]
_ <-> _ (assertion_scope) [notation, in Hoare]
_ -> _ (assertion_scope) [notation, in Hoare]
_ \/ _ (assertion_scope) [notation, in Hoare]
_ /\ _ (assertion_scope) [notation, in Hoare]
~ _ (assertion_scope) [notation, in Hoare]
_ [ _ ⊢> _ ] (hoare_spec_scope) [notation, in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [notation, in Hoare]
_ <<->> _ (hoare_spec_scope) [notation, in Hoare]
_ ->> _ (hoare_spec_scope) [notation, in Hoare]
_ / _ --> _ / _ [notation, in Smallstep]
_ / _ -->b _ [notation, in Smallstep]
_ / _ -->a _ [notation, in Smallstep]
_ -->* _ [notation, in Smallstep]
_ --> _ [notation, in Smallstep]
_ ==> _ [notation, in Smallstep]


Notation Index

C

com:_ ; _ [in Smallstep]
com:_ := _ [in Smallstep]
com:_ || _ [in Smallstep]
com:if _ then _ else _ end [in Smallstep]
com:skip [in Smallstep]
com:while _ do _ end [in Smallstep]
_ / _ -->* _ / _ [in Smallstep]
_ / _ --> _ / _ [in Smallstep]
_ --> _ [in Smallstep]


H

com:_ ; _ [in Hoare]
com:_ := _ [in Hoare]
com:havoc _ [in Hoare]
com:if _ then _ else _ end [in Hoare]
com:skip [in Hoare]
com:while _ do _ end [in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]
com:_ ; _ [in Hoare]
com:_ := _ [in Hoare]
com:assert _ [in Hoare]
com:assume _ [in Hoare]
com:if _ then _ else _ end [in Hoare]
com:skip [in Hoare]
com:while _ do _ end [in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]


S

_ --> _ [in Smallstep]
stlc:_ [in StlcProp]
stlc:_ * _ [in StlcProp]
stlc:_ _ [in StlcProp]
stlc:_ -> _ [in StlcProp]
stlc:if0 _ then _ else _ [in StlcProp]
stlc:Nat [in StlcProp]
stlc:pred _ [in StlcProp]
stlc:succ _ [in StlcProp]
stlc:( _ ) [in StlcProp]
stlc:\ _ : _ , _ [in StlcProp]
stlc:{ _ } [in StlcProp]
_ |-- _ ∈ _ [in StlcProp]
_ -->* _ [in StlcProp]
_ --> _ [in StlcProp]
<{ _ }> [in StlcProp]
stlc:_ [in Stlc]
stlc:_ _ [in Stlc]
stlc:_ -> _ [in Stlc]
stlc:Bool [in Stlc]
stlc:false [in Stlc]
stlc:if _ then _ else _ [in Stlc]
stlc:true [in Stlc]
stlc:( _ ) [in Stlc]
stlc:[ _ := _ ] _ [in Stlc]
stlc:\ _ : _ , _ [in Stlc]
_ |-- _ ∈ _ [in Stlc]
_ -->* _ [in Stlc]
_ --> _ [in Stlc]
false [in Stlc]
true [in Stlc]
<{ _ }> [in Stlc]


T

_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
tm:if _ then _ else _ (tm_scope) [in Types]
tm:iszero _ (tm_scope) [in Types]
tm:pred _ (tm_scope) [in Types]
tm:succ _ (tm_scope) [in Types]
tm:0 (tm_scope) [in Types]
tm:_ (tm_scope) [in Types]
tm:( _ ) (tm_scope) [in Types]
tm:false (tm_scope) [in Types]
tm:true (tm_scope) [in Types]
0 (tm_scope) [in Types]
<{ _ }> (tm_scope) [in Types]
false (tm_scope) [in Types]
true (tm_scope) [in Types]
_ -->* _ [in Types]
_ --> _ [in Types]
|-- _ ∈ _ [in Types]


other

com:{{ _ }} _ (dcom_scope) [in Hoare2]
com:_ ; _ (dcom_scope) [in Hoare2]
com:_ ->> {{ _ }} (dcom_scope) [in Hoare2]
com:->> {{ _ }} _ (dcom_scope) [in Hoare2]
com:if _ then {{ _ }} _ else {{ _ }} _ end {{ _ }} (dcom_scope) [in Hoare2]
com:while _ do {{ _ }} _ end {{ _ }} (dcom_scope) [in Hoare2]
com:_ := _ {{ _ }} (dcom_scope) [in Hoare2]
com:skip {{ _ }} (dcom_scope) [in Hoare2]
_ * _ (assertion_scope) [in Hoare]
_ - _ (assertion_scope) [in Hoare]
_ + _ (assertion_scope) [in Hoare]
_ > _ (assertion_scope) [in Hoare]
_ >= _ (assertion_scope) [in Hoare]
_ < _ (assertion_scope) [in Hoare]
_ <= _ (assertion_scope) [in Hoare]
_ <> _ (assertion_scope) [in Hoare]
_ = _ (assertion_scope) [in Hoare]
_ <-> _ (assertion_scope) [in Hoare]
_ -> _ (assertion_scope) [in Hoare]
_ \/ _ (assertion_scope) [in Hoare]
_ /\ _ (assertion_scope) [in Hoare]
~ _ (assertion_scope) [in Hoare]
_ [ _ ⊢> _ ] (hoare_spec_scope) [in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ <<->> _ (hoare_spec_scope) [in Hoare]
_ ->> _ (hoare_spec_scope) [in Hoare]
_ / _ --> _ / _ [in Smallstep]
_ / _ -->b _ [in Smallstep]
_ / _ -->a _ [in Smallstep]
_ -->* _ [in Smallstep]
_ --> _ [in Smallstep]
_ ==> _ [in Smallstep]


Binder Index

A

atrans:91 [in Equiv]
a':64 [in Equiv]
a1':193 [in Smallstep]
a1':201 [in Smallstep]
a1':209 [in Smallstep]
a1':220 [in Smallstep]
a1':228 [in Smallstep]
a1':248 [in Smallstep]
a1':280 [in Smallstep]
a1:1 [in Equiv]
a1:113 [in Equiv]
a1:125 [in Hoare]
a1:180 [in Hoare]
a1:192 [in Smallstep]
a1:200 [in Smallstep]
a1:208 [in Smallstep]
a1:219 [in Smallstep]
a1:227 [in Smallstep]
a1:247 [in Smallstep]
a1:279 [in Smallstep]
a1:45 [in Equiv]
a1:47 [in Equiv]
a2':197 [in Smallstep]
a2':205 [in Smallstep]
a2':213 [in Smallstep]
a2':224 [in Smallstep]
a2':232 [in Smallstep]
a2:114 [in Equiv]
a2:194 [in Smallstep]
a2:196 [in Smallstep]
a2:2 [in Equiv]
a2:202 [in Smallstep]
a2:204 [in Smallstep]
a2:210 [in Smallstep]
a2:212 [in Smallstep]
a2:221 [in Smallstep]
a2:223 [in Smallstep]
a2:229 [in Smallstep]
a2:231 [in Smallstep]
a2:46 [in Equiv]
a2:48 [in Equiv]
a3:49 [in Equiv]
a:10 [in Hoare]
a:104 [in Hoare]
a:108 [in Equiv]
a:11 [in HoareAsLogic]
a:232 [in Hoare]
a:43 [in Equiv]
a:44 [in Equiv]
a:55 [in Hoare]
a:57 [in Hoare2]
a:59 [in Hoare2]
a:60 [in Hoare]
a:61 [in Hoare2]
a:62 [in Hoare]
a:63 [in Equiv]
a:64 [in Hoare2]
a:66 [in Hoare]
a:7 [in Hoare2]
a:92 [in Equiv]
a:97 [in Equiv]


B

btrans:93 [in Equiv]
b':66 [in Equiv]
b':70 [in Equiv]
b':76 [in Equiv]
b':86 [in Equiv]
b1':236 [in Smallstep]
b1':238 [in Smallstep]
b1':261 [in Smallstep]
b1':293 [in Smallstep]
b1:235 [in Smallstep]
b1:237 [in Smallstep]
b1:260 [in Smallstep]
b1:271 [in Smallstep]
b1:292 [in Smallstep]
b1:303 [in Smallstep]
b1:4 [in Equiv]
b1:51 [in Equiv]
b1:53 [in Equiv]
b2':241 [in Smallstep]
b2:239 [in Smallstep]
b2:240 [in Smallstep]
b2:242 [in Smallstep]
b2:5 [in Equiv]
b2:52 [in Equiv]
b2:54 [in Equiv]
b3:55 [in Equiv]
b:100 [in Equiv]
b:106 [in Hoare]
b:108 [in Hoare]
b:112 [in Hoare]
b:116 [in Hoare]
b:135 [in Hoare]
b:140 [in Hoare]
b:143 [in Hoare]
b:149 [in Hoare]
b:15 [in Hoare2]
b:19 [in Equiv]
b:19 [in HoareAsLogic]
b:193 [in Hoare]
b:198 [in Hoare]
b:201 [in Hoare]
b:207 [in Hoare]
b:210 [in Hoare]
b:213 [in Hoare]
b:215 [in Hoare]
b:217 [in Hoare]
b:22 [in Equiv]
b:225 [in Hoare]
b:228 [in Hoare]
b:25 [in Equiv]
b:25 [in HoareAsLogic]
b:251 [in Hoare]
b:255 [in Hoare]
b:28 [in Equiv]
b:30 [in Equiv]
b:34 [in Equiv]
b:36 [in Equiv]
b:50 [in Equiv]
b:58 [in Hoare2]
b:60 [in Hoare2]
b:62 [in Hoare2]
b:65 [in Equiv]
b:65 [in Hoare2]
b:68 [in HoareAsLogic]
b:69 [in Equiv]
b:75 [in Equiv]
b:85 [in Equiv]
b:9 [in Hoare2]
b:94 [in Equiv]


C

ctrans:95 [in Equiv]
c':16 [in Types]
c':68 [in Equiv]
c':72 [in Equiv]
c':78 [in Equiv]
c1':254 [in Smallstep]
c1':286 [in Smallstep]
c1':307 [in Smallstep]
c1':82 [in Equiv]
c1':88 [in Equiv]
c1:11 [in Equiv]
c1:113 [in Hoare]
c1:128 [in Hoare]
c1:136 [in Hoare]
c1:141 [in Hoare]
c1:17 [in Equiv]
c1:183 [in Hoare]
c1:188 [in Hoare]
c1:194 [in Hoare]
c1:199 [in Hoare]
c1:20 [in Equiv]
c1:20 [in HoareAsLogic]
c1:23 [in Equiv]
c1:246 [in Hoare]
c1:252 [in Hoare]
c1:253 [in Smallstep]
c1:26 [in Equiv]
c1:262 [in Smallstep]
c1:265 [in Smallstep]
c1:268 [in Smallstep]
c1:272 [in Smallstep]
c1:285 [in Smallstep]
c1:294 [in Smallstep]
c1:297 [in Smallstep]
c1:300 [in Smallstep]
c1:304 [in Smallstep]
c1:306 [in Smallstep]
c1:311 [in Smallstep]
c1:38 [in Equiv]
c1:52 [in Hoare]
c1:57 [in Equiv]
c1:59 [in Equiv]
c1:66 [in HoareAsLogic]
c1:7 [in Equiv]
c1:81 [in Equiv]
c1:87 [in Equiv]
c2':313 [in Smallstep]
c2':84 [in Equiv]
c2':90 [in Equiv]
c2:114 [in Hoare]
c2:12 [in Equiv]
c2:129 [in Hoare]
c2:137 [in Hoare]
c2:142 [in Hoare]
c2:18 [in Equiv]
c2:184 [in Hoare]
c2:189 [in Hoare]
c2:195 [in Hoare]
c2:200 [in Hoare]
c2:21 [in Equiv]
c2:21 [in HoareAsLogic]
c2:24 [in Equiv]
c2:247 [in Hoare]
c2:253 [in Hoare]
c2:256 [in Smallstep]
c2:258 [in Smallstep]
c2:263 [in Smallstep]
c2:266 [in Smallstep]
c2:269 [in Smallstep]
c2:27 [in Equiv]
c2:288 [in Smallstep]
c2:290 [in Smallstep]
c2:295 [in Smallstep]
c2:298 [in Smallstep]
c2:301 [in Smallstep]
c2:308 [in Smallstep]
c2:312 [in Smallstep]
c2:39 [in Equiv]
c2:53 [in Hoare]
c2:58 [in Equiv]
c2:60 [in Equiv]
c2:67 [in HoareAsLogic]
c2:8 [in Equiv]
c2:83 [in Equiv]
c2:89 [in Equiv]
c3:40 [in Equiv]
c3:61 [in Equiv]
c:103 [in Hoare]
c:103 [in Equiv]
c:117 [in Hoare]
c:13 [in HoareAsLogic]
c:145 [in Hoare]
c:15 [in Equiv]
c:15 [in Types]
c:150 [in Hoare]
c:155 [in Hoare]
c:16 [in Equiv]
c:162 [in Hoare]
c:2 [in HoareAsLogic]
c:203 [in Hoare]
c:208 [in Hoare]
c:211 [in Hoare]
c:219 [in Hoare]
c:236 [in Hoare]
c:240 [in Hoare]
c:256 [in Hoare]
c:26 [in HoareAsLogic]
c:29 [in Equiv]
c:31 [in Equiv]
c:33 [in HoareAsLogic]
c:35 [in Equiv]
c:36 [in Hoare]
c:37 [in Equiv]
c:39 [in HoareAsLogic]
c:42 [in Hoare]
c:44 [in HoareAsLogic]
c:46 [in Hoare]
c:48 [in HoareAsLogic]
c:50 [in HoareAsLogic]
c:53 [in HoareAsLogic]
c:55 [in HoareAsLogic]
c:56 [in Equiv]
c:59 [in HoareAsLogic]
c:61 [in HoareAsLogic]
c:63 [in Hoare2]
c:66 [in Hoare2]
c:67 [in Equiv]
c:69 [in HoareAsLogic]
c:71 [in Equiv]
c:72 [in HoareAsLogic]
c:74 [in Hoare]
c:77 [in Equiv]
c:78 [in Hoare]
c:83 [in Hoare]
c:87 [in Hoare]
c:91 [in Hoare]
c:95 [in Hoare]
c:96 [in Equiv]
c:99 [in Hoare]


D

dec:28 [in Hoare2]
dec:30 [in Hoare2]
dec:35 [in Hoare2]
dec:37 [in Hoare2]
dec:44 [in Hoare2]
dec:46 [in Hoare2]
d1:11 [in Hoare2]
d1:4 [in Hoare2]
d2:13 [in Hoare2]
d2:5 [in Hoare2]
d:15 [in HoareAsLogic]
d:17 [in Hoare2]
d:20 [in Hoare2]
d:21 [in Hoare2]
d:25 [in Hoare2]
d:32 [in Hoare2]
d:39 [in Hoare2]
d:42 [in Hoare2]


E

e':343 [in Smallstep]
e':344 [in Smallstep]
e:40 [in StlcProp]


F

f:27 [in Hoare]
f:31 [in Hoare]


G

Gamma':14 [in StlcProp]
Gamma':72 [in StlcProp]
Gamma':92 [in StlcProp]
Gamma:13 [in StlcProp]
Gamma:17 [in StlcProp]
Gamma:20 [in StlcProp]
Gamma:26 [in StlcProp]
Gamma:39 [in StlcProp]
Gamma:45 [in Stlc]
Gamma:48 [in Stlc]
Gamma:55 [in Stlc]
Gamma:58 [in Stlc]
Gamma:59 [in Stlc]
Gamma:64 [in Stlc]
Gamma:67 [in StlcProp]
Gamma:71 [in StlcProp]
Gamma:91 [in StlcProp]


I

i:191 [in Smallstep]
i:246 [in Smallstep]
i:250 [in Smallstep]
i:278 [in Smallstep]
i:282 [in Smallstep]
i:327 [in Smallstep]


M

m:331 [in Smallstep]
m:335 [in Smallstep]
m:339 [in Smallstep]
m:47 [in Hoare2]
m:49 [in Hoare2]
m:51 [in Hoare2]
m:53 [in Hoare2]
m:55 [in Hoare2]
m:56 [in Hoare2]
m:61 [in Hoare]
m:70 [in Hoare]


N

n:105 [in Hoare]
n:126 [in Hoare]
n:151 [in Smallstep]
n:153 [in Hoare]
n:154 [in Smallstep]
n:157 [in Smallstep]
n:162 [in Smallstep]
n:171 [in Hoare]
n:181 [in Hoare]
n:187 [in Smallstep]
n:251 [in Smallstep]
n:283 [in Smallstep]
n:31 [in Smallstep]
n:318 [in Smallstep]
n:324 [in Smallstep]
n:330 [in Smallstep]
n:334 [in Smallstep]
n:338 [in Smallstep]
n:48 [in Hoare2]
n:50 [in Hoare2]
n:55 [in Smallstep]
n:71 [in Smallstep]
n:74 [in Smallstep]
n:8 [in Smallstep]
n:86 [in Smallstep]
n:9 [in Hoare]


P

P':160 [in Hoare]
P':234 [in Hoare]
P':31 [in HoareAsLogic]
P':38 [in HoareAsLogic]
P':63 [in HoareAsLogic]
P':72 [in Hoare]
P':80 [in Hoare]
P':85 [in Hoare]
P':89 [in Hoare]
P':93 [in Hoare]
P':97 [in Hoare]
P1:10 [in Hoare2]
P2:12 [in Hoare2]
P:1 [in HoareAsLogic]
P:100 [in Hoare]
P:110 [in Hoare]
P:115 [in Hoare]
P:12 [in HoareAsLogic]
P:154 [in Hoare]
P:159 [in Hoare]
P:16 [in Hoare2]
P:168 [in Hoare]
P:17 [in HoareAsLogic]
P:19 [in Hoare2]
P:218 [in Hoare]
P:224 [in Hoare]
P:227 [in Hoare]
P:233 [in Hoare]
P:237 [in Hoare]
P:24 [in HoareAsLogic]
P:243 [in Hoare]
P:248 [in Hoare]
P:249 [in Hoare]
P:254 [in Hoare]
P:29 [in HoareAsLogic]
p:325 [in Smallstep]
p:328 [in Smallstep]
p:332 [in Smallstep]
p:336 [in Smallstep]
p:340 [in Smallstep]
P:35 [in Hoare]
P:36 [in HoareAsLogic]
P:38 [in Hoare2]
P:40 [in Hoare]
P:41 [in HoareAsLogic]
P:43 [in Hoare2]
P:44 [in Hoare]
P:48 [in Hoare]
P:49 [in Hoare]
P:49 [in HoareAsLogic]
P:5 [in Hoare]
P:52 [in HoareAsLogic]
p:52 [in Hoare2]
p:54 [in Hoare2]
P:56 [in Hoare]
P:63 [in Hoare]
P:64 [in HoareAsLogic]
P:67 [in Hoare]
P:71 [in Hoare]
P:71 [in HoareAsLogic]
P:75 [in Hoare]
P:79 [in Hoare]
P:8 [in Hoare]
P:8 [in HoareAsLogic]
P:84 [in Hoare]
P:88 [in Hoare]
P:92 [in Hoare]
P:96 [in Hoare]


Q

Q':102 [in Hoare]
Q':239 [in Hoare]
Q':32 [in HoareAsLogic]
Q':43 [in HoareAsLogic]
Q':77 [in Hoare]
Q':82 [in Hoare]
Q:101 [in Hoare]
Q:111 [in Hoare]
Q:118 [in Hoare]
Q:14 [in HoareAsLogic]
Q:14 [in Hoare2]
Q:156 [in Hoare]
Q:161 [in Hoare]
Q:164 [in Hoare]
Q:166 [in Hoare]
Q:18 [in HoareAsLogic]
Q:18 [in Hoare2]
Q:22 [in Hoare2]
Q:220 [in Hoare]
Q:226 [in Hoare]
Q:229 [in Hoare]
Q:230 [in Hoare]
Q:235 [in Hoare]
Q:238 [in Hoare]
Q:244 [in Hoare]
Q:250 [in Hoare]
Q:3 [in HoareAsLogic]
Q:3 [in Hoare2]
Q:30 [in HoareAsLogic]
Q:37 [in Hoare]
Q:37 [in HoareAsLogic]
Q:41 [in Hoare]
Q:42 [in HoareAsLogic]
Q:45 [in Hoare]
Q:50 [in Hoare]
Q:51 [in HoareAsLogic]
Q:54 [in HoareAsLogic]
Q:56 [in HoareAsLogic]
Q:58 [in Hoare]
Q:6 [in Hoare]
Q:60 [in HoareAsLogic]
Q:62 [in HoareAsLogic]
Q:65 [in HoareAsLogic]
Q:70 [in HoareAsLogic]
Q:73 [in Hoare]
Q:73 [in HoareAsLogic]
Q:76 [in Hoare]
Q:8 [in Hoare2]
Q:81 [in Hoare]
Q:86 [in Hoare]
Q:9 [in HoareAsLogic]
Q:90 [in Hoare]
Q:94 [in Hoare]
Q:98 [in Hoare]


R

R:122 [in Smallstep]
R:130 [in Smallstep]
R:134 [in Smallstep]
R:141 [in Smallstep]
R:16 [in HoareAsLogic]
r:187 [in Hoare]
r:192 [in Hoare]
r:197 [in Hoare]
r:206 [in Hoare]
r:222 [in Hoare]
R:245 [in Hoare]
R:25 [in Smallstep]
R:45 [in Smallstep]
R:51 [in Hoare]


S

stk:323 [in Smallstep]
stk:326 [in Smallstep]
stk:329 [in Smallstep]
stk:333 [in Smallstep]
stk:337 [in Smallstep]
st'':132 [in Hoare]
st'':148 [in Hoare]
st':10 [in Equiv]
st':131 [in Hoare]
st':134 [in Hoare]
st':139 [in Hoare]
st':14 [in Equiv]
st':147 [in Hoare]
st':158 [in Hoare]
st':186 [in Hoare]
st':205 [in Hoare]
st':223 [in Hoare]
st':241 [in Hoare]
st':242 [in Hoare]
st':255 [in Smallstep]
st':287 [in Smallstep]
st':309 [in Smallstep]
st':314 [in Smallstep]
st':316 [in Smallstep]
st':317 [in Smallstep]
st':33 [in Equiv]
st':39 [in Hoare]
st':5 [in HoareAsLogic]
st':74 [in Equiv]
st':80 [in Equiv]
st:1 [in Hoare]
st:107 [in Hoare]
st:109 [in Hoare]
st:11 [in Hoare]
st:12 [in Hoare]
st:123 [in Hoare]
st:124 [in Hoare]
st:13 [in Hoare]
st:13 [in Equiv]
st:130 [in Hoare]
st:133 [in Hoare]
st:138 [in Hoare]
st:14 [in Hoare]
st:144 [in Hoare]
st:146 [in Hoare]
st:15 [in Hoare]
st:151 [in Hoare]
st:157 [in Hoare]
st:16 [in Hoare]
st:165 [in Hoare]
st:17 [in Hoare]
st:170 [in Hoare]
st:178 [in Hoare]
st:179 [in Hoare]
st:18 [in Hoare]
st:185 [in Hoare]
st:188 [in Smallstep]
st:19 [in Hoare]
st:190 [in Hoare]
st:191 [in Hoare]
st:196 [in Hoare]
st:2 [in Hoare]
st:20 [in Hoare]
st:202 [in Hoare]
st:204 [in Hoare]
st:209 [in Hoare]
st:21 [in Hoare]
st:212 [in Hoare]
st:214 [in Hoare]
st:216 [in Hoare]
st:216 [in Smallstep]
st:22 [in Hoare]
st:22 [in HoareAsLogic]
st:221 [in Hoare]
st:23 [in Hoare]
st:23 [in HoareAsLogic]
st:24 [in Hoare]
st:245 [in Smallstep]
st:249 [in Smallstep]
st:25 [in Hoare]
st:252 [in Smallstep]
st:257 [in Smallstep]
st:259 [in Smallstep]
st:264 [in Smallstep]
st:267 [in Smallstep]
st:27 [in HoareAsLogic]
st:270 [in Smallstep]
st:277 [in Smallstep]
st:28 [in HoareAsLogic]
st:281 [in Smallstep]
st:284 [in Smallstep]
st:289 [in Smallstep]
st:29 [in Hoare]
st:291 [in Smallstep]
st:296 [in Smallstep]
st:299 [in Smallstep]
st:3 [in Hoare]
st:3 [in Equiv]
st:302 [in Smallstep]
st:305 [in Smallstep]
st:310 [in Smallstep]
st:315 [in Smallstep]
st:319 [in Smallstep]
st:32 [in Equiv]
st:320 [in Smallstep]
st:34 [in Hoare]
st:34 [in HoareAsLogic]
st:341 [in Smallstep]
st:342 [in Smallstep]
st:35 [in HoareAsLogic]
st:38 [in Hoare]
st:4 [in Hoare]
st:4 [in HoareAsLogic]
st:40 [in HoareAsLogic]
st:43 [in Hoare]
st:45 [in HoareAsLogic]
st:46 [in HoareAsLogic]
st:47 [in Hoare]
st:47 [in HoareAsLogic]
st:57 [in Hoare]
st:6 [in Equiv]
st:64 [in Hoare]
st:65 [in Hoare]
st:68 [in Hoare]
st:69 [in Hoare]
st:7 [in Hoare]
st:73 [in Equiv]
st:79 [in Equiv]
st:9 [in Equiv]
s':58 [in HoareAsLogic]
s:11 [in Stlc]
s:15 [in Stlc]
s:19 [in Stlc]
s:57 [in HoareAsLogic]
s:81 [in StlcProp]


T

t':100 [in StlcProp]
t':110 [in Smallstep]
t':12 [in StlcProp]
t':139 [in Smallstep]
t':143 [in Smallstep]
t':153 [in Smallstep]
t':156 [in Smallstep]
t':182 [in Smallstep]
t':184 [in Smallstep]
t':22 [in Stlc]
t':33 [in StlcProp]
t':37 [in StlcProp]
T':42 [in StlcProp]
t':43 [in Smallstep]
t':45 [in Types]
t':47 [in Smallstep]
t':47 [in Types]
t':50 [in Smallstep]
t':50 [in Types]
t':51 [in Smallstep]
t':53 [in Types]
t':56 [in Types]
t':59 [in Types]
T':68 [in StlcProp]
t':9 [in StlcProp]
t':96 [in StlcProp]
t1':106 [in Smallstep]
t1':118 [in Smallstep]
t1':145 [in Smallstep]
t1':168 [in Smallstep]
t1':178 [in Smallstep]
t1':18 [in Smallstep]
t1':20 [in Types]
t1':23 [in Types]
t1':26 [in Types]
t1':30 [in Stlc]
t1':37 [in Smallstep]
t1':40 [in Stlc]
t1':63 [in Smallstep]
t1':78 [in Smallstep]
t1':92 [in Smallstep]
t1:101 [in Smallstep]
t1:103 [in Smallstep]
t1:105 [in Smallstep]
t1:11 [in Types]
t1:113 [in Smallstep]
t1:115 [in Smallstep]
t1:117 [in Smallstep]
t1:13 [in Types]
t1:144 [in Smallstep]
t1:167 [in Smallstep]
t1:17 [in Smallstep]
t1:173 [in Smallstep]
t1:175 [in Smallstep]
t1:177 [in Smallstep]
t1:19 [in Types]
t1:22 [in Types]
t1:25 [in Types]
t1:27 [in Stlc]
t1:29 [in Stlc]
T1:3 [in StlcProp]
t1:34 [in Types]
t1:35 [in Stlc]
t1:36 [in Smallstep]
t1:37 [in Stlc]
t1:38 [in Types]
t1:39 [in Stlc]
t1:39 [in Types]
t1:40 [in Types]
t1:46 [in StlcProp]
T1:47 [in Stlc]
t1:48 [in StlcProp]
T1:50 [in Stlc]
T1:51 [in StlcProp]
t1:52 [in StlcProp]
t1:52 [in Stlc]
t1:53 [in StlcProp]
T1:53 [in Stlc]
t1:56 [in Smallstep]
t1:56 [in StlcProp]
t1:56 [in Stlc]
t1:59 [in StlcProp]
t1:60 [in Stlc]
t1:62 [in Smallstep]
T1:63 [in Stlc]
t1:77 [in Smallstep]
t1:9 [in Smallstep]
t1:9 [in Stlc]
t1:91 [in Smallstep]
t2':149 [in Smallstep]
t2':172 [in Smallstep]
t2':22 [in Smallstep]
t2':34 [in Stlc]
t2':41 [in Smallstep]
t2':67 [in Smallstep]
t2':82 [in Smallstep]
t2:10 [in Smallstep]
t2:102 [in Smallstep]
t2:104 [in Smallstep]
t2:107 [in Smallstep]
t2:114 [in Smallstep]
t2:116 [in Smallstep]
t2:119 [in Smallstep]
t2:12 [in Types]
t2:14 [in Types]
t2:146 [in Smallstep]
t2:148 [in Smallstep]
t2:169 [in Smallstep]
t2:17 [in Types]
t2:171 [in Smallstep]
t2:174 [in Smallstep]
t2:176 [in Smallstep]
t2:179 [in Smallstep]
t2:19 [in Smallstep]
t2:21 [in Smallstep]
T2:26 [in Stlc]
t2:31 [in Stlc]
t2:33 [in Stlc]
t2:35 [in Types]
t2:36 [in Stlc]
t2:38 [in Smallstep]
t2:38 [in Stlc]
T2:4 [in StlcProp]
t2:40 [in Smallstep]
t2:41 [in Stlc]
t2:47 [in StlcProp]
t2:49 [in StlcProp]
T2:51 [in Stlc]
t2:54 [in StlcProp]
T2:54 [in Stlc]
t2:57 [in StlcProp]
t2:57 [in Stlc]
t2:60 [in StlcProp]
t2:61 [in Stlc]
t2:64 [in Smallstep]
t2:66 [in Smallstep]
t2:79 [in Smallstep]
T2:8 [in Stlc]
t2:81 [in Smallstep]
t2:93 [in Smallstep]
t3:108 [in Smallstep]
t3:120 [in Smallstep]
t3:18 [in Types]
t3:180 [in Smallstep]
t3:36 [in Types]
t3:42 [in Stlc]
t3:55 [in StlcProp]
t3:58 [in StlcProp]
t3:61 [in StlcProp]
t3:62 [in Stlc]
t:1 [in StlcProp]
t:10 [in StlcProp]
t:109 [in Smallstep]
T:11 [in StlcProp]
t:12 [in Stlc]
t:138 [in Smallstep]
t:142 [in Smallstep]
t:15 [in StlcProp]
t:150 [in Smallstep]
t:152 [in Smallstep]
t:155 [in Smallstep]
T:16 [in StlcProp]
t:18 [in StlcProp]
t:181 [in Smallstep]
t:183 [in Smallstep]
T:19 [in StlcProp]
t:2 [in StlcProp]
t:21 [in Stlc]
t:23 [in StlcProp]
T:25 [in StlcProp]
t:27 [in Types]
t:28 [in Types]
t:29 [in StlcProp]
t:29 [in Types]
t:3 [in Smallstep]
T:31 [in StlcProp]
t:32 [in StlcProp]
T:34 [in StlcProp]
t:35 [in StlcProp]
t:36 [in StlcProp]
T:37 [in Types]
T:38 [in StlcProp]
T:41 [in StlcProp]
t:41 [in Types]
t:42 [in Smallstep]
t:42 [in Types]
t:43 [in Types]
T:44 [in Types]
t:46 [in Smallstep]
t:46 [in Types]
T:48 [in Types]
t:49 [in Smallstep]
t:49 [in Types]
T:51 [in Types]
t:52 [in Smallstep]
t:52 [in Types]
T:54 [in Types]
t:55 [in Types]
T:57 [in Types]
t:58 [in Types]
T:60 [in Types]
t:62 [in StlcProp]
t:65 [in StlcProp]
T:65 [in Stlc]
T:66 [in StlcProp]
T:66 [in Stlc]
t:69 [in StlcProp]
t:7 [in StlcProp]
t:7 [in Types]
T:70 [in StlcProp]
t:73 [in StlcProp]
T:74 [in StlcProp]
T:8 [in StlcProp]
t:8 [in Types]
t:82 [in StlcProp]
t:88 [in StlcProp]
t:93 [in StlcProp]
t:94 [in Smallstep]
T:94 [in StlcProp]
t:95 [in StlcProp]
T:97 [in StlcProp]
t:98 [in StlcProp]
T:99 [in StlcProp]


U

u:107 [in Equiv]
U:22 [in StlcProp]
U:28 [in StlcProp]
u:6 [in StlcProp]


V

v1:11 [in Smallstep]
v1:147 [in Smallstep]
v1:15 [in Smallstep]
v1:165 [in Smallstep]
v1:170 [in Smallstep]
v1:195 [in Smallstep]
v1:198 [in Smallstep]
v1:20 [in Smallstep]
v1:203 [in Smallstep]
v1:206 [in Smallstep]
v1:211 [in Smallstep]
v1:214 [in Smallstep]
v1:222 [in Smallstep]
v1:225 [in Smallstep]
v1:230 [in Smallstep]
v1:233 [in Smallstep]
v1:32 [in Stlc]
v1:34 [in Smallstep]
v1:39 [in Smallstep]
v1:60 [in Smallstep]
v1:65 [in Smallstep]
v1:75 [in Smallstep]
v1:80 [in Smallstep]
v1:89 [in Smallstep]
v2:12 [in Smallstep]
v2:16 [in Smallstep]
v2:166 [in Smallstep]
v2:199 [in Smallstep]
v2:207 [in Smallstep]
v2:215 [in Smallstep]
v2:226 [in Smallstep]
v2:234 [in Smallstep]
v2:28 [in Stlc]
v2:35 [in Smallstep]
v2:57 [in Smallstep]
v2:61 [in Smallstep]
v2:76 [in Smallstep]
v2:90 [in Smallstep]
V:10 [in HoareAsLogic]
v:21 [in Types]
v:24 [in StlcProp]
v:24 [in Types]
v:30 [in StlcProp]
v:48 [in Smallstep]
v:68 [in Smallstep]
v:83 [in Smallstep]


X

x1:111 [in Equiv]
x2:112 [in Equiv]
x:10 [in Stlc]
x:106 [in Equiv]
X:121 [in Smallstep]
x:125 [in Smallstep]
x:126 [in Smallstep]
x:127 [in Hoare]
X:129 [in Smallstep]
x:131 [in Smallstep]
X:133 [in Smallstep]
x:135 [in Smallstep]
X:140 [in Smallstep]
x:152 [in Hoare]
x:16 [in Stlc]
X:163 [in Hoare]
X:167 [in Hoare]
X:169 [in Hoare]
x:182 [in Hoare]
x:20 [in Stlc]
x:21 [in StlcProp]
X:23 [in Smallstep]
X:231 [in Hoare]
X:24 [in Smallstep]
x:25 [in Stlc]
X:26 [in Hoare]
x:26 [in Smallstep]
x:27 [in StlcProp]
x:28 [in Hoare]
X:30 [in Hoare]
x:32 [in Hoare]
x:41 [in Equiv]
X:42 [in Equiv]
x:43 [in StlcProp]
X:44 [in Smallstep]
x:46 [in Stlc]
x:49 [in Stlc]
x:5 [in StlcProp]
X:54 [in Hoare]
X:59 [in Hoare]
X:6 [in Hoare2]
x:62 [in Equiv]
x:63 [in StlcProp]
x:64 [in StlcProp]
x:7 [in Stlc]
x:75 [in StlcProp]
x:80 [in StlcProp]


Y

y1:27 [in Smallstep]
y2:28 [in Smallstep]
y:127 [in Smallstep]
y:132 [in Smallstep]
y:136 [in Smallstep]
y:33 [in Hoare]
y:50 [in StlcProp]


Z

z:128 [in Smallstep]
z:137 [in Smallstep]


Module Index

C

CImp [in Smallstep]
Combined [in Smallstep]


E

ExamplePrettyAssertions [in Hoare]
ExAssertions [in Hoare]


H

Himp [in Hoare]
HoareAssertAssume [in Hoare]


S

SimpleArith1 [in Smallstep]
SimpleArith2 [in Smallstep]
SimpleArith3 [in Smallstep]
STLC [in Stlc]
STLCArith [in StlcProp]
STLCProp [in StlcProp]


T

Temp1 [in Smallstep]
Temp2 [in Smallstep]
Temp3 [in Smallstep]
Temp4 [in Smallstep]
Temp4.Temp5 [in Smallstep]
TM [in Types]


Library Index

B

Bib


E

Equiv


H

Hoare
HoareAsLogic
Hoare2


P

Postscript
Preface


S

Smallstep
Stlc
StlcProp


T

Types


Lemma Index

A

aequiv_example [in Equiv]
always_loop_hoare [in Hoare]
assign_aequiv [in Equiv]


B

bequiv_example [in Equiv]
bexp_eval_false [in Hoare]


C

CAsgn_congruence [in Equiv]
CIf_congruence [in Equiv]
CImp.par_body_n__Sn [in Smallstep]
Combined.combined_strong_progress [in Smallstep]
Combined.combined_step_deterministic [in Smallstep]
compiler_is_correct [in Smallstep]
CSeq_congruence [in Equiv]
CWhile_congruence [in Equiv]


D

dec_while_correct [in Hoare2]


E

eval__multistep [in Smallstep]


H

Himp.havoc_post [in Hoare]
Himp.hoare_havoc [in Hoare]
Himp.hoare_consequence_pre [in Hoare]
HoareAssertAssume.assert_implies_assume [in Hoare]
HoareAssertAssume.assert_assume_differ [in Hoare]
HoareAssertAssume.hoare_while [in Hoare]
HoareAssertAssume.hoare_if [in Hoare]
HoareAssertAssume.hoare_skip [in Hoare]
HoareAssertAssume.hoare_seq [in Hoare]
HoareAssertAssume.hoare_consequence_post [in Hoare]
HoareAssertAssume.hoare_consequence_pre [in Hoare]
HoareAssertAssume.hoare_asgn [in Hoare]
hoare_while [in Hoare]
hoare_if [in Hoare]
hoare_consequence_post' [in Hoare]
hoare_consequence_pre'''' [in Hoare]
hoare_consequence_pre''' [in Hoare]
hoare_consequence_pre'' [in Hoare]
hoare_consequence_pre' [in Hoare]
hoare_consequence [in Hoare]
hoare_consequence_post [in Hoare]
hoare_consequence_pre [in Hoare]
hoare_asgn_fwd_exists [in Hoare]
hoare_asgn_fwd [in Hoare]
hoare_asgn [in Hoare]
hoare_seq [in Hoare]
hoare_skip [in Hoare]
hoare_pre_false [in Hoare]
hoare_post_true [in Hoare]
hoare_complete [in HoareAsLogic]
hoare_sound [in HoareAsLogic]
H_Consequence_post [in HoareAsLogic]
H_Consequence_pre [in HoareAsLogic]


I

identity_assignment [in Equiv]
if_minus_plus [in Hoare]
if_false [in Equiv]
if_true [in Equiv]
if_true_simple [in Equiv]
if_minus_plus_correct [in Hoare2]
inequiv_exercise [in Equiv]


L

loop_unrolling [in Equiv]


M

minimum_correct [in Hoare2]
multistep__eval [in Smallstep]
multistep_congr_2 [in Smallstep]
multistep_congr_1 [in Smallstep]
multi_trans [in Smallstep]
multi_R [in Smallstep]


N

nf_same_as_value [in Smallstep]
nf_is_value [in Smallstep]
normalize_ex [in Smallstep]


P

positive_difference_correct [in Hoare2]
provable_false_pre [in HoareAsLogic]
provable_true_post [in HoareAsLogic]


R

reduce_to_zero_correct''' [in Hoare2]
reduce_to_zero_correct' [in Hoare2]
refl_cequiv [in Equiv]
refl_bequiv [in Equiv]
refl_aequiv [in Equiv]


S

seq_assoc [in Equiv]
SimpleArith2.step_deterministic [in Smallstep]
SimpleArith3.step_deterministic_alt [in Smallstep]
skip_right [in Equiv]
skip_left [in Equiv]
slow_assignment [in Hoare2]
stack_step_deterministic [in Smallstep]
step__eval [in Smallstep]
step_normalizing [in Smallstep]
step_deterministic [in Smallstep]
STLCArith.preservation [in StlcProp]
STLCArith.progress [in StlcProp]
STLCArith.weakening [in StlcProp]
STLCProp.canonical_forms_fun [in StlcProp]
STLCProp.canonical_forms_bool [in StlcProp]
STLCProp.context_invariance [in StlcProp]
STLCProp.free_in_context [in StlcProp]
STLCProp.preservation [in StlcProp]
STLCProp.progress [in StlcProp]
STLCProp.progress' [in StlcProp]
STLCProp.substitution_preserves_typing_from_typing_ind [in StlcProp]
STLCProp.substitution_preserves_typing [in StlcProp]
STLCProp.typable_empty__closed [in StlcProp]
STLCProp.type_soundness [in StlcProp]
STLCProp.unique_types [in StlcProp]
STLCProp.weakening [in StlcProp]
STLCProp.weakening_empty [in StlcProp]
STLC.step_example5_with_normalize [in Stlc]
STLC.step_example5 [in Stlc]
STLC.step_example4' [in Stlc]
STLC.step_example3' [in Stlc]
STLC.step_example2' [in Stlc]
STLC.step_example1' [in Stlc]
STLC.step_example4 [in Stlc]
STLC.step_example3 [in Stlc]
STLC.step_example2 [in Stlc]
STLC.step_example1 [in Stlc]
STLC.substi_correct [in Stlc]
strong_progress [in Smallstep]
subst_inequiv [in Equiv]
subtract_slowly_outer_triple_valid [in Hoare2]
swap_exercise [in Hoare]
swap_if_branches [in Equiv]
swap_correct [in Hoare2]
sym_cequiv [in Equiv]
sym_bequiv [in Equiv]
sym_aequiv [in Equiv]


T

Temp1.value_not_same_as_normal_form [in Smallstep]
Temp2.value_not_same_as_normal_form [in Smallstep]
Temp3.value_not_same_as_normal_form [in Smallstep]
Temp4.step_deterministic [in Smallstep]
Temp4.strong_progress_bool [in Smallstep]
test_multistep_4 [in Smallstep]
test_multistep_1' [in Smallstep]
test_multistep_1 [in Smallstep]
TM.bool_canonical [in Types]
TM.nat_canonical [in Types]
TM.preservation [in Types]
TM.preservation' [in Types]
TM.progress [in Types]
TM.soundness [in Types]
TM.step_deterministic [in Types]
TM.subject_expansion [in Types]
TM.value_is_nf [in Types]
trans_cequiv [in Equiv]
trans_bequiv [in Equiv]
trans_aequiv [in Equiv]
two_loops [in Hoare2]


V

value_is_nf [in Smallstep]
verification_correct_dec [in Hoare2]
verification_correct [in Hoare2]


W

while_true [in Equiv]
while_true_nonterm [in Equiv]
while_false [in Equiv]
wp_invariant [in HoareAsLogic]
wp_seq [in HoareAsLogic]
wp_is_weakest [in HoareAsLogic]
wp_is_precondition [in HoareAsLogic]


Constructor Index

A

AS_Mult [in Smallstep]
AS_Mult2 [in Smallstep]
AS_Mult1 [in Smallstep]
AS_Minus [in Smallstep]
AS_Minus2 [in Smallstep]
AS_Minus1 [in Smallstep]
AS_Plus [in Smallstep]
AS_Plus2 [in Smallstep]
AS_Plus1 [in Smallstep]
AS_Id [in Smallstep]
av_num [in Smallstep]


B

BS_AndTrueFalse [in Smallstep]
BS_AndTrueTrue [in Smallstep]
BS_AndFalse [in Smallstep]
BS_AndTrueStep [in Smallstep]
BS_AndStep [in Smallstep]
BS_NotFalse [in Smallstep]
BS_NotTrue [in Smallstep]
BS_NotStep [in Smallstep]
BS_LtEq [in Smallstep]
BS_LtEq2 [in Smallstep]
BS_LtEq1 [in Smallstep]
BS_Eq [in Smallstep]
BS_Eq2 [in Smallstep]
BS_Eq1 [in Smallstep]


C

C [in Smallstep]
CImp.CAsgn [in Smallstep]
CImp.CIf [in Smallstep]
CImp.CPar [in Smallstep]
CImp.CSeq [in Smallstep]
CImp.CSkip [in Smallstep]
CImp.CS_ParDone [in Smallstep]
CImp.CS_Par2 [in Smallstep]
CImp.CS_Par1 [in Smallstep]
CImp.CS_While [in Smallstep]
CImp.CS_IfFalse [in Smallstep]
CImp.CS_IfTrue [in Smallstep]
CImp.CS_IfStep [in Smallstep]
CImp.CS_SeqFinish [in Smallstep]
CImp.CS_SeqStep [in Smallstep]
CImp.CS_Asgn [in Smallstep]
CImp.CS_AsgnStep [in Smallstep]
CImp.CWhile [in Smallstep]
Combined.C [in Smallstep]
Combined.fls [in Smallstep]
Combined.P [in Smallstep]
Combined.ST_If [in Smallstep]
Combined.ST_IfFalse [in Smallstep]
Combined.ST_IfTrue [in Smallstep]
Combined.ST_Plus2 [in Smallstep]
Combined.ST_Plus1 [in Smallstep]
Combined.ST_PlusConstConst [in Smallstep]
Combined.test [in Smallstep]
Combined.tru [in Smallstep]
Combined.v_fls [in Smallstep]
Combined.v_tru [in Smallstep]
Combined.v_const [in Smallstep]
CS_While [in Smallstep]
CS_IfFalse [in Smallstep]
CS_IfTrue [in Smallstep]
CS_IfStep [in Smallstep]
CS_SeqFinish [in Smallstep]
CS_SeqStep [in Smallstep]
CS_Asgn [in Smallstep]
CS_AsgnStep [in Smallstep]


D

DCAsgn [in Hoare2]
DCIf [in Hoare2]
DCPost [in Hoare2]
DCPre [in Hoare2]
DCSeq [in Hoare2]
DCSkip [in Hoare2]
DCWhile [in Hoare2]
Decorated [in Hoare2]


E

E_Plus [in Smallstep]
E_Const [in Smallstep]


H

Himp.CAsgn [in Hoare]
Himp.CHavoc [in Hoare]
Himp.CIf [in Hoare]
Himp.CSeq [in Hoare]
Himp.CSkip [in Hoare]
Himp.CWhile [in Hoare]
Himp.E_Havoc [in Hoare]
Himp.E_WhileTrue [in Hoare]
Himp.E_WhileFalse [in Hoare]
Himp.E_IfFalse [in Hoare]
Himp.E_IfTrue [in Hoare]
Himp.E_Seq [in Hoare]
Himp.E_Asgn [in Hoare]
Himp.E_Skip [in Hoare]
HoareAssertAssume.CAsgn [in Hoare]
HoareAssertAssume.CAssert [in Hoare]
HoareAssertAssume.CAssume [in Hoare]
HoareAssertAssume.CIf [in Hoare]
HoareAssertAssume.CSeq [in Hoare]
HoareAssertAssume.CSkip [in Hoare]
HoareAssertAssume.CWhile [in Hoare]
HoareAssertAssume.E_Assume [in Hoare]
HoareAssertAssume.E_AssertFalse [in Hoare]
HoareAssertAssume.E_AssertTrue [in Hoare]
HoareAssertAssume.E_WhileTrueError [in Hoare]
HoareAssertAssume.E_WhileTrueNormal [in Hoare]
HoareAssertAssume.E_WhileFalse [in Hoare]
HoareAssertAssume.E_IfFalse [in Hoare]
HoareAssertAssume.E_IfTrue [in Hoare]
HoareAssertAssume.E_SeqError [in Hoare]
HoareAssertAssume.E_SeqNormal [in Hoare]
HoareAssertAssume.E_Asgn [in Hoare]
HoareAssertAssume.E_Skip [in Hoare]
HoareAssertAssume.RError [in Hoare]
HoareAssertAssume.RNormal [in Hoare]
H_Consequence [in HoareAsLogic]
H_While [in HoareAsLogic]
H_If [in HoareAsLogic]
H_Seq [in HoareAsLogic]
H_Asgn [in HoareAsLogic]
H_Skip [in HoareAsLogic]


M

multi_step [in Smallstep]
multi_refl [in Smallstep]


P

P [in Smallstep]


S

SimpleArith1.ST_Plus2 [in Smallstep]
SimpleArith1.ST_Plus1 [in Smallstep]
SimpleArith1.ST_PlusConstConst [in Smallstep]
SS_Mult [in Smallstep]
SS_Minus [in Smallstep]
SS_Plus [in Smallstep]
SS_Load [in Smallstep]
SS_Push [in Smallstep]
STLCArith.tm_if0 [in StlcProp]
STLCArith.tm_mult [in StlcProp]
STLCArith.tm_pred [in StlcProp]
STLCArith.tm_succ [in StlcProp]
STLCArith.tm_const [in StlcProp]
STLCArith.tm_abs [in StlcProp]
STLCArith.tm_app [in StlcProp]
STLCArith.tm_var [in StlcProp]
STLCArith.Ty_Nat [in StlcProp]
STLCArith.Ty_Arrow [in StlcProp]
STLCProp.afi_if3 [in StlcProp]
STLCProp.afi_if2 [in StlcProp]
STLCProp.afi_if1 [in StlcProp]
STLCProp.afi_abs [in StlcProp]
STLCProp.afi_app2 [in StlcProp]
STLCProp.afi_app1 [in StlcProp]
STLCProp.afi_var [in StlcProp]
STLC.ST_If [in Stlc]
STLC.ST_IfFalse [in Stlc]
STLC.ST_IfTrue [in Stlc]
STLC.ST_App2 [in Stlc]
STLC.ST_App1 [in Stlc]
STLC.ST_AppAbs [in Stlc]
STLC.s_var1 [in Stlc]
STLC.tm_if [in Stlc]
STLC.tm_false [in Stlc]
STLC.tm_true [in Stlc]
STLC.tm_abs [in Stlc]
STLC.tm_app [in Stlc]
STLC.tm_var [in Stlc]
STLC.Ty_Arrow [in Stlc]
STLC.Ty_Bool [in Stlc]
STLC.T_If [in Stlc]
STLC.T_False [in Stlc]
STLC.T_True [in Stlc]
STLC.T_App [in Stlc]
STLC.T_Abs [in Stlc]
STLC.T_Var [in Stlc]
STLC.v_false [in Stlc]
STLC.v_true [in Stlc]
STLC.v_abs [in Stlc]
ST_Plus2 [in Smallstep]
ST_Plus1 [in Smallstep]
ST_PlusConstConst [in Smallstep]


T

Temp1.ST_Plus2 [in Smallstep]
Temp1.ST_Plus1 [in Smallstep]
Temp1.ST_PlusConstConst [in Smallstep]
Temp1.v_funny [in Smallstep]
Temp1.v_const [in Smallstep]
Temp2.ST_Plus2 [in Smallstep]
Temp2.ST_Plus1 [in Smallstep]
Temp2.ST_PlusConstConst [in Smallstep]
Temp2.ST_Funny [in Smallstep]
Temp2.v_const [in Smallstep]
Temp3.ST_Plus1 [in Smallstep]
Temp3.ST_PlusConstConst [in Smallstep]
Temp3.v_const [in Smallstep]
Temp4.fls [in Smallstep]
Temp4.ST_If [in Smallstep]
Temp4.ST_IfFalse [in Smallstep]
Temp4.ST_IfTrue [in Smallstep]
Temp4.Temp5.ST_If [in Smallstep]
Temp4.Temp5.ST_IfFalse [in Smallstep]
Temp4.Temp5.ST_IfTrue [in Smallstep]
Temp4.test [in Smallstep]
Temp4.tru [in Smallstep]
Temp4.v_fls [in Smallstep]
Temp4.v_tru [in Smallstep]
TM.Bool [in Types]
TM.bv_false [in Types]
TM.bv_True [in Types]
TM.fls [in Types]
TM.iszro [in Types]
TM.ite [in Types]
TM.Nat [in Types]
TM.nv_succ [in Types]
TM.nv_0 [in Types]
TM.prd [in Types]
TM.scc [in Types]
TM.ST_Iszero [in Types]
TM.ST_IszeroSucc [in Types]
TM.ST_Iszero0 [in Types]
TM.ST_Pred [in Types]
TM.ST_PredSucc [in Types]
TM.ST_Pred0 [in Types]
TM.ST_Succ [in Types]
TM.ST_If [in Types]
TM.ST_IfFalse [in Types]
TM.ST_IfTrue [in Types]
TM.tru [in Types]
TM.T_Iszero [in Types]
TM.T_Pred [in Types]
TM.T_Succ [in Types]
TM.T_0 [in Types]
TM.T_If [in Types]
TM.T_False [in Types]
TM.T_True [in Types]
TM.zro [in Types]


V

v_const [in Smallstep]


Inductive Index

A

astep [in Smallstep]
aval [in Smallstep]


B

bstep [in Smallstep]


C

CImp.com [in Smallstep]
CImp.cstep [in Smallstep]
Combined.step [in Smallstep]
Combined.tm [in Smallstep]
Combined.value [in Smallstep]
cstep [in Smallstep]


D

dcom [in Hoare2]
decorated [in Hoare2]
derivable [in HoareAsLogic]


E

eval [in Smallstep]


H

Himp.ceval [in Hoare]
Himp.com [in Hoare]
HoareAssertAssume.ceval [in Hoare]
HoareAssertAssume.com [in Hoare]
HoareAssertAssume.result [in Hoare]


M

multi [in Smallstep]


S

SimpleArith1.step [in Smallstep]
stack_step [in Smallstep]
step [in Smallstep]
STLCArith.has_type [in StlcProp]
STLCArith.step [in StlcProp]
STLCArith.tm [in StlcProp]
STLCArith.ty [in StlcProp]
STLCArith.value [in StlcProp]
STLCProp.appears_free_in [in StlcProp]
STLC.has_type [in Stlc]
STLC.step [in Stlc]
STLC.substi [in Stlc]
STLC.tm [in Stlc]
STLC.ty [in Stlc]
STLC.value [in Stlc]


T

Temp1.step [in Smallstep]
Temp1.value [in Smallstep]
Temp2.step [in Smallstep]
Temp2.value [in Smallstep]
Temp3.step [in Smallstep]
Temp3.value [in Smallstep]
Temp4.step [in Smallstep]
Temp4.Temp5.step [in Smallstep]
Temp4.tm [in Smallstep]
Temp4.value [in Smallstep]
tm [in Smallstep]
TM.bvalue [in Types]
TM.has_type [in Types]
TM.nvalue [in Types]
TM.step [in Types]
TM.tm [in Types]
TM.ty [in Types]


V

value [in Smallstep]


Abbreviation Index

A

assert [in Hoare]


M

mkAexp [in Hoare]


S

STLCArith.multistep [in StlcProp]
STLC.idB [in Stlc]
STLC.idBB [in Stlc]
STLC.idBBBB [in Stlc]
STLC.k [in Stlc]
STLC.multistep [in Stlc]
STLC.notB [in Stlc]


T

TM.step_normal_form [in Types]


Definition Index

A

aequiv [in Equiv]
Aexp [in Hoare]
Aexp_of_aexp [in Hoare]
Aexp_of_nat [in Hoare]
ap [in Hoare]
ap2 [in Hoare]
Assertion [in Hoare]
assert_of_Prop [in Hoare]
assert_implies [in Hoare]
assn_sub_ex2' [in Hoare]
assn_sub_ex1' [in Hoare]
assn_sub_example2'' [in Hoare]
assn_sub_example2' [in Hoare]
assn_sub_example2 [in Hoare]
assn_sub_example [in Hoare]
assn_sub [in Hoare]
atrans_sound [in Equiv]


B

bassn [in Hoare]
bequiv [in Equiv]
btrans_sound [in Equiv]


C

cequiv [in Equiv]
CImp.cmultistep [in Smallstep]
CImp.par_loop_example_2 [in Smallstep]
CImp.par_loop_example_0 [in Smallstep]
CImp.par_loop [in Smallstep]
compiler_is_correct_statement [in Smallstep]
congruence_example [in Equiv]
ctrans_sound [in Equiv]


D

dec_while_triple_correct [in Hoare2]
dec_while [in Hoare2]
dec0 [in Hoare2]
dec1 [in Hoare2]
deterministic [in Smallstep]


E

evalF [in Smallstep]
ExamplePrettyAssertions.assn1 [in Hoare]
ExamplePrettyAssertions.assn2 [in Hoare]
ExamplePrettyAssertions.assn3 [in Hoare]
ExamplePrettyAssertions.assn4 [in Hoare]
ExamplePrettyAssertions.ex1 [in Hoare]
ExamplePrettyAssertions.ex2 [in Hoare]
ExamplePrettyAssertions.ex3 [in Hoare]
ExAssertions.assn1 [in Hoare]
ExAssertions.assn2 [in Hoare]
ExAssertions.assn3 [in Hoare]
ExAssertions.assn4 [in Hoare]
extract [in Hoare2]
extract_while_ex [in Hoare2]
extract_dec [in Hoare2]


F

FILL_IN_HERE [in Smallstep]
FILL_IN_HERE [in Hoare2]
fold_com_ex1 [in Equiv]
fold_constants_com [in Equiv]
fold_bexp_ex2 [in Equiv]
fold_bexp_ex1 [in Equiv]
fold_constants_bexp [in Equiv]
fold_aexp_ex2 [in Equiv]
fold_aexp_ex1 [in Equiv]
fold_constants_aexp [in Equiv]


H

Himp.havoc_pre [in Hoare]
Himp.hoare_triple [in Hoare]
HoareAssertAssume.assert_assume_example [in Hoare]
HoareAssertAssume.hoare_triple [in Hoare]
hoare_asgn_example4 [in Hoare]
hoare_asgn_example3 [in Hoare]
hoare_asgn_example1''' [in Hoare]
hoare_asgn_example1'' [in Hoare]
hoare_asgn_example1' [in Hoare]
hoare_asgn_example1 [in Hoare]
hoare_triple [in Hoare]


I

if_example''' [in Hoare]
if_example'' [in Hoare]
if_example [in Hoare]
if_minus_plus_dec [in Hoare2]


M

minimum_dec [in Hoare2]


N

normalizing [in Smallstep]
normal_form_of [in Smallstep]
normal_form [in Smallstep]


O

outer_triple_valid [in Hoare2]


P

positive_difference_dec [in Hoare2]
post [in Hoare2]
post_dec_while [in Hoare2]
post_dec [in Hoare2]
pre_dec_while [in Hoare2]
pre_dec [in Hoare2]
prog [in Smallstep]


R

reduce_to_zero' [in Hoare2]
refines [in Equiv]
relation [in Smallstep]


S

sample_proof [in HoareAsLogic]
SimpleArith1.test_step_2 [in Smallstep]
SimpleArith1.test_step_1 [in Smallstep]
slow_assignment_dec [in Hoare2]
stack [in Smallstep]
stack_multistep [in Smallstep]
step_example1''' [in Smallstep]
step_example1'' [in Smallstep]
step_example1' [in Smallstep]
step_example1 [in Smallstep]
step_normal_form [in Smallstep]
STLCArith.context [in StlcProp]
STLCArith.Nat_typing_example [in StlcProp]
STLCArith.Nat_step_example [in StlcProp]
STLCArith.subst [in StlcProp]
STLCProp.closed [in StlcProp]
STLCProp.stuck [in StlcProp]
STLC.context [in Stlc]
STLC.subst [in Stlc]
STLC.typing_nonexample_1 [in Stlc]
STLC.typing_example_3 [in Stlc]
STLC.typing_example_2 [in Stlc]
STLC.typing_example_1' [in Stlc]
STLC.typing_example_1 [in Stlc]
STLC.x [in Stlc]
STLC.y [in Stlc]
STLC.z [in Stlc]
subst_equiv_property [in Equiv]
subst_aexp_ex [in Equiv]
subst_aexp [in Equiv]
subtract_slowly_dec [in Hoare2]
swap_program [in Hoare]
swap_dec [in Hoare2]


T

Temp4.Temp5.bool_step_prop4_holds [in Smallstep]
Temp4.Temp5.bool_step_prop4 [in Smallstep]
TM.has_type_not [in Types]
TM.has_type_1 [in Types]
TM.multistep [in Types]
TM.some_term_is_stuck [in Types]
TM.stuck [in Types]
TM.value [in Types]
two_loops_dec [in Hoare2]


V

valid [in HoareAsLogic]
vc_dec_while [in Hoare2]
verification_conditions_dec [in Hoare2]
verification_conditions [in Hoare2]


W

while_example [in Hoare]
wp [in HoareAsLogic]


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1667 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (111 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (952 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (18 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (151 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (226 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (52 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (10 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (136 entries)
This page has been generated by coqdoc