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.manual_grade_for_properties_of_altered_step [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_3 [lemma, in Smallstep]
test_multistep_2 [lemma, in Smallstep]
test_multistep_1' [lemma, in Smallstep]
test_multistep_1 [lemma, in Smallstep]
test_optimize_0plus [definition, in Equiv]
test_pe_bexp2 [definition, in PE]
test_pe_bexp1 [definition, in PE]
test_pe_update [definition, in PE]
test_pe_aexp1 [definition, in PE]
text_pe_aexp2 [definition, in PE]
Tguard:21 [binder, in Typechecking]
Tguard:55 [binder, in Typechecking]
Ti:100 [binder, in Records]
Ti:102 [binder, in RecordSub]
Ti:109 [binder, in Records]
ti:110 [binder, in Records]
Ti:128 [binder, in RecordSub]
Ti:148 [binder, in RecordSub]
Ti:88 [binder, in Records]
Ti:98 [binder, in RecordSub]
TL:201 [binder, in Sub]
TL:205 [binder, in Sub]
TL:209 [binder, in Sub]
TL:213 [binder, in Sub]
tm [inductive, in Smallstep]
TM [module, in Types]
tm [inductive, in Norm]
tm_snd [constructor, in Norm]
tm_fst [constructor, in Norm]
tm_pair [constructor, in Norm]
tm_if [constructor, in Norm]
tm_false [constructor, in Norm]
tm_true [constructor, in Norm]
tm_abs [constructor, in Norm]
tm_app [constructor, in Norm]
tm_var [constructor, in Norm]
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.manual_grade_for_prog_pres_bigstep [definition, in Types]
TM.manual_grade_for_remove_pred0 [definition, in Types]
TM.manual_grade_for_variation2 [definition, in Types]
TM.manual_grade_for_variation1 [definition, in Types]
TM.manual_grade_for_finish_preservation_informal [definition, in Types]
TM.manual_grade_for_finish_progress_informal [definition, 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.succ_hastype_nat__hastype_nat [definition, 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]
transitivity_workaround_2 [lemma, in UseAuto]
transitivity_workaround_1 [lemma, in UseAuto]
transitivity_bad_hint_1 [lemma, in UseAuto]
trans_cequiv [lemma, in Equiv]
trans_bequiv [lemma, in Equiv]
trans_aequiv [lemma, in Equiv]
tr':102 [binder, in Records]
tr':144 [binder, in RecordSub]
tr2':68 [binder, in Records]
tr2':69 [binder, in RecordSub]
tr2:64 [binder, in Records]
tr2:65 [binder, in RecordSub]
tr2:67 [binder, in Records]
tr2:68 [binder, in RecordSub]
Tr2:88 [binder, in RecordSub]
Tr3:93 [binder, in RecordSub]
tr:101 [binder, in Records]
tr:138 [binder, in RecordSub]
Tr:139 [binder, in RecordSub]
tr:143 [binder, in RecordSub]
Tr:37 [binder, in RecordSub]
tr:40 [binder, in Records]
tr:41 [binder, in RecordSub]
tr:58 [binder, in Records]
tr:59 [binder, in RecordSub]
Tr:70 [binder, in Records]
Tr:89 [binder, in Records]
tr:93 [binder, in Records]
Tr:94 [binder, in Records]
TS:200 [binder, in Sub]
TS:203 [binder, in Sub]
TS:207 [binder, in Sub]
TS:211 [binder, in Sub]
TS:221 [binder, in Sub]
two_loops [lemma, in Hoare2]
two_loops_dec [definition, in Hoare2]
ty [inductive, in Norm]
typ [axiom, in UseAuto]
typable_empty__closed [lemma, in Norm]
TypecheckerExtensions [module, in Typechecking]
TypecheckerExtensions.eqb_ty__eq [lemma, in Typechecking]
TypecheckerExtensions.eqb_ty_refl [lemma, in Typechecking]
TypecheckerExtensions.eqb_ty [definition, in Typechecking]
TypecheckerExtensions.manual_grade_for_type_check_defn [definition, in Typechecking]
TypecheckerExtensions.type_checking_complete [lemma, in Typechecking]
TypecheckerExtensions.type_checking_sound [lemma, in Typechecking]
TypecheckerExtensions.type_check [definition, in Typechecking]
Typechecking [library]
Types [library]
Ty_Prod [constructor, in Norm]
Ty_Arrow [constructor, in Norm]
Ty_Bool [constructor, in Norm]
T_Snd [constructor, in Norm]
T_Fst [constructor, in Norm]
T_Pair [constructor, in Norm]
T_If [constructor, in Norm]
T_False [constructor, in Norm]
T_True [constructor, in Norm]
T_App [constructor, in Norm]
T_Abs [constructor, in Norm]
T_Var [constructor, in Norm]
t':101 [binder, in Norm]
t':103 [binder, in StlcProp]
t':110 [binder, in Smallstep]
t':112 [binder, in UseAuto]
t':113 [binder, in Records]
t':12 [binder, in StlcProp]
t':127 [binder, in UseAuto]
t':128 [binder, in Records]
t':131 [binder, in Sub]
t':136 [binder, in UseAuto]
t':139 [binder, in Smallstep]
t':143 [binder, in Smallstep]
T':151 [binder, in Norm]
t':153 [binder, in Smallstep]
t':155 [binder, in Norm]
t':156 [binder, in Smallstep]
t':159 [binder, in RecordSub]
t':167 [binder, in Norm]
t':170 [binder, in MoreStlc]
t':170 [binder, in Norm]
t':172 [binder, in References]
t':173 [binder, in Norm]
t':176 [binder, in Norm]
t':179 [binder, in Norm]
t':184 [binder, in Smallstep]
t':184 [binder, in References]
t':185 [binder, in RecordSub]
t':185 [binder, in MoreStlc]
t':186 [binder, in Smallstep]
t':203 [binder, in References]
t':207 [binder, in Norm]
t':210 [binder, in Norm]
t':214 [binder, in Norm]
t':22 [binder, in Stlc]
t':243 [binder, in References]
t':252 [binder, in References]
t':264 [binder, in Norm]
t':33 [binder, in StlcProp]
t':36 [binder, in StlcProp]
t':40 [binder, in StlcProp]
t':43 [binder, in Smallstep]
T':45 [binder, in StlcProp]
t':46 [binder, in Types]
t':47 [binder, in Smallstep]
t':48 [binder, in Types]
t':50 [binder, in Smallstep]
t':51 [binder, in Smallstep]
t':51 [binder, in Types]
t':54 [binder, in Types]
t':57 [binder, in Types]
t':60 [binder, in Types]
T':71 [binder, in StlcProp]
t':87 [binder, in UseAuto]
t':87 [binder, in Typechecking]
t':9 [binder, in StlcProp]
t':90 [binder, in UseAuto]
t':90 [binder, in Typechecking]
t':94 [binder, in UseAuto]
t':94 [binder, in Sub]
t':97 [binder, in UseAuto]
t':99 [binder, in StlcProp]
t0':44 [binder, in Norm]
t0':48 [binder, in Norm]
t0':67 [binder, in MoreStlc]
t0:117 [binder, in Norm]
t0:121 [binder, in Norm]
t0:125 [binder, in Norm]
T0:135 [binder, in MoreStlc]
t0:145 [binder, in MoreStlc]
T0:154 [binder, in References]
t0:43 [binder, in Norm]
t0:47 [binder, in Norm]
T0:59 [binder, in Typechecking]
t0:66 [binder, in MoreStlc]
t0:80 [binder, in Norm]
t0:84 [binder, in Norm]
t1':100 [binder, in References]
t1':106 [binder, in Smallstep]
t1':106 [binder, in References]
t1':113 [binder, in References]
t1':118 [binder, in Smallstep]
t1':145 [binder, in Smallstep]
t1':170 [binder, in Smallstep]
t1':18 [binder, in Smallstep]
t1':180 [binder, in Smallstep]
t1':20 [binder, in Types]
t1':22 [binder, in Sub]
t1':23 [binder, in Types]
t1':24 [binder, in Norm]
t1':26 [binder, in Types]
t1':30 [binder, in Stlc]
t1':32 [binder, in MoreStlc]
t1':32 [binder, in Sub]
t1':34 [binder, in Norm]
t1':37 [binder, in Smallstep]
t1':38 [binder, in MoreStlc]
t1':38 [binder, in Norm]
t1':40 [binder, in Stlc]
t1':41 [binder, in MoreStlc]
t1':46 [binder, in MoreStlc]
t1':50 [binder, in References]
t1':50 [binder, in Records]
t1':51 [binder, in RecordSub]
t1':52 [binder, in MoreStlc]
t1':56 [binder, in Records]
t1':57 [binder, in RecordSub]
t1':61 [binder, in MoreStlc]
t1':62 [binder, in References]
t1':63 [binder, in Smallstep]
t1':63 [binder, in Records]
t1':64 [binder, in RecordSub]
t1':68 [binder, in References]
t1':76 [binder, in References]
t1':78 [binder, in Smallstep]
t1':85 [binder, in References]
t1':85 [binder, in MoreStlc]
t1':91 [binder, in MoreStlc]
t1':92 [binder, in Smallstep]
T11:114 [binder, in Norm]
T11:116 [binder, in RecordSub]
T11:79 [binder, in Records]
t12:115 [binder, in Norm]
T12:117 [binder, in RecordSub]
t12:118 [binder, in RecordSub]
T12:80 [binder, in Records]
t12:81 [binder, in Records]
T1:1 [binder, in Typechecking]
t1:101 [binder, in Smallstep]
t1:103 [binder, in Smallstep]
t1:105 [binder, in Smallstep]
t1:105 [binder, in References]
t1:106 [binder, in Sub]
t1:107 [binder, in Norm]
T1:109 [binder, in Sub]
t1:11 [binder, in Types]
T1:11 [binder, in Records]
t1:110 [binder, in Norm]
T1:111 [binder, in MoreStlc]
t1:112 [binder, in References]
t1:113 [binder, in Smallstep]
T1:114 [binder, in MoreStlc]
t1:115 [binder, in Smallstep]
T1:115 [binder, in Sub]
t1:116 [binder, in MoreStlc]
t1:117 [binder, in Smallstep]
T1:117 [binder, in MoreStlc]
t1:118 [binder, in Norm]
T1:119 [binder, in RecordSub]
t1:120 [binder, in MoreStlc]
t1:122 [binder, in RecordSub]
t1:122 [binder, in Norm]
T1:124 [binder, in UseAuto]
t1:126 [binder, in Norm]
t1:129 [binder, in MoreStlc]
t1:129 [binder, in Norm]
t1:13 [binder, in RecordSub]
t1:13 [binder, in Types]
T1:130 [binder, in References]
t1:132 [binder, in MoreStlc]
t1:132 [binder, in Norm]
T1:133 [binder, in References]
t1:135 [binder, in References]
T1:136 [binder, in References]
t1:137 [binder, in MoreStlc]
T1:138 [binder, in MoreStlc]
t1:139 [binder, in References]
t1:14 [binder, in MoreStlc]
t1:14 [binder, in Norm]
t1:14 [binder, in Sub]
T1:141 [binder, in UseAuto]
T1:142 [binder, in MoreStlc]
t1:144 [binder, in Smallstep]
t1:144 [binder, in References]
T1:146 [binder, in UseAuto]
t1:146 [binder, in References]
T1:147 [binder, in MoreStlc]
t1:148 [binder, in References]
t1:148 [binder, in MoreStlc]
t1:151 [binder, in References]
T1:152 [binder, in RecordSub]
T1:154 [binder, in MoreStlc]
t1:156 [binder, in MoreStlc]
T1:158 [binder, in MoreStlc]
t1:159 [binder, in References]
T1:16 [binder, in Records]
T1:160 [binder, in References]
t1:160 [binder, in MoreStlc]
T1:161 [binder, in MoreStlc]
t1:162 [binder, in References]
T1:163 [binder, in References]
t1:165 [binder, in References]
t1:169 [binder, in Smallstep]
T1:169 [binder, in RecordSub]
t1:17 [binder, in Smallstep]
t1:17 [binder, in References]
T1:17 [binder, in Typechecking]
T1:17 [binder, in MoreStlc]
T1:172 [binder, in Sub]
t1:175 [binder, in Smallstep]
T1:176 [binder, in Sub]
t1:177 [binder, in Smallstep]
T1:177 [binder, in UseAuto]
t1:179 [binder, in Smallstep]
T1:18 [binder, in Typechecking]
T1:18 [binder, in RecordSub]
T1:180 [binder, in Sub]
T1:184 [binder, in Sub]
t1:19 [binder, in Types]
T1:19 [binder, in MoreStlc]
T1:19 [binder, in Records]
t1:19 [binder, in Sub]
T1:20 [binder, in MoreStlc]
T1:21 [binder, in RecordSub]
t1:21 [binder, in Norm]
t1:21 [binder, in Sub]
T1:22 [binder, in Typechecking]
t1:22 [binder, in Types]
t1:23 [binder, in Norm]
t1:235 [binder, in References]
T1:236 [binder, in References]
t1:239 [binder, in Norm]
t1:24 [binder, in Records]
t1:25 [binder, in Types]
t1:27 [binder, in Stlc]
t1:27 [binder, in Sub]
t1:29 [binder, in Stlc]
t1:29 [binder, in MoreStlc]
t1:29 [binder, in Norm]
t1:29 [binder, in Sub]
T1:3 [binder, in StlcProp]
T1:31 [binder, in Typechecking]
t1:31 [binder, in MoreStlc]
t1:31 [binder, in Norm]
t1:31 [binder, in Sub]
t1:32 [binder, in RecordSub]
t1:33 [binder, in Norm]
t1:34 [binder, in Types]
t1:35 [binder, in Stlc]
t1:35 [binder, in Records]
t1:36 [binder, in Smallstep]
T1:37 [binder, in Typechecking]
t1:37 [binder, in Stlc]
t1:37 [binder, in MoreStlc]
t1:37 [binder, in Norm]
t1:38 [binder, in Types]
t1:39 [binder, in Stlc]
t1:39 [binder, in Types]
t1:40 [binder, in Types]
t1:40 [binder, in MoreStlc]
T1:44 [binder, in Typechecking]
T1:44 [binder, in Sub]
t1:45 [binder, in MoreStlc]
t1:46 [binder, in References]
T1:47 [binder, in Typechecking]
T1:47 [binder, in Stlc]
t1:47 [binder, in Records]
t1:48 [binder, in RecordSub]
t1:49 [binder, in References]
T1:49 [binder, in Typechecking]
t1:49 [binder, in StlcProp]
t1:49 [binder, in Records]
t1:50 [binder, in RecordSub]
T1:50 [binder, in Stlc]
T1:50 [binder, in Sub]
T1:51 [binder, in Typechecking]
t1:51 [binder, in StlcProp]
t1:51 [binder, in MoreStlc]
t1:52 [binder, in Stlc]
T1:53 [binder, in Stlc]
T1:53 [binder, in Sub]
T1:54 [binder, in StlcProp]
t1:55 [binder, in StlcProp]
t1:55 [binder, in Records]
t1:55 [binder, in Sub]
t1:56 [binder, in Smallstep]
T1:56 [binder, in Typechecking]
t1:56 [binder, in StlcProp]
t1:56 [binder, in RecordSub]
t1:56 [binder, in Stlc]
T1:56 [binder, in Norm]
T1:56 [binder, in Sub]
t1:59 [binder, in StlcProp]
T1:59 [binder, in Norm]
t1:59 [binder, in Sub]
t1:60 [binder, in Stlc]
t1:60 [binder, in MoreStlc]
t1:61 [binder, in References]
T1:61 [binder, in Typechecking]
t1:61 [binder, in Norm]
t1:62 [binder, in Smallstep]
t1:62 [binder, in StlcProp]
T1:62 [binder, in Norm]
t1:62 [binder, in Records]
t1:63 [binder, in RecordSub]
T1:63 [binder, in Stlc]
t1:63 [binder, in Sub]
T1:65 [binder, in MoreStlc]
t1:65 [binder, in Norm]
T1:66 [binder, in Sub]
t1:67 [binder, in References]
t1:69 [binder, in MoreStlc]
t1:69 [binder, in Norm]
T1:7 [binder, in Typechecking]
t1:70 [binder, in Sub]
T1:71 [binder, in Sub]
T1:72 [binder, in Norm]
t1:74 [binder, in References]
t1:74 [binder, in MoreStlc]
t1:75 [binder, in Norm]
t1:77 [binder, in Smallstep]
T1:77 [binder, in Norm]
T1:79 [binder, in RecordSub]
T1:8 [binder, in RecordSub]
t1:80 [binder, in MoreStlc]
T1:81 [binder, in Norm]
T1:82 [binder, in RecordSub]
T1:82 [binder, in Records]
T1:83 [binder, in MoreStlc]
t1:84 [binder, in References]
t1:84 [binder, in MoreStlc]
t1:84 [binder, in Records]
T1:85 [binder, in Norm]
T1:85 [binder, in Sub]
T1:86 [binder, in RecordSub]
t1:9 [binder, in Smallstep]
t1:9 [binder, in References]
t1:9 [binder, in Stlc]
t1:90 [binder, in MoreStlc]
t1:91 [binder, in Smallstep]
T1:91 [binder, in RecordSub]
T1:96 [binder, in MoreStlc]
t1:99 [binder, in References]
t2':119 [binder, in References]
t2':149 [binder, in Smallstep]
t2':174 [binder, in Smallstep]
t2':22 [binder, in Smallstep]
t2':26 [binder, in Sub]
t2':28 [binder, in Norm]
t2':34 [binder, in Stlc]
t2':36 [binder, in MoreStlc]
t2':41 [binder, in Smallstep]
t2':42 [binder, in Norm]
t2':50 [binder, in MoreStlc]
t2':54 [binder, in Records]
t2':55 [binder, in RecordSub]
t2':56 [binder, in References]
t2':64 [binder, in MoreStlc]
t2':67 [binder, in Smallstep]
t2':81 [binder, in References]
t2':82 [binder, in Smallstep]
t2':89 [binder, in MoreStlc]
t2:10 [binder, in Smallstep]
t2:102 [binder, in Smallstep]
t2:103 [binder, in MoreStlc]
t2:104 [binder, in Smallstep]
t2:107 [binder, in Smallstep]
t2:107 [binder, in Sub]
t2:108 [binder, in Norm]
T2:108 [binder, in Sub]
t2:111 [binder, in Norm]
t2:114 [binder, in Smallstep]
t2:114 [binder, in References]
T2:115 [binder, in MoreStlc]
t2:116 [binder, in Smallstep]
T2:116 [binder, in Sub]
t2:118 [binder, in References]
T2:118 [binder, in MoreStlc]
t2:119 [binder, in Smallstep]
t2:119 [binder, in Norm]
t2:12 [binder, in Types]
T2:12 [binder, in Records]
T2:120 [binder, in RecordSub]
t2:121 [binder, in MoreStlc]
t2:123 [binder, in RecordSub]
t2:123 [binder, in Norm]
t2:127 [binder, in Norm]
T2:13 [binder, in MoreStlc]
T2:13 [binder, in Norm]
T2:13 [binder, in Sub]
t2:130 [binder, in MoreStlc]
t2:130 [binder, in Norm]
t2:133 [binder, in MoreStlc]
t2:133 [binder, in Norm]
T2:134 [binder, in References]
T2:137 [binder, in References]
T2:139 [binder, in MoreStlc]
t2:14 [binder, in RecordSub]
t2:14 [binder, in Types]
t2:140 [binder, in References]
t2:141 [binder, in MoreStlc]
T2:142 [binder, in UseAuto]
T2:143 [binder, in MoreStlc]
t2:146 [binder, in Smallstep]
T2:147 [binder, in UseAuto]
t2:148 [binder, in Smallstep]
t2:149 [binder, in References]
T2:150 [binder, in MoreStlc]
t2:151 [binder, in MoreStlc]
t2:152 [binder, in References]
T2:153 [binder, in RecordSub]
t2:157 [binder, in MoreStlc]
t2:162 [binder, in MoreStlc]
t2:163 [binder, in RecordSub]
t2:166 [binder, in References]
T2:166 [binder, in MoreStlc]
T2:167 [binder, in References]
t2:17 [binder, in Types]
T2:17 [binder, in Records]
T2:170 [binder, in RecordSub]
t2:171 [binder, in Smallstep]
t2:173 [binder, in Smallstep]
T2:173 [binder, in Sub]
t2:176 [binder, in Smallstep]
T2:177 [binder, in Sub]
t2:178 [binder, in Smallstep]
T2:178 [binder, in UseAuto]
t2:18 [binder, in References]
T2:18 [binder, in Sub]
t2:181 [binder, in Smallstep]
T2:181 [binder, in Sub]
T2:185 [binder, in Sub]
t2:19 [binder, in Smallstep]
T2:19 [binder, in Typechecking]
T2:19 [binder, in RecordSub]
T2:2 [binder, in Typechecking]
T2:20 [binder, in Norm]
T2:20 [binder, in Records]
t2:21 [binder, in Smallstep]
T2:22 [binder, in RecordSub]
T2:23 [binder, in Typechecking]
t2:23 [binder, in Sub]
t2:240 [binder, in Norm]
t2:25 [binder, in Norm]
t2:25 [binder, in Records]
t2:25 [binder, in Sub]
T2:26 [binder, in Stlc]
t2:27 [binder, in Norm]
T2:28 [binder, in MoreStlc]
t2:28 [binder, in Sub]
t2:30 [binder, in Norm]
t2:30 [binder, in Sub]
T2:31 [binder, in RecordSub]
t2:31 [binder, in Stlc]
T2:32 [binder, in Typechecking]
t2:32 [binder, in Norm]
t2:33 [binder, in Stlc]
t2:33 [binder, in MoreStlc]
t2:33 [binder, in Sub]
T2:34 [binder, in Records]
t2:35 [binder, in Types]
t2:35 [binder, in MoreStlc]
t2:35 [binder, in Norm]
t2:36 [binder, in Stlc]
t2:38 [binder, in Smallstep]
T2:38 [binder, in Typechecking]
t2:38 [binder, in Stlc]
t2:39 [binder, in Norm]
T2:4 [binder, in StlcProp]
t2:40 [binder, in Smallstep]
t2:41 [binder, in Stlc]
t2:41 [binder, in Norm]
T2:43 [binder, in Typechecking]
T2:45 [binder, in References]
T2:45 [binder, in Typechecking]
T2:45 [binder, in Sub]
T2:46 [binder, in Records]
T2:47 [binder, in RecordSub]
t2:47 [binder, in MoreStlc]
t2:49 [binder, in MoreStlc]
t2:50 [binder, in StlcProp]
t2:51 [binder, in References]
T2:51 [binder, in Stlc]
t2:51 [binder, in Records]
T2:52 [binder, in Typechecking]
t2:52 [binder, in StlcProp]
t2:52 [binder, in RecordSub]
t2:53 [binder, in MoreStlc]
t2:53 [binder, in Records]
t2:54 [binder, in RecordSub]
T2:54 [binder, in Stlc]
T2:54 [binder, in Sub]
t2:55 [binder, in References]
t2:55 [binder, in MoreStlc]
T2:57 [binder, in Typechecking]
t2:57 [binder, in StlcProp]
t2:57 [binder, in Stlc]
T2:57 [binder, in Sub]
t2:58 [binder, in MoreStlc]
t2:60 [binder, in StlcProp]
T2:60 [binder, in Norm]
t2:60 [binder, in Sub]
t2:61 [binder, in Stlc]
T2:62 [binder, in Typechecking]
T2:62 [binder, in MoreStlc]
t2:63 [binder, in StlcProp]
t2:63 [binder, in MoreStlc]
T2:63 [binder, in Norm]
t2:64 [binder, in Smallstep]
t2:64 [binder, in Sub]
t2:66 [binder, in Smallstep]
t2:66 [binder, in Norm]
t2:70 [binder, in Norm]
t2:71 [binder, in MoreStlc]
T2:72 [binder, in Sub]
t2:75 [binder, in References]
t2:76 [binder, in MoreStlc]
t2:76 [binder, in Norm]
T2:77 [binder, in MoreStlc]
T2:78 [binder, in Norm]
t2:79 [binder, in Smallstep]
T2:8 [binder, in References]
T2:8 [binder, in Typechecking]
T2:8 [binder, in Stlc]
t2:80 [binder, in References]
T2:80 [binder, in RecordSub]
t2:81 [binder, in Smallstep]
t2:82 [binder, in MoreStlc]
T2:82 [binder, in Norm]
T2:83 [binder, in RecordSub]
T2:83 [binder, in Records]
t2:85 [binder, in Records]
t2:86 [binder, in References]
t2:86 [binder, in MoreStlc]
T2:86 [binder, in Norm]
T2:86 [binder, in Sub]
t2:88 [binder, in MoreStlc]
T2:9 [binder, in RecordSub]
t2:90 [binder, in References]
T2:92 [binder, in RecordSub]
t2:92 [binder, in MoreStlc]
t2:93 [binder, in Smallstep]
t2:94 [binder, in References]
t2:97 [binder, in MoreStlc]
t2:98 [binder, in Sub]
t3:100 [binder, in MoreStlc]
t3:106 [binder, in MoreStlc]
t3:108 [binder, in Smallstep]
t3:120 [binder, in Smallstep]
t3:134 [binder, in MoreStlc]
T3:152 [binder, in MoreStlc]
t3:153 [binder, in References]
t3:165 [binder, in MoreStlc]
T3:179 [binder, in UseAuto]
t3:18 [binder, in Types]
t3:182 [binder, in Smallstep]
t3:34 [binder, in Sub]
t3:36 [binder, in Types]
t3:36 [binder, in Norm]
t3:42 [binder, in Stlc]
t3:54 [binder, in MoreStlc]
t3:56 [binder, in MoreStlc]
t3:58 [binder, in StlcProp]
t3:59 [binder, in MoreStlc]
t3:61 [binder, in StlcProp]
t3:62 [binder, in Stlc]
t3:64 [binder, in StlcProp]
t3:65 [binder, in Sub]
t3:71 [binder, in Norm]
t3:87 [binder, in References]
t3:91 [binder, in References]
t3:95 [binder, in References]
t3:95 [binder, in MoreStlc]
T4:180 [binder, in UseAuto]
t:1 [binder, in StlcProp]
t:10 [binder, in Typechecking]
t:10 [binder, in StlcProp]
T:100 [binder, in StlcProp]
T:100 [binder, in RecordSub]
t:100 [binder, in Norm]
t:101 [binder, in UseAuto]
t:101 [binder, in StlcProp]
T:101 [binder, in UseTactics]
T:102 [binder, in StlcProp]
T:102 [binder, in Norm]
T:103 [binder, in Sub]
t:104 [binder, in UseAuto]
T:104 [binder, in UseTactics]
t:104 [binder, in Records]
T:105 [binder, in Records]
t:107 [binder, in UseAuto]
T:107 [binder, in Records]
t:109 [binder, in Smallstep]
T:11 [binder, in StlcProp]
t:111 [binder, in UseAuto]
t:111 [binder, in Records]
T:111 [binder, in Sub]
T:111 [binder, in LibTactics]
T:112 [binder, in Records]
T:113 [binder, in UseAuto]
T:113 [binder, in RecordSub]
t:116 [binder, in Records]
T:117 [binder, in Records]
t:119 [binder, in Records]
t:119 [binder, in Sub]
t:12 [binder, in Stlc]
T:120 [binder, in Records]
T:120 [binder, in Sub]
t:122 [binder, in References]
t:122 [binder, in Sub]
T:123 [binder, in Sub]
t:124 [binder, in Records]
t:125 [binder, in MoreStlc]
t:126 [binder, in UseAuto]
t:126 [binder, in RecordSub]
T:126 [binder, in Records]
T:127 [binder, in RecordSub]
t:127 [binder, in MoreStlc]
t:127 [binder, in Records]
t:127 [binder, in Sub]
T:128 [binder, in UseAuto]
T:129 [binder, in Records]
T:129 [binder, in Sub]
t:130 [binder, in RecordSub]
t:130 [binder, in Sub]
T:132 [binder, in RecordSub]
T:132 [binder, in Sub]
t:133 [binder, in UseAuto]
T:134 [binder, in UseAuto]
t:135 [binder, in Norm]
T:135 [binder, in Sub]
t:136 [binder, in RecordSub]
T:137 [binder, in RecordSub]
t:137 [binder, in Norm]
t:138 [binder, in Smallstep]
t:138 [binder, in Norm]
T:139 [binder, in Sub]
t:14 [binder, in References]
t:14 [binder, in Typechecking]
t:141 [binder, in RecordSub]
t:142 [binder, in Smallstep]
T:142 [binder, in RecordSub]
t:142 [binder, in Norm]
T:143 [binder, in Sub]
T:146 [binder, in RecordSub]
T:147 [binder, in Sub]
t:148 [binder, in Norm]
T:149 [binder, in Norm]
t:15 [binder, in StlcProp]
T:15 [binder, in LibTactics]
t:150 [binder, in Smallstep]
T:151 [binder, in Sub]
t:152 [binder, in Smallstep]
t:152 [binder, in Norm]
T:153 [binder, in Norm]
t:154 [binder, in Norm]
t:155 [binder, in Smallstep]
T:155 [binder, in Sub]
t:157 [binder, in RecordSub]
T:157 [binder, in Norm]
t:158 [binder, in Smallstep]
T:158 [binder, in RecordSub]
t:158 [binder, in Norm]
T:159 [binder, in Sub]
T:16 [binder, in StlcProp]
T:162 [binder, in Norm]
t:163 [binder, in Norm]
T:163 [binder, in Sub]
T:164 [binder, in RecordSub]
T:164 [binder, in Norm]
t:165 [binder, in Norm]
T:165 [binder, in Sub]
t:166 [binder, in Norm]
t:168 [binder, in MoreStlc]
T:168 [binder, in Norm]
T:168 [binder, in Sub]
T:169 [binder, in UseAuto]
T:169 [binder, in References]
T:169 [binder, in MoreStlc]
t:169 [binder, in Norm]
t:170 [binder, in References]
T:170 [binder, in Sub]
T:171 [binder, in Norm]
T:172 [binder, in UseAuto]
t:172 [binder, in Norm]
t:173 [binder, in RecordSub]
t:173 [binder, in MoreStlc]
T:174 [binder, in RecordSub]
T:174 [binder, in MoreStlc]
T:174 [binder, in Norm]
t:175 [binder, in Norm]
T:176 [binder, in UseAuto]
t:176 [binder, in RecordSub]
t:176 [binder, in MoreStlc]
T:177 [binder, in RecordSub]
T:177 [binder, in MoreStlc]
T:177 [binder, in Norm]
t:178 [binder, in Norm]
t:18 [binder, in StlcProp]
T:181 [binder, in References]
t:181 [binder, in RecordSub]
t:181 [binder, in MoreStlc]
t:181 [binder, in Norm]
T:182 [binder, in UseAuto]
t:182 [binder, in References]
t:183 [binder, in Smallstep]
T:183 [binder, in RecordSub]
T:183 [binder, in MoreStlc]
t:184 [binder, in RecordSub]
t:184 [binder, in MoreStlc]
t:185 [binder, in Smallstep]
T:186 [binder, in RecordSub]
T:186 [binder, in MoreStlc]
T:19 [binder, in StlcProp]
T:19 [binder, in LibTactics]
T:196 [binder, in Sub]
T:199 [binder, in References]
t:2 [binder, in StlcProp]
T:201 [binder, in Norm]
t:202 [binder, in References]
T:202 [binder, in Sub]
T:204 [binder, in References]
T:204 [binder, in Sub]
t:205 [binder, in Norm]
T:206 [binder, in Sub]
t:208 [binder, in Norm]
T:208 [binder, in Sub]
t:21 [binder, in Stlc]
T:210 [binder, in Sub]
t:211 [binder, in References]
t:211 [binder, in Norm]
T:212 [binder, in References]
T:212 [binder, in Sub]
T:214 [binder, in Sub]
t:215 [binder, in References]
T:215 [binder, in Sub]
T:216 [binder, in References]
t:216 [binder, in Norm]
T:216 [binder, in Sub]
T:217 [binder, in Sub]
t:218 [binder, in Norm]
T:218 [binder, in Sub]
t:221 [binder, in References]
T:222 [binder, in Sub]
T:223 [binder, in References]
t:223 [binder, in Norm]
T:223 [binder, in Sub]
t:225 [binder, in Sub]
T:226 [binder, in Sub]
t:227 [binder, in References]
t:23 [binder, in StlcProp]
t:231 [binder, in References]
t:231 [binder, in Norm]
T:232 [binder, in References]
T:236 [binder, in Norm]
t:237 [binder, in Norm]
t:242 [binder, in References]
T:244 [binder, in References]
t:249 [binder, in References]
T:25 [binder, in StlcProp]
t:25 [binder, in RecordSub]
T:250 [binder, in References]
T:250 [binder, in Norm]
t:251 [binder, in Norm]
T:254 [binder, in References]
t:257 [binder, in Norm]
T:258 [binder, in Norm]
t:26 [binder, in Typechecking]
t:263 [binder, in Norm]
t:268 [binder, in Norm]
T:27 [binder, in Typechecking]
t:27 [binder, in Types]
t:272 [binder, in Norm]
T:273 [binder, in Norm]
t:276 [binder, in Norm]
T:277 [binder, in Norm]
t:28 [binder, in Types]
t:28 [binder, in Records]
t:29 [binder, in Typechecking]
t:29 [binder, in StlcProp]
t:29 [binder, in Types]
t:3 [binder, in Smallstep]
T:30 [binder, in Typechecking]
T:31 [binder, in StlcProp]
T:31 [binder, in UseTactics]
t:32 [binder, in StlcProp]
T:34 [binder, in StlcProp]
t:35 [binder, in StlcProp]
t:36 [binder, in References]
T:36 [binder, in Typechecking]
T:37 [binder, in StlcProp]
T:37 [binder, in Types]
T:37 [binder, in Sub]
t:38 [binder, in StlcProp]
t:39 [binder, in StlcProp]
t:40 [binder, in References]
t:40 [binder, in Typechecking]
T:40 [binder, in Sub]
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 StlcProp]
t:44 [binder, in Types]
T:45 [binder, in Types]
t:46 [binder, in Smallstep]
t:47 [binder, in Types]
t:49 [binder, in Smallstep]
T:49 [binder, in Types]
t:50 [binder, in Types]
t:51 [binder, in Norm]
t:52 [binder, in Smallstep]
T:52 [binder, in Types]
t:53 [binder, in Types]
T:55 [binder, in Types]
t:56 [binder, in Types]
T:58 [binder, in Types]
t:59 [binder, in Types]
T:6 [binder, in Typechecking]
T:61 [binder, in Types]
t:64 [binder, in Typechecking]
T:65 [binder, in Typechecking]
t:65 [binder, in StlcProp]
T:65 [binder, in Stlc]
T:66 [binder, in Stlc]
t:67 [binder, in Typechecking]
T:68 [binder, in Typechecking]
t:68 [binder, in StlcProp]
T:68 [binder, in Stlc]
t:69 [binder, in Typechecking]
T:69 [binder, in StlcProp]
t:7 [binder, in StlcProp]
t:7 [binder, in Types]
t:7 [binder, in MoreStlc]
t:7 [binder, in Norm]
t:7 [binder, in Sub]
t:72 [binder, in StlcProp]
T:72 [binder, in RecordSub]
T:73 [binder, in StlcProp]
t:74 [binder, in Typechecking]
T:75 [binder, in RecordSub]
t:75 [binder, in UseTactics]
t:76 [binder, in StlcProp]
T:77 [binder, in StlcProp]
T:77 [binder, in UseTactics]
T:77 [binder, in Records]
T:8 [binder, in StlcProp]
t:8 [binder, in Types]
t:84 [binder, in Typechecking]
t:85 [binder, in Typechecking]
t:85 [binder, in StlcProp]
t:86 [binder, in UseAuto]
t:86 [binder, in Typechecking]
t:87 [binder, in Records]
T:88 [binder, in UseAuto]
t:88 [binder, in Typechecking]
t:89 [binder, in UseAuto]
t:89 [binder, in Typechecking]
t:89 [binder, in Norm]
T:90 [binder, in Norm]
T:91 [binder, in UseAuto]
t:91 [binder, in StlcProp]
t:91 [binder, in Records]
t:92 [binder, in UseAuto]
t:92 [binder, in Norm]
T:92 [binder, in Records]
t:92 [binder, in Sub]
T:93 [binder, in UseAuto]
T:93 [binder, in Norm]
T:93 [binder, in Sub]
t:94 [binder, in Smallstep]
t:95 [binder, in UseAuto]
T:95 [binder, in RecordSub]
T:95 [binder, in Records]
T:96 [binder, in UseAuto]
t:96 [binder, in StlcProp]
T:96 [binder, in UseTactics]
T:97 [binder, in StlcProp]
T:97 [binder, in RecordSub]
t:97 [binder, in Norm]
T:97 [binder, in Records]
t:98 [binder, in UseAuto]
t:98 [binder, in StlcProp]
T:99 [binder, in Norm]
T:99 [binder, in Records]
T:99 [binder, in Sub]
U
UnfoldsExample [module, in UseTactics]UnfoldsExample.bexp_eval_true [lemma, in UseTactics]
UseAuto [library]
UseTactics [library]
U1:107 [binder, in RecordSub]
U1:77 [binder, in Sub]
U2:108 [binder, in RecordSub]
U2:78 [binder, in Sub]
U:104 [binder, in RecordSub]
u:114 [binder, in Equiv]
U:123 [binder, in Records]
U:126 [binder, in Sub]
U:136 [binder, in Sub]
U:140 [binder, in Sub]
U:144 [binder, in Sub]
U:148 [binder, in Sub]
U:152 [binder, in Sub]
U:156 [binder, in Sub]
U:160 [binder, in Sub]
U:173 [binder, in UseAuto]
U:180 [binder, in RecordSub]
U:180 [binder, in MoreStlc]
U:189 [binder, in LibTactics]
U:22 [binder, in StlcProp]
U:220 [binder, in References]
U:28 [binder, in StlcProp]
u:38 [binder, in UseTactics]
U:39 [binder, in Sub]
u:6 [binder, in StlcProp]
U:73 [binder, in Sub]
U:74 [binder, in RecordSub]
U:74 [binder, in UseTactics]
U:74 [binder, in Sub]
U:79 [binder, in Sub]
U:80 [binder, in Sub]
U:82 [binder, in Sub]
U:96 [binder, in Norm]
V
vacuous_substitution [lemma, in Norm]valid [definition, in HoareAsLogic]
value [inductive, in Smallstep]
value [inductive, in Norm]
value_is_nf [lemma, in Smallstep]
value_halts [lemma, in Norm]
value__normal [lemma, in Norm]
varname:273 [binder, in LibTactics]
varname:274 [binder, in LibTactics]
varname:275 [binder, in LibTactics]
varname:276 [binder, in LibTactics]
var_not_used_in_aexp [inductive, in Equiv]
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]
vi:149 [binder, in RecordSub]
vi:60 [binder, in Records]
vi:61 [binder, in RecordSub]
vl:102 [binder, in MoreStlc]
VNUId [constructor, in Equiv]
VNUMinus [constructor, in Equiv]
VNUMult [constructor, in Equiv]
VNUNum [constructor, in Equiv]
VNUPlus [constructor, in Equiv]
vr:35 [binder, in RecordSub]
vr:38 [binder, in Records]
v_const [constructor, in Smallstep]
V_cons [constructor, in Norm]
V_nil [constructor, in Norm]
v_pair [constructor, in Norm]
v_false [constructor, in Norm]
v_true [constructor, in Norm]
v_abs [constructor, in Norm]
V0:39 [binder, in PE]
V0:62 [binder, in PE]
V0:69 [binder, in PE]
v0:72 [binder, in MoreStlc]
v0:78 [binder, in MoreStlc]
v1:101 [binder, in MoreStlc]
V1:105 [binder, in RecordSub]
v1:11 [binder, in Smallstep]
v1:117 [binder, in References]
v1:147 [binder, in Smallstep]
v1:15 [binder, in Smallstep]
v1:15 [binder, in Norm]
v1:167 [binder, in Smallstep]
v1:172 [binder, in Smallstep]
v1:197 [binder, in Smallstep]
v1:20 [binder, in Smallstep]
v1:200 [binder, in Smallstep]
v1:205 [binder, in Smallstep]
v1:208 [binder, in Smallstep]
v1:21 [binder, in MoreStlc]
v1:213 [binder, in Smallstep]
v1:216 [binder, in Smallstep]
v1:222 [binder, in Norm]
v1:224 [binder, in Smallstep]
v1:227 [binder, in Smallstep]
v1:23 [binder, in MoreStlc]
v1:232 [binder, in Smallstep]
v1:235 [binder, in Smallstep]
v1:24 [binder, in Sub]
v1:26 [binder, in Norm]
v1:32 [binder, in Stlc]
v1:34 [binder, in Smallstep]
v1:34 [binder, in RecordSub]
v1:34 [binder, in MoreStlc]
v1:37 [binder, in Records]
v1:39 [binder, in Smallstep]
v1:40 [binder, in Norm]
v1:45 [binder, in Norm]
v1:48 [binder, in MoreStlc]
v1:49 [binder, in Norm]
v1:52 [binder, in Records]
v1:53 [binder, in RecordSub]
v1:54 [binder, in References]
v1:60 [binder, in Smallstep]
v1:65 [binder, in Smallstep]
v1:66 [binder, in Records]
v1:67 [binder, in RecordSub]
v1:75 [binder, in Smallstep]
V1:75 [binder, in Sub]
v1:79 [binder, in References]
v1:80 [binder, in Smallstep]
v1:87 [binder, in MoreStlc]
v1:89 [binder, in Smallstep]
V2:106 [binder, in RecordSub]
v2:12 [binder, in Smallstep]
v2:16 [binder, in Smallstep]
v2:16 [binder, in Norm]
v2:168 [binder, in Smallstep]
v2:20 [binder, in Sub]
v2:201 [binder, in Smallstep]
v2:209 [binder, in Smallstep]
v2:217 [binder, in Smallstep]
v2:22 [binder, in MoreStlc]
v2:22 [binder, in Norm]
v2:228 [binder, in Smallstep]
v2:236 [binder, in Smallstep]
v2:24 [binder, in MoreStlc]
v2:28 [binder, in Stlc]
v2:30 [binder, in MoreStlc]
v2:35 [binder, in Smallstep]
v2:46 [binder, in Norm]
v2:47 [binder, in References]
v2:48 [binder, in Records]
v2:49 [binder, in RecordSub]
v2:50 [binder, in Norm]
v2:57 [binder, in Smallstep]
v2:61 [binder, in Smallstep]
v2:76 [binder, in Smallstep]
V2:76 [binder, in Sub]
v2:90 [binder, in Smallstep]
V:10 [binder, in HoareAsLogic]
V:101 [binder, in PE]
v:102 [binder, in UseAuto]
V:104 [binder, in PE]
v:105 [binder, in UseAuto]
v:106 [binder, in Records]
v:108 [binder, in UseAuto]
v:109 [binder, in References]
V:115 [binder, in PE]
V:123 [binder, in PE]
v:125 [binder, in Records]
v:128 [binder, in Sub]
V:137 [binder, in Sub]
V:141 [binder, in Sub]
v:145 [binder, in RecordSub]
V:145 [binder, in Sub]
V:149 [binder, in Sub]
V:153 [binder, in Sub]
v:156 [binder, in Norm]
V:157 [binder, in Sub]
v:16 [binder, in MoreStlc]
V:161 [binder, in Sub]
v:18 [binder, in MoreStlc]
v:182 [binder, in RecordSub]
v:182 [binder, in MoreStlc]
V:2 [binder, in PE]
v:202 [binder, in Norm]
v:21 [binder, in Types]
v:213 [binder, in Norm]
v:217 [binder, in Norm]
v:221 [binder, in Norm]
v:222 [binder, in References]
v:230 [binder, in Norm]
v:24 [binder, in StlcProp]
v:24 [binder, in Types]
V:26 [binder, in PE]
v:262 [binder, in Norm]
v:30 [binder, in StlcProp]
V:366 [binder, in PE]
v:39 [binder, in UseTactics]
V:44 [binder, in PE]
v:48 [binder, in Smallstep]
V:57 [binder, in PE]
V:6 [binder, in PE]
V:61 [binder, in PE]
V:64 [binder, in PE]
V:67 [binder, in PE]
v:68 [binder, in Smallstep]
V:72 [binder, in PE]
v:76 [binder, in UseTactics]
V:76 [binder, in PE]
V:80 [binder, in PE]
v:83 [binder, in Smallstep]
V:83 [binder, in PE]
V:94 [binder, in PE]
v:97 [binder, in References]
v:98 [binder, in Norm]
v:99 [binder, in UseAuto]
W
weakening [lemma, in Norm]weakening_empty [lemma, in Norm]
while_example [definition, in Hoare]
while_true [lemma, in Equiv]
while_true_nonterm [lemma, in Equiv]
while_false [lemma, in Equiv]
working_of_auto_2 [lemma, in UseAuto]
working_of_auto_1 [lemma, in UseAuto]
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]
w:40 [binder, in UseTactics]
X
xts:185 [binder, in Norm]x':246 [binder, in Norm]
x1:104 [binder, in MoreStlc]
x1:118 [binder, in Equiv]
x1:127 [binder, in LibTactics]
x1:130 [binder, in LibTactics]
x1:135 [binder, in LibTactics]
x1:142 [binder, in LibTactics]
x1:146 [binder, in MoreStlc]
x1:151 [binder, in LibTactics]
x1:162 [binder, in LibTactics]
x1:163 [binder, in MoreStlc]
x1:175 [binder, in LibTactics]
x1:201 [binder, in LibTactics]
x1:209 [binder, in LibTactics]
x1:217 [binder, in LibTactics]
x1:220 [binder, in Norm]
x1:224 [binder, in LibTactics]
x1:231 [binder, in LibTactics]
x1:237 [binder, in LibTactics]
x1:243 [binder, in LibTactics]
x1:248 [binder, in LibTactics]
x1:253 [binder, in LibTactics]
x1:257 [binder, in LibTactics]
x1:261 [binder, in LibTactics]
x1:264 [binder, in LibTactics]
x1:267 [binder, in LibTactics]
x1:269 [binder, in LibTactics]
x1:271 [binder, in LibTactics]
x1:272 [binder, in LibTactics]
x1:35 [binder, in LibTactics]
x1:37 [binder, in LibTactics]
x1:40 [binder, in LibTactics]
x1:44 [binder, in LibTactics]
x1:49 [binder, in LibTactics]
x1:58 [binder, in LibTactics]
x1:61 [binder, in LibTactics]
x1:63 [binder, in UseTactics]
x1:63 [binder, in LibTactics]
x1:66 [binder, in LibTactics]
x1:68 [binder, in MoreStlc]
x1:69 [binder, in LibTactics]
x1:73 [binder, in MoreStlc]
x1:73 [binder, in LibTactics]
x1:77 [binder, in LibTactics]
x1:79 [binder, in MoreStlc]
x1:82 [binder, in LibTactics]
x1:87 [binder, in LibTactics]
x1:93 [binder, in MoreStlc]
x1:93 [binder, in LibTactics]
x1:98 [binder, in MoreStlc]
x1:99 [binder, in LibTactics]
x2:100 [binder, in LibTactics]
x2:105 [binder, in MoreStlc]
x2:119 [binder, in Equiv]
x2:132 [binder, in LibTactics]
x2:137 [binder, in LibTactics]
x2:144 [binder, in LibTactics]
x2:149 [binder, in MoreStlc]
x2:153 [binder, in LibTactics]
x2:164 [binder, in MoreStlc]
x2:164 [binder, in LibTactics]
x2:177 [binder, in LibTactics]
x2:202 [binder, in LibTactics]
x2:210 [binder, in LibTactics]
x2:218 [binder, in LibTactics]
x2:225 [binder, in LibTactics]
x2:232 [binder, in LibTactics]
x2:238 [binder, in LibTactics]
x2:244 [binder, in LibTactics]
x2:249 [binder, in LibTactics]
x2:254 [binder, in LibTactics]
x2:258 [binder, in LibTactics]
x2:262 [binder, in LibTactics]
x2:265 [binder, in LibTactics]
x2:268 [binder, in LibTactics]
x2:270 [binder, in LibTactics]
x2:38 [binder, in LibTactics]
x2:41 [binder, in LibTactics]
x2:45 [binder, in LibTactics]
x2:50 [binder, in LibTactics]
x2:64 [binder, in UseTactics]
x2:64 [binder, in LibTactics]
x2:67 [binder, in LibTactics]
x2:70 [binder, in MoreStlc]
x2:70 [binder, in LibTactics]
x2:74 [binder, in LibTactics]
x2:75 [binder, in MoreStlc]
x2:78 [binder, in LibTactics]
x2:81 [binder, in MoreStlc]
x2:83 [binder, in LibTactics]
x2:88 [binder, in LibTactics]
x2:94 [binder, in MoreStlc]
x2:94 [binder, in LibTactics]
x2:99 [binder, in MoreStlc]
x3:101 [binder, in LibTactics]
x3:139 [binder, in LibTactics]
x3:146 [binder, in LibTactics]
x3:155 [binder, in LibTactics]
x3:166 [binder, in LibTactics]
x3:179 [binder, in LibTactics]
x3:203 [binder, in LibTactics]
x3:211 [binder, in LibTactics]
x3:219 [binder, in LibTactics]
x3:226 [binder, in LibTactics]
x3:233 [binder, in LibTactics]
x3:239 [binder, in LibTactics]
x3:245 [binder, in LibTactics]
x3:250 [binder, in LibTactics]
x3:255 [binder, in LibTactics]
x3:259 [binder, in LibTactics]
x3:263 [binder, in LibTactics]
x3:266 [binder, in LibTactics]
x3:42 [binder, in LibTactics]
x3:46 [binder, in LibTactics]
x3:51 [binder, in LibTactics]
x3:71 [binder, in LibTactics]
x3:75 [binder, in LibTactics]
x3:79 [binder, in LibTactics]
x3:84 [binder, in LibTactics]
x3:89 [binder, in LibTactics]
x3:95 [binder, in LibTactics]
x4:102 [binder, in LibTactics]
x4:148 [binder, in LibTactics]
x4:157 [binder, in LibTactics]
x4:168 [binder, in LibTactics]
x4:181 [binder, in LibTactics]
x4:204 [binder, in LibTactics]
x4:212 [binder, in LibTactics]
x4:220 [binder, in LibTactics]
x4:227 [binder, in LibTactics]
x4:234 [binder, in LibTactics]
x4:240 [binder, in LibTactics]
x4:246 [binder, in LibTactics]
x4:251 [binder, in LibTactics]
x4:256 [binder, in LibTactics]
x4:260 [binder, in LibTactics]
x4:47 [binder, in LibTactics]
x4:52 [binder, in LibTactics]
x4:80 [binder, in LibTactics]
x4:85 [binder, in LibTactics]
x4:90 [binder, in LibTactics]
x4:96 [binder, in LibTactics]
x5:103 [binder, in LibTactics]
x5:159 [binder, in LibTactics]
x5:170 [binder, in LibTactics]
x5:183 [binder, in LibTactics]
x5:205 [binder, in LibTactics]
x5:213 [binder, in LibTactics]
x5:221 [binder, in LibTactics]
x5:228 [binder, in LibTactics]
x5:235 [binder, in LibTactics]
x5:241 [binder, in LibTactics]
x5:247 [binder, in LibTactics]
x5:252 [binder, in LibTactics]
x5:53 [binder, in LibTactics]
x5:91 [binder, in LibTactics]
x5:97 [binder, in LibTactics]
x6:104 [binder, in LibTactics]
x6:172 [binder, in LibTactics]
x6:185 [binder, in LibTactics]
x6:206 [binder, in LibTactics]
x6:214 [binder, in LibTactics]
x6:222 [binder, in LibTactics]
x6:229 [binder, in LibTactics]
x6:236 [binder, in LibTactics]
x6:242 [binder, in LibTactics]
x7:187 [binder, in LibTactics]
x7:207 [binder, in LibTactics]
x7:215 [binder, in LibTactics]
x7:223 [binder, in LibTactics]
x7:230 [binder, in LibTactics]
x8:208 [binder, in LibTactics]
x8:216 [binder, in LibTactics]
X:1 [binder, in Records]
x:10 [binder, in Stlc]
x:10 [binder, in UseTactics]
x:100 [binder, in UseTactics]
x:102 [binder, in Sub]
x:103 [binder, in UseTactics]
x:105 [binder, in UseTactics]
x:105 [binder, in Norm]
x:106 [binder, in Norm]
x:109 [binder, in Norm]
x:110 [binder, in MoreStlc]
x:112 [binder, in RecordSub]
x:112 [binder, in Norm]
x:112 [binder, in Sub]
x:113 [binder, in MoreStlc]
x:113 [binder, in Equiv]
x:115 [binder, in RecordSub]
x:116 [binder, in Norm]
x:116 [binder, in LibTactics]
x:119 [binder, in UseAuto]
x:12 [binder, in References]
x:12 [binder, in MoreStlc]
x:12 [binder, in Norm]
x:12 [binder, in Sub]
x:120 [binder, in Norm]
X:121 [binder, in Smallstep]
x:122 [binder, in Equiv]
x:122 [binder, in Records]
x:124 [binder, in Norm]
x:125 [binder, in Smallstep]
x:125 [binder, in Sub]
x:126 [binder, in Smallstep]
x:127 [binder, in Hoare]
x:128 [binder, in Norm]
X:129 [binder, in Smallstep]
x:129 [binder, in References]
x:131 [binder, in Smallstep]
x:131 [binder, in Norm]
x:132 [binder, in References]
X:133 [binder, in Smallstep]
x:133 [binder, in Equiv]
x:134 [binder, in Norm]
x:135 [binder, in Smallstep]
x:136 [binder, in Norm]
x:138 [binder, in UseAuto]
x:139 [binder, in Norm]
X:140 [binder, in Smallstep]
x:143 [binder, in UseAuto]
x:144 [binder, in Norm]
x:145 [binder, in Equiv]
x:145 [binder, in Norm]
x:147 [binder, in Norm]
X:15 [binder, in UseTactics]
x:154 [binder, in RecordSub]
x:155 [binder, in UseAuto]
x:156 [binder, in UseAuto]
x:157 [binder, in UseAuto]
x:158 [binder, in UseAuto]
x:16 [binder, in Stlc]
x:160 [binder, in UseAuto]
X:161 [binder, in Hoare]
x:161 [binder, in RecordSub]
x:162 [binder, in UseAuto]
x:164 [binder, in UseAuto]
x:165 [binder, in UseAuto]
x:166 [binder, in UseAuto]
x:166 [binder, in RecordSub]
x:17 [binder, in Sub]
x:175 [binder, in Hoare]
x:179 [binder, in RecordSub]
x:179 [binder, in MoreStlc]
x:183 [binder, in UseAuto]
x:185 [binder, in UseAuto]
x:188 [binder, in UseAuto]
X:188 [binder, in Norm]
x:189 [binder, in References]
x:19 [binder, in UseTactics]
x:19 [binder, in Norm]
x:190 [binder, in UseAuto]
x:192 [binder, in LibTactics]
x:193 [binder, in UseAuto]
X:193 [binder, in Norm]
x:199 [binder, in UseAuto]
x:20 [binder, in Stlc]
x:20 [binder, in UseTactics]
x:200 [binder, in Norm]
x:205 [binder, in UseAuto]
x:206 [binder, in Norm]
x:209 [binder, in Norm]
x:21 [binder, in StlcProp]
X:21 [binder, in LibTactics]
x:212 [binder, in Hoare]
x:212 [binder, in Norm]
x:215 [binder, in UseAuto]
x:215 [binder, in Norm]
x:219 [binder, in References]
x:219 [binder, in Norm]
x:22 [binder, in LibTactics]
x:229 [binder, in Norm]
X:23 [binder, in Smallstep]
x:23 [binder, in References]
x:23 [binder, in RecordSub]
x:233 [binder, in Norm]
x:235 [binder, in Norm]
x:237 [binder, in Hoare]
x:239 [binder, in References]
X:24 [binder, in Smallstep]
x:242 [binder, in Norm]
x:245 [binder, in Norm]
X:248 [binder, in Hoare]
x:249 [binder, in Norm]
x:25 [binder, in Stlc]
X:252 [binder, in Hoare]
X:254 [binder, in Hoare]
X:255 [binder, in References]
x:256 [binder, in Norm]
x:259 [binder, in References]
x:26 [binder, in Smallstep]
X:26 [binder, in Hoare]
x:26 [binder, in Records]
x:26 [binder, in LibTactics]
x:261 [binder, in References]
x:261 [binder, in Norm]
x:267 [binder, in Hoare]
x:27 [binder, in StlcProp]
x:27 [binder, in MoreStlc]
x:274 [binder, in Norm]
x:275 [binder, in Norm]
x:28 [binder, in Hoare]
x:28 [binder, in LibTactics]
x:282 [binder, in LibTactics]
X:30 [binder, in Hoare]
x:30 [binder, in References]
x:30 [binder, in RecordSub]
X:316 [binder, in Hoare]
x:32 [binder, in Hoare]
x:33 [binder, in References]
x:33 [binder, in Records]
x:35 [binder, in PE]
x:38 [binder, in UseAuto]
x:41 [binder, in UseAuto]
x:41 [binder, in UseTactics]
x:41 [binder, in Equiv]
X:42 [binder, in Equiv]
X:44 [binder, in Smallstep]
x:44 [binder, in References]
x:45 [binder, in UseAuto]
x:45 [binder, in Records]
x:46 [binder, in StlcProp]
x:46 [binder, in RecordSub]
x:46 [binder, in Stlc]
x:47 [binder, in UseAuto]
x:48 [binder, in UseTactics]
x:49 [binder, in Stlc]
x:49 [binder, in Sub]
x:5 [binder, in StlcProp]
X:5 [binder, in UseTactics]
x:5 [binder, in MoreStlc]
x:5 [binder, in Norm]
x:5 [binder, in Sub]
x:50 [binder, in UseAuto]
x:52 [binder, in Sub]
X:54 [binder, in Hoare]
x:55 [binder, in Norm]
x:58 [binder, in Norm]
X:59 [binder, in Hoare]
x:59 [binder, in UseTactics]
X:6 [binder, in Hoare2]
x:61 [binder, in Hoare2]
x:62 [binder, in Equiv]
x:64 [binder, in UseAuto]
x:65 [binder, in Hoare2]
x:66 [binder, in StlcProp]
x:66 [binder, in Hoare2]
x:67 [binder, in StlcProp]
x:7 [binder, in References]
x:7 [binder, in Stlc]
x:73 [binder, in UseTactics]
x:76 [binder, in Records]
x:78 [binder, in StlcProp]
x:78 [binder, in Records]
x:8 [binder, in UseTactics]
x:83 [binder, in StlcProp]
x:87 [binder, in Sub]
x:89 [binder, in PE]
x:9 [binder, in UseTactics]
X:94 [binder, in Hoare2]
x:95 [binder, in UseTactics]
x:95 [binder, in Norm]
x:96 [binder, in Sub]
X:98 [binder, in Hoare2]
Y
y1:128 [binder, in LibTactics]y1:131 [binder, in LibTactics]
y1:136 [binder, in LibTactics]
y1:143 [binder, in LibTactics]
y1:152 [binder, in LibTactics]
y1:163 [binder, in LibTactics]
y1:176 [binder, in LibTactics]
y1:27 [binder, in Smallstep]
y1:59 [binder, in LibTactics]
y1:60 [binder, in LibTactics]
y1:65 [binder, in UseTactics]
y1:65 [binder, in LibTactics]
y1:72 [binder, in LibTactics]
y1:81 [binder, in LibTactics]
y1:92 [binder, in LibTactics]
y2:133 [binder, in LibTactics]
y2:138 [binder, in LibTactics]
y2:145 [binder, in LibTactics]
y2:154 [binder, in LibTactics]
y2:165 [binder, in LibTactics]
y2:178 [binder, in LibTactics]
y2:28 [binder, in Smallstep]
y2:66 [binder, in UseTactics]
y3:140 [binder, in LibTactics]
y3:147 [binder, in LibTactics]
y3:156 [binder, in LibTactics]
y3:167 [binder, in LibTactics]
y3:180 [binder, in LibTactics]
y4:149 [binder, in LibTactics]
y4:158 [binder, in LibTactics]
y4:169 [binder, in LibTactics]
y4:182 [binder, in LibTactics]
y5:160 [binder, in LibTactics]
y5:171 [binder, in LibTactics]
y5:184 [binder, in LibTactics]
y6:173 [binder, in LibTactics]
y6:186 [binder, in LibTactics]
y7:188 [binder, in LibTactics]
y:113 [binder, in Norm]
y:117 [binder, in LibTactics]
y:126 [binder, in Equiv]
y:127 [binder, in Smallstep]
y:132 [binder, in Smallstep]
y:136 [binder, in Smallstep]
y:146 [binder, in Norm]
y:184 [binder, in UseAuto]
y:186 [binder, in UseAuto]
y:189 [binder, in UseAuto]
y:191 [binder, in UseAuto]
y:193 [binder, in LibTactics]
y:194 [binder, in UseAuto]
y:200 [binder, in UseAuto]
y:206 [binder, in UseAuto]
y:260 [binder, in References]
y:262 [binder, in References]
y:283 [binder, in LibTactics]
y:33 [binder, in Hoare]
y:36 [binder, in PE]
y:42 [binder, in UseTactics]
y:49 [binder, in UseTactics]
y:53 [binder, in StlcProp]
y:60 [binder, in UseTactics]
y:87 [binder, in PE]
y:96 [binder, in Records]
Z
zprop [definition, in Equiv]zprop_preserving [lemma, in Equiv]
z:128 [binder, in Smallstep]
z:137 [binder, in Smallstep]
z:187 [binder, in UseAuto]
z:195 [binder, in UseAuto]
z:201 [binder, in UseAuto]
z:207 [binder, in UseAuto]
z:263 [binder, in References]
z:43 [binder, in UseTactics]
z:61 [binder, in UseTactics]
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]
stlc:_ [notation, in Norm]
stlc:_ .snd [notation, in Norm]
stlc:_ .fst [notation, in Norm]
stlc:_ * _ [notation, in Norm]
stlc:_ _ [notation, in Norm]
stlc:_ -> _ [notation, in Norm]
stlc:Bool [notation, in Norm]
stlc:false [notation, in Norm]
stlc:if _ then _ else _ [notation, in Norm]
stlc:true [notation, in Norm]
stlc:( _ , _ ) [notation, in Norm]
stlc:( _ ) [notation, in Norm]
stlc:[ _ := _ ] _ [notation, in Norm]
stlc:\ _ : _ , _ [notation, in Norm]
stlc:{ _ } [notation, in Norm]
_ * _ (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]
>> _ _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ (ltac_scope) [notation, in LibTactics]
>> _ (ltac_scope) [notation, in LibTactics]
>> (ltac_scope) [notation, in LibTactics]
___ (ltac_scope) [notation, in LibTactics]
__ (ltac_scope) [notation, in LibTactics]
_ / _ --> _ / _ [notation, in Smallstep]
_ / _ -->b _ [notation, in Smallstep]
_ / _ -->a _ [notation, in Smallstep]
_ -->* _ [notation, in Smallstep]
_ --> _ [notation, in Smallstep]
_ ==> _ [notation, in Smallstep]
_ [ _ ⊢> _ ] [notation, in Hoare]
_ <- _ ;; _ [notation, in Typechecking]
_ ⊢ _ ∈ _ [notation, in Norm]
_ -->* _ [notation, in Norm]
_ --> _ [notation, in Norm]
_ =' _ [notation, in LibTactics]
_ / _ / _ ==> _ [notation, in PE]
_ / _ ==> _ / _ [notation, in PE]
fail [notation, in Typechecking]
false [notation, in Norm]
nosimpl _ [notation, in LibTactics]
Register _ _ [notation, in LibTactics]
return _ [notation, in Typechecking]
Something [notation, in LibTactics]
true [notation, in Norm]
<{ _ }> [notation, in Norm]
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:_ ; _ [in Equiv]
com:_ := _ [in Equiv]
com:havoc _ [in Hoare]
com:havoc _ [in Equiv]
com:if _ then _ else _ end [in Hoare]
com:if _ then _ else _ end [in Equiv]
com:skip [in Hoare]
com:skip [in Equiv]
com:while _ do _ end [in Hoare]
com:while _ do _ end [in Equiv]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]
_ =[ _ ]=> _ [in Equiv]
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]
I
com:_ ; _ [in Hoare]com:_ := _ [in Hoare]
com:if _ then _ else _ end [in Hoare]
com:if1 _ then _ end [in Hoare]
com:skip [in Hoare]
com:while _ do _ end [in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]
L
_ / _ / _ / _ ==> _ # _ [in PE]_ / _ ==> _ # _ [in PE]
_ / _ ==> _ / _ / _ [in PE]
R
stlc_ty:Top [in RecordSub]stlc_ty:nil [in RecordSub]
stlc_ty:_ : _ :: _ [in RecordSub]
stlc_ty:Base _ [in RecordSub]
stlc_ty:_ -> _ [in RecordSub]
stlc_ty:_ [in RecordSub]
stlc_ty:( _ ) [in RecordSub]
stlc:_ [in RecordSub]
stlc:_ --> _ [in RecordSub]
stlc:_ := _ :: _ [in RecordSub]
stlc:_ _ [in RecordSub]
stlc:nil [in RecordSub]
stlc:( _ ) [in RecordSub]
stlc:[ _ := _ ] _ [in RecordSub]
stlc:\ _ : _ , _ [in RecordSub]
stlc:{ _ } [in RecordSub]
_ ⊢ _ ∈ _ [in RecordSub]
_ <: _ [in RecordSub]
_ --> _ [in RecordSub]
<{ _ }> [in RecordSub]
<{{ _ }}> [in RecordSub]
com:_ ; _ [in Hoare]
com:_ := _ [in Hoare]
com:if _ then _ else _ end [in Hoare]
com:repeat _ until _ end [in Hoare]
com:skip [in Hoare]
com:while _ do _ end [in Hoare]
_ =[ _ ]=> _ [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_ty:nil [in Records]
stlc_ty:_ : _ :: _ [in Records]
stlc_ty:Base _ [in Records]
stlc_ty:_ -> _ [in Records]
stlc_ty:_ [in Records]
stlc_ty:( _ ) [in Records]
stlc:_ [in Records]
stlc:_ --> _ [in Records]
stlc:_ := _ :: _ [in Records]
stlc:_ _ [in Records]
stlc:nil [in Records]
stlc:( _ ) [in Records]
stlc:[ _ := _ ] _ [in Records]
stlc:\ _ : _ , _ [in Records]
stlc:{ _ } [in Records]
_ ⊢ _ ∈ _ [in Records]
_ -->* _ [in Records]
_ --> _ [in Records]
<{ _ }> [in Records]
<{{ _ }}> [in Records]
stlc_ty:Unit [in MoreStlc]
stlc_ty:List _ [in MoreStlc]
stlc_ty:_ * _ [in MoreStlc]
stlc_ty:_ + _ [in MoreStlc]
stlc_ty:Nat [in MoreStlc]
stlc_ty:_ -> _ [in MoreStlc]
stlc_ty:_ [in MoreStlc]
stlc_ty:( _ ) [in MoreStlc]
stlc:_ [in MoreStlc]
stlc:_ :: _ [in MoreStlc]
stlc:_ .snd [in MoreStlc]
stlc:_ .fst [in MoreStlc]
stlc:_ * _ [in MoreStlc]
stlc:_ _ [in MoreStlc]
stlc:case _ of | nil => _ | _ :: _ => _ [in MoreStlc]
stlc:case _ of | inl _ => _ | inr _ => _ [in MoreStlc]
stlc:fix _ [in MoreStlc]
stlc:if0 _ then _ else _ [in MoreStlc]
stlc:inl _ _ [in MoreStlc]
stlc:inr _ _ [in MoreStlc]
stlc:let _ = _ in _ [in MoreStlc]
stlc:nil _ [in MoreStlc]
stlc:pred _ [in MoreStlc]
stlc:succ _ [in MoreStlc]
stlc:unit [in MoreStlc]
stlc:( _ , _ ) [in MoreStlc]
stlc:( _ ) [in MoreStlc]
stlc:[ _ := _ ] _ [in MoreStlc]
stlc:\ _ : _ , _ [in MoreStlc]
stlc:{ _ } [in MoreStlc]
_ ⊢ _ ∈ _ [in MoreStlc]
_ -->* _ [in MoreStlc]
_ --> _ [in MoreStlc]
<{ _ }> [in MoreStlc]
<{{ _ }}> [in MoreStlc]
_ / _ -->+ _ / _ [in References]
stlc:_ [in References]
stlc:_ ; _ [in References]
stlc:_ := _ [in References]
stlc:_ * _ [in References]
stlc:_ _ [in References]
stlc:_ -> _ [in References]
stlc:if0 _ then _ else _ [in References]
stlc:loc _ [in References]
stlc:Nat [in References]
stlc:pred _ [in References]
stlc:ref _ [in References]
stlc:Ref _ [in References]
stlc:succ _ [in References]
stlc:unit [in References]
stlc:Unit [in References]
stlc:! _ [in References]
stlc:( _ ) [in References]
stlc:[ _ := _ ] _ [in References]
stlc:\ _ : _ , _ [in References]
stlc:{ _ } [in References]
_ ; _ ⊢ _ ∈ _ [in References]
_ / _ -->* _ / _ [in References]
_ / _ --> _ / _ [in References]
<{ _ }> [in References]
stlc:_ [in Sub]
stlc:_ .snd [in Sub]
stlc:_ .fst [in Sub]
stlc:_ * _ [in Sub]
stlc:_ _ [in Sub]
stlc:_ -> _ [in Sub]
stlc:Base _ [in Sub]
stlc:Bool [in Sub]
stlc:false [in Sub]
stlc:if _ then _ else _ [in Sub]
stlc:Top [in Sub]
stlc:true [in Sub]
stlc:unit [in Sub]
stlc:Unit [in Sub]
stlc:( _ , _ ) [in Sub]
stlc:( _ ) [in Sub]
stlc:[ _ := _ ] _ [in Sub]
stlc:\ _ : _ , _ [in Sub]
stlc:{ _ } [in Sub]
_ ⊢ _ ∈ _ [in Sub]
_ <: _ [in Sub]
_ --> _ [in Sub]
false [in Sub]
true [in Sub]
<{ _ }> [in Sub]
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]
stlc:_ [in Norm]
stlc:_ .snd [in Norm]
stlc:_ .fst [in Norm]
stlc:_ * _ [in Norm]
stlc:_ _ [in Norm]
stlc:_ -> _ [in Norm]
stlc:Bool [in Norm]
stlc:false [in Norm]
stlc:if _ then _ else _ [in Norm]
stlc:true [in Norm]
stlc:( _ , _ ) [in Norm]
stlc:( _ ) [in Norm]
stlc:[ _ := _ ] _ [in Norm]
stlc:\ _ : _ , _ [in Norm]
stlc:{ _ } [in Norm]
_ * _ (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]
>> _ _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ (ltac_scope) [in LibTactics]
>> _ _ (ltac_scope) [in LibTactics]
>> _ (ltac_scope) [in LibTactics]
>> (ltac_scope) [in LibTactics]
___ (ltac_scope) [in LibTactics]
__ (ltac_scope) [in LibTactics]
_ / _ --> _ / _ [in Smallstep]
_ / _ -->b _ [in Smallstep]
_ / _ -->a _ [in Smallstep]
_ -->* _ [in Smallstep]
_ --> _ [in Smallstep]
_ ==> _ [in Smallstep]
_ [ _ ⊢> _ ] [in Hoare]
_ <- _ ;; _ [in Typechecking]
_ ⊢ _ ∈ _ [in Norm]
_ -->* _ [in Norm]
_ --> _ [in Norm]
_ =' _ [in LibTactics]
_ / _ / _ ==> _ [in PE]
_ / _ ==> _ / _ [in PE]
fail [in Typechecking]
false [in Norm]
nosimpl _ [in LibTactics]
Register _ _ [in LibTactics]
return _ [in Typechecking]
Something [in LibTactics]
true [in Norm]
<{ _ }> [in Norm]
Binder Index
A
atrans:91 [in Equiv]a':64 [in Equiv]
a1':136 [in PE]
a1':195 [in Smallstep]
a1':203 [in Smallstep]
a1':210 [in PE]
a1':211 [in Smallstep]
a1':222 [in Smallstep]
a1':230 [in Smallstep]
a1':250 [in Smallstep]
a1':282 [in Smallstep]
a1:1 [in Equiv]
a1:120 [in Equiv]
a1:125 [in Hoare]
a1:127 [in Equiv]
a1:129 [in Equiv]
a1:131 [in Equiv]
a1:131 [in PE]
a1:135 [in PE]
a1:16 [in PE]
a1:173 [in Hoare]
a1:179 [in Equiv]
a1:194 [in Smallstep]
a1:202 [in Smallstep]
a1:205 [in PE]
a1:209 [in PE]
a1:210 [in Smallstep]
a1:210 [in Hoare]
a1:221 [in Smallstep]
a1:229 [in Smallstep]
a1:249 [in Smallstep]
a1:265 [in Hoare]
a1:281 [in Smallstep]
a1:324 [in PE]
a1:45 [in Equiv]
a1:47 [in Equiv]
a2':199 [in Smallstep]
a2':207 [in Smallstep]
a2':215 [in Smallstep]
a2':226 [in Smallstep]
a2':234 [in Smallstep]
a2:121 [in Equiv]
a2:128 [in Equiv]
a2:130 [in Equiv]
a2:132 [in Equiv]
a2:17 [in PE]
a2:180 [in Equiv]
a2:196 [in Smallstep]
a2:198 [in Smallstep]
a2:2 [in Equiv]
a2:204 [in Smallstep]
a2:206 [in Smallstep]
a2:212 [in Smallstep]
a2:214 [in Smallstep]
a2:223 [in Smallstep]
a2:225 [in Smallstep]
a2:231 [in Smallstep]
a2:233 [in Smallstep]
a2:46 [in Equiv]
a2:48 [in Equiv]
a3:49 [in Equiv]
a:10 [in Hoare]
a:10 [in PE]
a:106 [in Hoare]
a:106 [in Equiv]
a:108 [in Hoare]
A:108 [in LibTactics]
a:11 [in HoareAsLogic]
A:112 [in LibTactics]
a:115 [in Equiv]
A:117 [in UseAuto]
a:135 [in Equiv]
A:14 [in PE]
a:143 [in Equiv]
A:16 [in LibTactics]
a:162 [in Hoare]
A:17 [in LibTactics]
a:18 [in PE]
A:20 [in LibTactics]
a:208 [in UseAuto]
A:21 [in References]
a:21 [in PE]
a:211 [in UseAuto]
a:216 [in UseAuto]
A:237 [in References]
A:25 [in LibTactics]
A:27 [in LibTactics]
A:28 [in References]
a:29 [in LibTactics]
A:3 [in LibTactics]
a:30 [in LibTactics]
a:30 [in PE]
A:31 [in References]
a:31 [in LibTactics]
a:317 [in Hoare]
a:32 [in LibTactics]
a:42 [in UseAuto]
a:43 [in UseAuto]
a:43 [in Equiv]
a:44 [in UseTactics]
a:44 [in Equiv]
a:46 [in UseTactics]
a:46 [in PE]
a:51 [in Hoare2]
a:51 [in UseTactics]
a:53 [in Hoare2]
a:55 [in Hoare]
a:60 [in Hoare]
a:63 [in Equiv]
a:64 [in Hoare]
a:68 [in Hoare]
a:7 [in Hoare2]
a:72 [in Hoare2]
a:73 [in Typechecking]
a:74 [in Hoare2]
a:76 [in Hoare2]
a:79 [in Hoare2]
A:8 [in PE]
a:84 [in UseTactics]
a:85 [in UseTactics]
a:92 [in Equiv]
a:95 [in Hoare2]
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':238 [in Smallstep]
b1':240 [in Smallstep]
b1':263 [in Smallstep]
b1':295 [in Smallstep]
b1:148 [in PE]
b1:154 [in PE]
b1:161 [in PE]
b1:223 [in PE]
b1:230 [in PE]
b1:237 [in Smallstep]
b1:238 [in PE]
b1:239 [in Smallstep]
b1:245 [in PE]
b1:250 [in PE]
b1:258 [in PE]
b1:262 [in Smallstep]
b1:264 [in PE]
b1:269 [in PE]
b1:273 [in Smallstep]
b1:276 [in PE]
b1:294 [in Smallstep]
b1:305 [in Smallstep]
b1:336 [in PE]
b1:342 [in PE]
b1:346 [in PE]
b1:352 [in PE]
b1:4 [in Equiv]
b1:51 [in Equiv]
b1:53 [in Equiv]
b2':243 [in Smallstep]
b2:241 [in Smallstep]
b2:242 [in Smallstep]
b2:244 [in Smallstep]
b2:5 [in Equiv]
b2:52 [in Equiv]
b2:54 [in Equiv]
b3:55 [in Equiv]
b:100 [in Equiv]
B:107 [in LibTactics]
b:108 [in Equiv]
b:110 [in Hoare]
b:112 [in Hoare]
B:113 [in LibTactics]
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:153 [in Equiv]
b:158 [in Equiv]
b:161 [in Equiv]
b:164 [in Hoare]
b:167 [in Equiv]
b:183 [in Hoare]
b:188 [in Hoare]
b:19 [in Equiv]
b:19 [in HoareAsLogic]
b:191 [in Hoare]
b:197 [in Hoare]
b:22 [in Equiv]
b:220 [in Hoare]
b:225 [in Hoare]
b:228 [in Hoare]
b:234 [in Hoare]
b:25 [in Equiv]
b:25 [in HoareAsLogic]
b:278 [in Hoare]
b:28 [in Equiv]
b:283 [in Hoare]
b:286 [in Hoare]
b:292 [in Hoare]
b:295 [in Hoare]
b:298 [in Hoare]
b:30 [in Equiv]
b:300 [in Hoare]
b:302 [in Hoare]
b:310 [in Hoare]
b:313 [in Hoare]
b:336 [in Hoare]
b:34 [in Equiv]
b:340 [in Hoare]
b:36 [in Equiv]
b:45 [in UseTactics]
b:47 [in UseTactics]
b:49 [in PE]
b:50 [in Equiv]
b:52 [in Hoare2]
b:52 [in UseTactics]
b:52 [in PE]
b:54 [in Hoare2]
b:54 [in PE]
b:65 [in Equiv]
b:67 [in UseTactics]
b:68 [in HoareAsLogic]
b:69 [in Equiv]
b:72 [in Typechecking]
b:73 [in Hoare2]
b:75 [in Hoare2]
b:75 [in Equiv]
b:77 [in Hoare2]
b:80 [in Hoare2]
b:85 [in Equiv]
b:9 [in Hoare2]
b:94 [in Equiv]
C
ctrans:95 [in Equiv]c'':220 [in PE]
c'':227 [in PE]
c'':234 [in PE]
c'':243 [in PE]
c'':372 [in PE]
c'':382 [in PE]
c'':391 [in PE]
c'':399 [in PE]
c':16 [in Types]
c':176 [in PE]
c':186 [in PE]
c':188 [in Equiv]
c':192 [in PE]
c':198 [in PE]
c':370 [in PE]
c':380 [in PE]
c':390 [in PE]
c':398 [in PE]
c':406 [in PE]
c':68 [in Equiv]
c':72 [in Equiv]
c':78 [in Equiv]
c1':144 [in PE]
c1':151 [in PE]
c1':164 [in PE]
c1':218 [in PE]
c1':226 [in PE]
c1':241 [in PE]
c1':252 [in PE]
c1':256 [in Smallstep]
c1':260 [in PE]
c1':271 [in PE]
c1':278 [in PE]
c1':288 [in Smallstep]
c1':309 [in Smallstep]
c1':82 [in Equiv]
c1':88 [in Equiv]
c1:11 [in Equiv]
c1:117 [in Hoare]
c1:128 [in Hoare]
c1:136 [in Hoare]
c1:141 [in Hoare]
c1:142 [in PE]
c1:146 [in Equiv]
c1:149 [in PE]
c1:154 [in Equiv]
c1:155 [in PE]
c1:159 [in Equiv]
c1:162 [in PE]
c1:169 [in Equiv]
c1:17 [in Equiv]
c1:176 [in Hoare]
c1:181 [in Equiv]
c1:184 [in Hoare]
c1:189 [in Hoare]
c1:20 [in Equiv]
c1:20 [in HoareAsLogic]
c1:213 [in Hoare]
c1:216 [in PE]
c1:221 [in Hoare]
c1:224 [in PE]
c1:226 [in Hoare]
c1:23 [in Equiv]
c1:231 [in PE]
c1:239 [in PE]
c1:246 [in PE]
c1:251 [in PE]
c1:255 [in Smallstep]
c1:259 [in PE]
c1:26 [in Equiv]
c1:264 [in Smallstep]
c1:265 [in PE]
c1:267 [in Smallstep]
c1:268 [in Hoare]
c1:270 [in Smallstep]
c1:270 [in PE]
c1:273 [in Hoare]
c1:274 [in Smallstep]
c1:277 [in PE]
c1:279 [in Hoare]
c1:284 [in Hoare]
c1:287 [in Smallstep]
c1:296 [in Smallstep]
c1:299 [in Smallstep]
c1:302 [in Smallstep]
c1:306 [in Smallstep]
c1:308 [in Smallstep]
c1:313 [in Smallstep]
c1:327 [in PE]
c1:331 [in Hoare]
c1:337 [in Hoare]
c1:337 [in PE]
c1:343 [in PE]
c1:348 [in PE]
c1:353 [in PE]
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'':254 [in PE]
c2'':262 [in PE]
c2':145 [in PE]
c2':157 [in PE]
c2':165 [in PE]
c2':219 [in PE]
c2':233 [in PE]
c2':242 [in PE]
c2':253 [in PE]
c2':261 [in PE]
c2':272 [in PE]
c2':279 [in PE]
c2':315 [in Smallstep]
c2':84 [in Equiv]
c2':90 [in Equiv]
c2:118 [in Hoare]
c2:12 [in Equiv]
c2:129 [in Hoare]
c2:137 [in Hoare]
c2:142 [in Hoare]
c2:143 [in PE]
c2:147 [in Equiv]
c2:150 [in PE]
c2:155 [in Equiv]
c2:156 [in PE]
c2:160 [in Equiv]
c2:163 [in PE]
c2:170 [in Equiv]
c2:177 [in Hoare]
c2:18 [in Equiv]
c2:182 [in Equiv]
c2:185 [in Hoare]
c2:190 [in Hoare]
c2:21 [in Equiv]
c2:21 [in HoareAsLogic]
c2:214 [in Hoare]
c2:217 [in PE]
c2:222 [in Hoare]
c2:225 [in PE]
c2:227 [in Hoare]
c2:232 [in PE]
c2:24 [in Equiv]
c2:240 [in PE]
c2:258 [in Smallstep]
c2:260 [in Smallstep]
c2:265 [in Smallstep]
c2:268 [in Smallstep]
c2:269 [in Hoare]
c2:27 [in Equiv]
c2:271 [in Smallstep]
c2:274 [in Hoare]
c2:280 [in Hoare]
c2:285 [in Hoare]
c2:290 [in Smallstep]
c2:292 [in Smallstep]
c2:297 [in Smallstep]
c2:300 [in Smallstep]
c2:303 [in Smallstep]
c2:310 [in Smallstep]
c2:314 [in Smallstep]
c2:328 [in PE]
c2:332 [in Hoare]
c2:338 [in Hoare]
c2:338 [in PE]
c2:344 [in PE]
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:1 [in UseTactics]
c:101 [in Hoare]
c:103 [in Equiv]
c:105 [in Hoare]
c:11 [in UseTactics]
c:110 [in Equiv]
c:112 [in Equiv]
c:119 [in PE]
c:13 [in HoareAsLogic]
c:145 [in Hoare]
c:15 [in Types]
c:15 [in Equiv]
c:150 [in Hoare]
c:152 [in Hoare]
c:159 [in Hoare]
c:16 [in Equiv]
c:163 [in Equiv]
c:165 [in Hoare]
c:166 [in PE]
c:168 [in Equiv]
c:168 [in PE]
c:170 [in PE]
c:172 [in PE]
c:174 [in PE]
c:183 [in PE]
c:185 [in Equiv]
c:186 [in Equiv]
c:187 [in Equiv]
c:189 [in PE]
c:193 [in Hoare]
c:195 [in PE]
c:198 [in Hoare]
c:2 [in HoareAsLogic]
c:200 [in Hoare]
c:203 [in Norm]
c:21 [in UseTactics]
c:22 [in UseTactics]
c:230 [in Hoare]
c:235 [in Hoare]
c:240 [in Hoare]
c:241 [in Norm]
c:243 [in Norm]
c:247 [in Hoare]
c:247 [in Norm]
c:252 [in Norm]
c:254 [in Norm]
c:259 [in Norm]
c:26 [in UseTactics]
c:26 [in HoareAsLogic]
c:265 [in Norm]
c:270 [in Norm]
c:280 [in PE]
c:282 [in PE]
c:284 [in PE]
c:286 [in PE]
c:288 [in Hoare]
c:288 [in PE]
c:29 [in Equiv]
c:290 [in PE]
c:292 [in PE]
c:293 [in Hoare]
c:294 [in PE]
c:296 [in Hoare]
c:296 [in PE]
c:298 [in PE]
c:30 [in UseTactics]
c:300 [in PE]
c:302 [in PE]
c:304 [in Hoare]
c:304 [in PE]
c:306 [in PE]
c:308 [in PE]
c:31 [in Equiv]
c:310 [in PE]
c:312 [in PE]
c:314 [in PE]
c:316 [in PE]
c:318 [in PE]
c:321 [in Hoare]
c:325 [in Hoare]
c:33 [in HoareAsLogic]
c:341 [in Hoare]
c:35 [in Equiv]
c:356 [in PE]
c:36 [in Hoare]
c:360 [in PE]
c:37 [in Equiv]
c:387 [in PE]
c:39 [in HoareAsLogic]
c:395 [in PE]
c:403 [in PE]
c:42 [in Hoare]
c:44 [in HoareAsLogic]
c:46 [in Hoare]
c:48 [in HoareAsLogic]
c:50 [in HoareAsLogic]
c:53 [in UseTactics]
c:53 [in HoareAsLogic]
c:55 [in HoareAsLogic]
c:56 [in Equiv]
c:59 [in HoareAsLogic]
c:61 [in HoareAsLogic]
c:66 [in UseAuto]
c:67 [in Equiv]
c:69 [in HoareAsLogic]
c:70 [in UseAuto]
c:71 [in Equiv]
c:72 [in HoareAsLogic]
c:74 [in UseAuto]
c:76 [in Hoare]
c:77 [in Equiv]
c:78 [in UseAuto]
c:78 [in Hoare2]
c:80 [in Hoare]
c:81 [in Hoare2]
c:82 [in UseAuto]
c:85 [in Hoare]
c:86 [in UseTactics]
c:89 [in Hoare]
c:90 [in Hoare2]
c:90 [in UseTactics]
c:93 [in Hoare]
c:96 [in Equiv]
c:97 [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:120 [in UseAuto]
D:14 [in LibTactics]
d:15 [in HoareAsLogic]
d:17 [in Hoare2]
D:18 [in LibTactics]
d:20 [in Hoare2]
d:21 [in Hoare2]
d:240 [in References]
d:25 [in Hoare2]
d:32 [in Hoare2]
d:39 [in Hoare2]
d:42 [in Hoare2]
d:54 [in UseTactics]
E
env:225 [in Norm]env:228 [in Norm]
env:260 [in Norm]
env:271 [in Norm]
eqb:15 [in PE]
eqb:9 [in PE]
e':350 [in Smallstep]
e':351 [in Smallstep]
e':352 [in Smallstep]
e:204 [in Norm]
e:248 [in Norm]
e:253 [in Norm]
e:255 [in Norm]
e:266 [in Norm]
e:278 [in LibTactics]
e:279 [in LibTactics]
e:280 [in LibTactics]
e:281 [in LibTactics]
e:43 [in StlcProp]
e:55 [in UseTactics]
F
F':13 [in UseAuto]F':15 [in UseAuto]
F':31 [in UseAuto]
F':33 [in UseAuto]
F1:34 [in UseAuto]
F2:35 [in UseAuto]
F3:36 [in UseAuto]
F:10 [in UseAuto]
F:12 [in UseAuto]
f:126 [in LibTactics]
f:129 [in LibTactics]
f:134 [in LibTactics]
F:14 [in UseAuto]
f:141 [in LibTactics]
f:150 [in LibTactics]
f:161 [in LibTactics]
f:174 [in LibTactics]
f:188 [in Sub]
F:19 [in UseAuto]
f:192 [in Sub]
f:196 [in UseAuto]
f:202 [in UseAuto]
f:209 [in UseAuto]
f:212 [in UseAuto]
F:27 [in UseAuto]
f:27 [in Hoare]
F:30 [in UseAuto]
f:31 [in Hoare]
F:32 [in UseAuto]
f:37 [in UseAuto]
f:39 [in UseAuto]
f:48 [in UseAuto]
f:50 [in UseTactics]
f:56 [in UseTactics]
G
Gamma':115 [in Records]Gamma':118 [in Sub]
Gamma':14 [in StlcProp]
Gamma':141 [in Norm]
Gamma':172 [in RecordSub]
Gamma':172 [in MoreStlc]
Gamma':209 [in References]
Gamma':75 [in StlcProp]
Gamma':88 [in Norm]
Gamma':95 [in StlcProp]
Gamma:101 [in Sub]
Gamma:103 [in Records]
Gamma:105 [in Sub]
Gamma:109 [in MoreStlc]
Gamma:110 [in Sub]
Gamma:111 [in RecordSub]
Gamma:112 [in MoreStlc]
Gamma:114 [in RecordSub]
Gamma:114 [in Records]
Gamma:117 [in Sub]
Gamma:118 [in Records]
Gamma:119 [in MoreStlc]
Gamma:121 [in RecordSub]
Gamma:121 [in Records]
Gamma:121 [in Sub]
Gamma:122 [in MoreStlc]
Gamma:124 [in RecordSub]
Gamma:124 [in MoreStlc]
Gamma:124 [in Sub]
Gamma:126 [in MoreStlc]
Gamma:128 [in References]
Gamma:128 [in MoreStlc]
Gamma:129 [in RecordSub]
Gamma:13 [in Typechecking]
Gamma:13 [in StlcProp]
Gamma:131 [in References]
Gamma:131 [in MoreStlc]
Gamma:133 [in RecordSub]
Gamma:134 [in RecordSub]
Gamma:136 [in MoreStlc]
Gamma:138 [in References]
Gamma:140 [in RecordSub]
Gamma:140 [in MoreStlc]
Gamma:140 [in Norm]
Gamma:141 [in References]
Gamma:143 [in References]
Gamma:144 [in MoreStlc]
Gamma:145 [in References]
Gamma:147 [in References]
Gamma:150 [in References]
Gamma:150 [in RecordSub]
Gamma:150 [in Norm]
Gamma:153 [in MoreStlc]
Gamma:155 [in References]
Gamma:155 [in MoreStlc]
Gamma:156 [in References]
Gamma:158 [in References]
Gamma:159 [in MoreStlc]
Gamma:160 [in RecordSub]
Gamma:161 [in References]
Gamma:164 [in References]
Gamma:167 [in MoreStlc]
Gamma:17 [in StlcProp]
Gamma:171 [in RecordSub]
Gamma:171 [in MoreStlc]
Gamma:175 [in RecordSub]
Gamma:175 [in MoreStlc]
Gamma:178 [in RecordSub]
Gamma:178 [in MoreStlc]
Gamma:184 [in Norm]
Gamma:20 [in StlcProp]
Gamma:208 [in References]
Gamma:213 [in References]
Gamma:217 [in References]
Gamma:228 [in References]
Gamma:244 [in Norm]
Gamma:25 [in Typechecking]
Gamma:26 [in StlcProp]
Gamma:267 [in Norm]
Gamma:28 [in Typechecking]
Gamma:39 [in Typechecking]
Gamma:42 [in StlcProp]
Gamma:45 [in Stlc]
Gamma:48 [in Stlc]
Gamma:48 [in Sub]
Gamma:51 [in Sub]
Gamma:54 [in Norm]
Gamma:55 [in Stlc]
Gamma:57 [in Norm]
Gamma:58 [in Stlc]
Gamma:58 [in Sub]
Gamma:59 [in Stlc]
Gamma:61 [in Sub]
Gamma:62 [in Sub]
Gamma:63 [in Typechecking]
Gamma:64 [in Stlc]
Gamma:64 [in Norm]
Gamma:66 [in Typechecking]
Gamma:67 [in Norm]
Gamma:67 [in Sub]
Gamma:68 [in Norm]
Gamma:68 [in Sub]
Gamma:69 [in Sub]
Gamma:70 [in StlcProp]
Gamma:72 [in UseTactics]
Gamma:73 [in Norm]
Gamma:73 [in Records]
Gamma:74 [in StlcProp]
Gamma:74 [in Norm]
Gamma:79 [in Norm]
Gamma:83 [in Norm]
Gamma:83 [in Sub]
Gamma:87 [in Norm]
Gamma:9 [in Typechecking]
Gamma:90 [in Sub]
Gamma:91 [in Norm]
Gamma:94 [in StlcProp]
Gamma:94 [in UseTactics]
Gamma:94 [in Norm]
Gamma:95 [in Sub]
G:102 [in UseTactics]
g:197 [in UseAuto]
g:203 [in UseAuto]
g:210 [in UseAuto]
g:213 [in UseAuto]
g:40 [in UseAuto]
g:49 [in UseAuto]
G:99 [in UseTactics]
H
HT:199 [in Sub]h:198 [in UseAuto]
h:204 [in UseAuto]
h:214 [in UseAuto]
I
ids:100 [in PE]ids:109 [in PE]
ids:113 [in PE]
ids:117 [in PE]
ids:125 [in PE]
ids:96 [in PE]
i1:89 [in RecordSub]
i2:90 [in RecordSub]
i:10 [in Records]
i:101 [in RecordSub]
i:108 [in Records]
i:12 [in RecordSub]
i:125 [in RecordSub]
i:135 [in RecordSub]
i:147 [in RecordSub]
i:15 [in Records]
i:17 [in RecordSub]
i:18 [in Records]
i:189 [in Sub]
i:191 [in Sub]
i:193 [in Smallstep]
i:193 [in Sub]
i:195 [in Sub]
i:20 [in RecordSub]
i:23 [in Records]
i:248 [in Smallstep]
i:252 [in Smallstep]
i:280 [in Smallstep]
i:284 [in Smallstep]
i:33 [in RecordSub]
i:334 [in Smallstep]
i:36 [in RecordSub]
i:36 [in Records]
i:39 [in Records]
i:40 [in RecordSub]
i:57 [in Records]
i:58 [in RecordSub]
i:59 [in Records]
i:60 [in RecordSub]
i:61 [in Records]
i:62 [in RecordSub]
i:65 [in Records]
i:66 [in RecordSub]
i:69 [in Records]
i:7 [in RecordSub]
i:81 [in RecordSub]
i:84 [in RecordSub]
i:86 [in Records]
i:90 [in Records]
i:96 [in RecordSub]
i:98 [in Records]
J
j:190 [in Sub]j:194 [in Sub]
K
k:189 [in Norm]k:417 [in PE]
k:431 [in PE]
k:442 [in PE]
k:448 [in PE]
k:53 [in UseAuto]
k:55 [in UseAuto]
k:57 [in UseAuto]
k:59 [in UseAuto]
k:60 [in UseAuto]
k:62 [in UseAuto]
k:63 [in UseAuto]
L
Label:410 [in PE]l'':435 [in PE]
l':433 [in PE]
l':451 [in PE]
l':462 [in PE]
l':473 [in PE]
l1:177 [in Equiv]
l1:38 [in References]
l2:178 [in Equiv]
l2:39 [in References]
l:104 [in References]
l:11 [in References]
l:11 [in PE]
l:110 [in References]
l:118 [in UseAuto]
l:133 [in PE]
l:137 [in PE]
l:157 [in References]
l:176 [in References]
l:19 [in PE]
l:190 [in Norm]
l:192 [in References]
l:195 [in References]
l:207 [in PE]
l:211 [in PE]
l:226 [in References]
l:238 [in References]
l:24 [in References]
l:326 [in PE]
l:34 [in References]
l:35 [in References]
L:415 [in PE]
L:420 [in PE]
l:421 [in PE]
L:423 [in PE]
l:428 [in PE]
l:430 [in PE]
L:440 [in PE]
L:445 [in PE]
L:452 [in PE]
L:456 [in PE]
l:460 [in PE]
L:467 [in PE]
l:471 [in PE]
l:84 [in PE]
l:88 [in PE]
M
m:107 [in UseTactics]m:150 [in UseAuto]
m:153 [in UseAuto]
m:21 [in UseAuto]
m:33 [in UseTactics]
m:338 [in Smallstep]
m:342 [in Smallstep]
m:346 [in Smallstep]
m:35 [in UseTactics]
m:37 [in UseTactics]
m:47 [in Hoare2]
m:49 [in Hoare2]
m:55 [in Hoare2]
m:57 [in Hoare2]
m:59 [in Hoare2]
m:60 [in Hoare2]
m:63 [in Hoare]
m:64 [in Hoare2]
m:67 [in Hoare2]
m:68 [in Hoare2]
m:69 [in Hoare2]
m:70 [in Hoare2]
m:71 [in Hoare2]
m:72 [in Hoare]
m:79 [in UseTactics]
m:8 [in UseAuto]
m:81 [in UseTactics]
m:83 [in UseTactics]
N
ni:136 [in Equiv]nxs:195 [in Norm]
n':379 [in PE]
n':386 [in PE]
n1:132 [in PE]
n1:195 [in LibTactics]
n1:206 [in PE]
n1:332 [in PE]
n1:354 [in PE]
n1:43 [in MoreStlc]
n1:71 [in References]
n2:196 [in LibTactics]
n2:333 [in PE]
n2:355 [in PE]
n2:44 [in MoreStlc]
n2:72 [in References]
n:10 [in References]
n:100 [in UseAuto]
n:103 [in UseAuto]
n:103 [in Hoare2]
n:104 [in Hoare2]
n:105 [in Hoare2]
n:106 [in UseAuto]
n:106 [in UseTactics]
n:107 [in Hoare]
n:109 [in UseAuto]
n:109 [in Hoare]
n:11 [in UseAuto]
n:121 [in UseAuto]
n:123 [in References]
n:123 [in MoreStlc]
n:125 [in Equiv]
n:126 [in Hoare]
n:138 [in PE]
n:142 [in References]
n:144 [in Equiv]
n:149 [in UseAuto]
n:15 [in MoreStlc]
n:151 [in Smallstep]
n:152 [in UseAuto]
n:154 [in Smallstep]
n:157 [in Smallstep]
n:159 [in Smallstep]
n:164 [in Smallstep]
n:174 [in Hoare]
n:189 [in Smallstep]
n:19 [in References]
n:194 [in Norm]
n:197 [in Sub]
n:197 [in LibTactics]
n:20 [in UseAuto]
n:211 [in Hoare]
n:212 [in PE]
n:22 [in References]
n:238 [in Hoare]
n:24 [in UseAuto]
n:253 [in Smallstep]
n:256 [in Hoare]
n:266 [in Hoare]
n:27 [in PE]
n:28 [in UseAuto]
n:285 [in Smallstep]
n:29 [in UseAuto]
n:29 [in References]
n:3 [in UseAuto]
n:31 [in Smallstep]
n:32 [in References]
n:32 [in UseTactics]
n:320 [in Smallstep]
n:322 [in Smallstep]
n:325 [in Smallstep]
n:325 [in PE]
n:331 [in Smallstep]
n:337 [in Smallstep]
n:339 [in PE]
n:34 [in UseTactics]
n:341 [in Smallstep]
n:345 [in Smallstep]
n:345 [in PE]
n:359 [in PE]
n:36 [in UseTactics]
n:363 [in PE]
n:375 [in PE]
n:385 [in PE]
n:39 [in MoreStlc]
n:394 [in PE]
n:4 [in UseAuto]
n:402 [in PE]
n:42 [in MoreStlc]
n:48 [in Hoare2]
n:50 [in Hoare2]
n:55 [in Smallstep]
n:57 [in MoreStlc]
n:59 [in References]
n:65 [in UseAuto]
n:65 [in References]
n:65 [in PE]
n:68 [in PE]
n:69 [in UseTactics]
n:7 [in UseAuto]
n:7 [in PE]
n:70 [in UseTactics]
n:71 [in Smallstep]
n:71 [in UseTactics]
n:73 [in PE]
n:74 [in Smallstep]
n:77 [in PE]
n:78 [in UseTactics]
n:8 [in Smallstep]
n:80 [in UseTactics]
n:82 [in Hoare2]
n:82 [in UseTactics]
n:85 [in Hoare2]
n:86 [in Smallstep]
n:86 [in Hoare2]
n:87 [in Hoare2]
n:88 [in Hoare2]
n:9 [in Hoare]
n:93 [in References]
n:99 [in Hoare2]
P
pe_st:470 [in PE]pe_st':466 [in PE]
pe_st:459 [in PE]
pe_l:454 [in PE]
pe_st':450 [in PE]
pe_st:447 [in PE]
pe_st:441 [in PE]
pe_st':405 [in PE]
pe_st:404 [in PE]
pe_st':397 [in PE]
pe_st:396 [in PE]
pe_st':389 [in PE]
pe_st:388 [in PE]
pe_st':381 [in PE]
pe_st':371 [in PE]
pe_st2:368 [in PE]
pe_st1:367 [in PE]
pe_st2:365 [in PE]
pe_st1:364 [in PE]
pe_st'':275 [in PE]
pe_st':274 [in PE]
pe_st:273 [in PE]
pe_st'':268 [in PE]
pe_st':267 [in PE]
pe_st:266 [in PE]
pe_st:263 [in PE]
pe_st'':257 [in PE]
pe_st':256 [in PE]
pe_st:255 [in PE]
pe_st'':249 [in PE]
pe_st':248 [in PE]
pe_st:247 [in PE]
pe_st:244 [in PE]
pe_st2:237 [in PE]
pe_st1:236 [in PE]
pe_st:235 [in PE]
pe_st':229 [in PE]
pe_st:228 [in PE]
pe_st':222 [in PE]
pe_st:221 [in PE]
pe_st'':215 [in PE]
pe_st':214 [in PE]
pe_st:213 [in PE]
pe_st:208 [in PE]
pe_st:204 [in PE]
pe_st:203 [in PE]
pe_st':197 [in PE]
pe_st:196 [in PE]
pe_st':191 [in PE]
pe_st:190 [in PE]
pe_st':185 [in PE]
pe_st:184 [in PE]
pe_st':177 [in PE]
pe_st2:160 [in PE]
pe_st1:159 [in PE]
pe_st:158 [in PE]
pe_st':153 [in PE]
pe_st:152 [in PE]
pe_st':147 [in PE]
pe_st:146 [in PE]
pe_st'':141 [in PE]
pe_st':140 [in PE]
pe_st:139 [in PE]
pe_st:134 [in PE]
pe_st:130 [in PE]
pe_st:129 [in PE]
pe_st:124 [in PE]
pe_st:116 [in PE]
pe_st:112 [in PE]
pe_st:108 [in PE]
pe_st2:106 [in PE]
pe_st1:105 [in PE]
pe_st2:103 [in PE]
pe_st1:102 [in PE]
pe_st:99 [in PE]
pe_st:95 [in PE]
pe_st2:93 [in PE]
pe_st1:92 [in PE]
pe_st2:91 [in PE]
pe_st1:90 [in PE]
pe_st2:82 [in PE]
pe_st1:81 [in PE]
pe_st2:79 [in PE]
pe_st1:78 [in PE]
pe_st:75 [in PE]
pe_st:71 [in PE]
pe_st:66 [in PE]
pe_st:63 [in PE]
pe_st:60 [in PE]
pe_st:56 [in PE]
pe_st:53 [in PE]
pe_st:48 [in PE]
pe_st:45 [in PE]
pe_st:43 [in PE]
pe_st:41 [in PE]
pe_st:38 [in PE]
pe_st:32 [in PE]
pe_st:29 [in PE]
pe_st:25 [in PE]
pe_st:20 [in PE]
pe_st:5 [in PE]
pe_st:1 [in PE]
P':157 [in Hoare]
P':245 [in Hoare]
P':31 [in HoareAsLogic]
P':319 [in Hoare]
P':38 [in HoareAsLogic]
P':63 [in HoareAsLogic]
P':74 [in Hoare]
P':82 [in Hoare]
P':87 [in Hoare]
P':91 [in Hoare]
P':92 [in Hoare2]
P':95 [in Hoare]
P':99 [in Hoare]
P1:10 [in Hoare2]
P2:12 [in Hoare2]
P:1 [in UseAuto]
P:1 [in HoareAsLogic]
P:102 [in Hoare]
P:105 [in LibTactics]
P:109 [in LibTactics]
P:114 [in Hoare]
P:114 [in LibTactics]
P:12 [in HoareAsLogic]
P:133 [in Sub]
P:148 [in UseAuto]
P:151 [in UseAuto]
P:151 [in Hoare]
P:156 [in Hoare]
P:16 [in UseAuto]
P:16 [in Hoare2]
P:16 [in UseTactics]
P:163 [in Hoare]
P:17 [in HoareAsLogic]
P:19 [in Hoare2]
P:190 [in LibTactics]
p:191 [in LibTactics]
P:192 [in UseAuto]
P:198 [in LibTactics]
P:199 [in Hoare]
P:199 [in LibTactics]
P:22 [in UseAuto]
P:220 [in Sub]
P:239 [in Hoare]
P:24 [in LibTactics]
P:24 [in HoareAsLogic]
P:244 [in Hoare]
P:25 [in UseAuto]
P:253 [in Hoare]
P:277 [in LibTactics]
P:29 [in HoareAsLogic]
P:303 [in Hoare]
P:309 [in Hoare]
P:312 [in Hoare]
P:318 [in Hoare]
P:322 [in Hoare]
P:328 [in Hoare]
p:332 [in Smallstep]
P:333 [in Hoare]
P:334 [in Hoare]
p:335 [in Smallstep]
p:339 [in Smallstep]
P:339 [in Hoare]
p:343 [in Smallstep]
p:347 [in Smallstep]
P:35 [in Hoare]
P:36 [in HoareAsLogic]
P:38 [in Hoare2]
P:40 [in Hoare]
P:41 [in HoareAsLogic]
p:424 [in PE]
P:43 [in Hoare2]
P:44 [in UseAuto]
P:44 [in Hoare]
p:453 [in PE]
p:457 [in PE]
P:46 [in UseAuto]
p:468 [in PE]
P:48 [in Hoare]
P:49 [in Hoare]
P:49 [in HoareAsLogic]
P:5 [in UseAuto]
P:5 [in Hoare]
P:51 [in UseAuto]
P:52 [in UseAuto]
P:52 [in HoareAsLogic]
P:54 [in UseAuto]
P:55 [in LibTactics]
P:56 [in UseAuto]
P:56 [in Hoare]
p:56 [in Hoare2]
P:57 [in LibTactics]
P:58 [in UseAuto]
p:58 [in Hoare2]
P:58 [in UseTactics]
P:6 [in UseTactics]
P:61 [in UseAuto]
P:61 [in Hoare]
P:62 [in Hoare]
P:62 [in UseTactics]
P:62 [in LibTactics]
P:64 [in HoareAsLogic]
P:65 [in Hoare]
P:68 [in LibTactics]
P:69 [in Hoare]
P:71 [in HoareAsLogic]
P:73 [in Hoare]
P:76 [in LibTactics]
P:77 [in Hoare]
P:8 [in Hoare]
P:8 [in HoareAsLogic]
P:81 [in Hoare]
P:86 [in Hoare]
P:86 [in LibTactics]
P:89 [in Hoare2]
P:9 [in UseAuto]
P:90 [in Hoare]
P:94 [in Hoare]
P:96 [in Hoare2]
P:98 [in Hoare]
P:98 [in LibTactics]
Q
Q':104 [in Hoare]Q':32 [in HoareAsLogic]
Q':324 [in Hoare]
Q':43 [in HoareAsLogic]
Q':79 [in Hoare]
Q':84 [in Hoare]
Q:100 [in Hoare]
Q:103 [in Hoare]
Q:106 [in LibTactics]
Q:110 [in LibTactics]
Q:115 [in Hoare]
Q:115 [in LibTactics]
Q:14 [in Hoare2]
Q:14 [in HoareAsLogic]
Q:153 [in Hoare]
Q:158 [in Hoare]
Q:160 [in Hoare]
Q:166 [in Hoare]
Q:17 [in UseAuto]
Q:17 [in UseTactics]
Q:18 [in Hoare2]
Q:18 [in HoareAsLogic]
Q:2 [in UseAuto]
Q:200 [in LibTactics]
Q:201 [in Hoare]
Q:22 [in Hoare2]
Q:23 [in UseAuto]
Q:241 [in Hoare]
Q:246 [in Hoare]
Q:249 [in Hoare]
Q:251 [in Hoare]
Q:26 [in UseAuto]
Q:3 [in Hoare2]
Q:3 [in HoareAsLogic]
Q:30 [in HoareAsLogic]
Q:305 [in Hoare]
Q:311 [in Hoare]
Q:314 [in Hoare]
Q:315 [in Hoare]
Q:320 [in Hoare]
Q:323 [in Hoare]
Q:329 [in Hoare]
Q:335 [in Hoare]
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 LibTactics]
Q:56 [in HoareAsLogic]
Q:58 [in Hoare]
Q:6 [in UseAuto]
Q:6 [in Hoare]
Q:60 [in HoareAsLogic]
Q:62 [in HoareAsLogic]
Q:65 [in HoareAsLogic]
Q:7 [in UseTactics]
Q:70 [in HoareAsLogic]
Q:73 [in HoareAsLogic]
Q:75 [in Hoare]
Q:78 [in Hoare]
Q:8 [in Hoare2]
Q:83 [in Hoare]
Q:88 [in Hoare]
Q:9 [in HoareAsLogic]
Q:91 [in Hoare2]
Q:92 [in Hoare]
Q:93 [in Hoare2]
Q:96 [in Hoare]
Q:97 [in Hoare2]
R
R:122 [in Smallstep]R:130 [in Smallstep]
R:134 [in Smallstep]
R:141 [in Smallstep]
R:16 [in HoareAsLogic]
R:18 [in UseAuto]
R:18 [in UseTactics]
R:25 [in Smallstep]
R:256 [in References]
r:272 [in Hoare]
r:277 [in Hoare]
r:282 [in Hoare]
r:291 [in Hoare]
r:307 [in Hoare]
R:330 [in Hoare]
R:45 [in Smallstep]
R:51 [in Hoare]
S
Si:103 [in RecordSub]Sr2:87 [in RecordSub]
ss:180 [in Norm]
ss:224 [in Norm]
ss:232 [in Norm]
ss:234 [in Norm]
ss:238 [in Norm]
stk:330 [in Smallstep]
stk:333 [in Smallstep]
stk:336 [in Smallstep]
stk:340 [in Smallstep]
stk:344 [in Smallstep]
st'o:461 [in PE]
st'o:472 [in PE]
st'':132 [in Hoare]
st'':148 [in Hoare]
st'':150 [in Equiv]
st'':166 [in Equiv]
st'':179 [in PE]
st'':180 [in Hoare]
st'':188 [in PE]
st'':194 [in PE]
st'':196 [in Hoare]
st'':200 [in PE]
st'':217 [in Hoare]
st'':233 [in Hoare]
st'':331 [in PE]
st'':351 [in PE]
st'':374 [in PE]
st'':384 [in PE]
st'':393 [in PE]
st'':401 [in PE]
st'':408 [in PE]
st'':434 [in PE]
st':10 [in Equiv]
st':102 [in References]
st':108 [in References]
st':115 [in UseAuto]
ST':116 [in UseAuto]
st':116 [in References]
st':121 [in References]
st':130 [in UseAuto]
ST':131 [in UseAuto]
st':131 [in Hoare]
st':134 [in Hoare]
st':137 [in UseAuto]
st':139 [in Hoare]
st':14 [in Equiv]
st':147 [in Hoare]
st':149 [in Equiv]
st':152 [in Equiv]
st':155 [in Hoare]
st':157 [in Equiv]
st':165 [in Equiv]
st':172 [in Equiv]
st':173 [in References]
st':174 [in Equiv]
st':176 [in Equiv]
st':179 [in Hoare]
st':182 [in Hoare]
st':182 [in PE]
st':184 [in Equiv]
st':185 [in References]
st':187 [in Hoare]
ST':188 [in References]
ST':190 [in References]
ST':194 [in References]
st':195 [in Hoare]
ST':197 [in References]
st':203 [in Hoare]
st':206 [in References]
ST':207 [in References]
st':216 [in Hoare]
st':219 [in Hoare]
st':224 [in Hoare]
ST':230 [in References]
st':232 [in Hoare]
st':243 [in Hoare]
st':246 [in References]
ST':247 [in References]
st':253 [in References]
st':257 [in Smallstep]
st':271 [in Hoare]
st':289 [in Smallstep]
st':290 [in Hoare]
st':308 [in Hoare]
st':311 [in Smallstep]
st':316 [in Smallstep]
st':318 [in Smallstep]
st':319 [in Smallstep]
st':324 [in Smallstep]
st':326 [in Smallstep]
st':326 [in Hoare]
st':327 [in Hoare]
st':33 [in Equiv]
st':330 [in PE]
st':335 [in PE]
st':341 [in PE]
st':350 [in PE]
st':358 [in PE]
st':362 [in PE]
st':378 [in PE]
st':39 [in Hoare]
st':409 [in PE]
st':432 [in PE]
st':449 [in PE]
st':465 [in PE]
st':5 [in HoareAsLogic]
st':53 [in References]
st':58 [in References]
st':64 [in References]
st':70 [in References]
st':74 [in Equiv]
st':78 [in References]
st':80 [in Equiv]
st':83 [in References]
st':89 [in References]
st1:121 [in PE]
st1:13 [in UseTactics]
ST1:178 [in References]
st1:24 [in UseTactics]
st1:28 [in UseTactics]
st1:3 [in UseTactics]
st1:68 [in UseAuto]
st1:72 [in UseAuto]
st1:76 [in UseAuto]
st1:80 [in UseAuto]
st1:84 [in UseAuto]
st1:88 [in UseTactics]
st1:92 [in UseTactics]
st2:122 [in PE]
st2:14 [in UseTactics]
ST2:179 [in References]
st2:25 [in UseTactics]
st2:29 [in UseTactics]
st2:4 [in UseTactics]
st2:69 [in UseAuto]
st2:73 [in UseAuto]
st2:77 [in UseAuto]
st2:81 [in UseAuto]
st2:85 [in UseAuto]
st2:89 [in UseTactics]
st2:93 [in UseTactics]
st:1 [in Hoare]
st:101 [in References]
st:103 [in References]
st:107 [in References]
st:107 [in PE]
st:11 [in Hoare]
ST:110 [in UseAuto]
st:111 [in Hoare]
st:111 [in References]
st:113 [in Hoare]
st:114 [in UseAuto]
st:114 [in PE]
st:115 [in References]
st:118 [in PE]
st:12 [in Hoare]
st:12 [in UseTactics]
st:120 [in References]
st:120 [in PE]
st:122 [in UseAuto]
ST:123 [in UseAuto]
st:123 [in Hoare]
st:124 [in Hoare]
ST:124 [in References]
ST:125 [in UseAuto]
ST:125 [in References]
st:126 [in PE]
st:129 [in UseAuto]
st:13 [in Hoare]
st:13 [in Equiv]
st:130 [in Hoare]
ST:132 [in UseAuto]
st:133 [in Hoare]
st:134 [in Equiv]
st:135 [in UseAuto]
st:138 [in Hoare]
st:14 [in Hoare]
st:141 [in Equiv]
st:142 [in Equiv]
st:144 [in Hoare]
st:146 [in Hoare]
st:148 [in Equiv]
st:15 [in Hoare]
st:151 [in Equiv]
st:154 [in Hoare]
st:156 [in Equiv]
st:16 [in Hoare]
st:162 [in Equiv]
st:164 [in Equiv]
st:167 [in PE]
ST:168 [in References]
st:169 [in PE]
st:17 [in Hoare]
st:171 [in Hoare]
st:171 [in References]
st:171 [in Equiv]
st:171 [in PE]
st:172 [in Hoare]
st:173 [in Equiv]
st:173 [in PE]
ST:174 [in References]
st:175 [in References]
st:175 [in Equiv]
st:175 [in PE]
st:177 [in References]
st:178 [in Hoare]
st:178 [in PE]
st:18 [in Hoare]
ST:180 [in References]
st:181 [in Hoare]
st:183 [in References]
st:183 [in Equiv]
st:186 [in Hoare]
st:187 [in PE]
st:19 [in Hoare]
st:190 [in Smallstep]
ST:191 [in References]
st:192 [in Hoare]
ST:193 [in References]
st:193 [in PE]
st:194 [in Hoare]
ST:196 [in References]
ST:198 [in References]
st:199 [in PE]
st:2 [in Hoare]
st:2 [in UseTactics]
st:20 [in Hoare]
st:20 [in References]
ST:200 [in References]
ST:201 [in References]
st:202 [in Hoare]
st:205 [in References]
st:208 [in Hoare]
st:209 [in Hoare]
st:21 [in Hoare]
ST:210 [in References]
ST:214 [in References]
st:215 [in Hoare]
st:218 [in Smallstep]
st:218 [in Hoare]
ST:218 [in References]
st:22 [in Hoare]
st:22 [in HoareAsLogic]
st:223 [in Hoare]
ST:224 [in References]
st:225 [in References]
st:229 [in Hoare]
ST:229 [in References]
st:23 [in Hoare]
st:23 [in UseTactics]
st:23 [in HoareAsLogic]
st:231 [in Hoare]
ST:233 [in References]
st:234 [in References]
st:236 [in Hoare]
st:24 [in Hoare]
st:24 [in PE]
ST:241 [in References]
st:242 [in Hoare]
st:245 [in References]
st:247 [in Smallstep]
ST:248 [in References]
st:25 [in Hoare]
st:250 [in Hoare]
st:251 [in Smallstep]
st:251 [in References]
st:254 [in Smallstep]
st:255 [in Hoare]
st:259 [in Smallstep]
st:261 [in Smallstep]
st:263 [in Hoare]
st:264 [in Hoare]
st:266 [in Smallstep]
st:269 [in Smallstep]
st:27 [in UseTactics]
st:27 [in HoareAsLogic]
st:270 [in Hoare]
st:272 [in Smallstep]
st:275 [in Hoare]
st:276 [in Hoare]
st:279 [in Smallstep]
st:28 [in PE]
st:28 [in HoareAsLogic]
st:281 [in Hoare]
st:281 [in PE]
st:283 [in Smallstep]
st:283 [in PE]
st:285 [in PE]
st:286 [in Smallstep]
st:287 [in Hoare]
st:287 [in PE]
st:289 [in Hoare]
st:289 [in PE]
st:29 [in Hoare]
st:291 [in Smallstep]
st:291 [in PE]
st:293 [in Smallstep]
st:293 [in PE]
st:294 [in Hoare]
st:295 [in PE]
st:297 [in Hoare]
st:297 [in PE]
st:298 [in Smallstep]
st:299 [in Hoare]
st:299 [in PE]
st:3 [in Hoare]
st:3 [in Equiv]
st:301 [in Smallstep]
st:301 [in Hoare]
st:301 [in PE]
st:303 [in PE]
st:304 [in Smallstep]
st:305 [in PE]
st:306 [in Hoare]
st:307 [in Smallstep]
st:307 [in PE]
st:309 [in PE]
st:31 [in PE]
st:311 [in PE]
st:312 [in Smallstep]
st:313 [in PE]
st:315 [in PE]
st:317 [in Smallstep]
st:317 [in PE]
st:319 [in PE]
st:32 [in Equiv]
st:321 [in Smallstep]
st:322 [in PE]
st:323 [in Smallstep]
st:323 [in PE]
st:327 [in Smallstep]
st:329 [in PE]
st:334 [in PE]
st:34 [in Hoare]
st:34 [in HoareAsLogic]
st:340 [in PE]
st:347 [in PE]
st:348 [in Smallstep]
st:349 [in Smallstep]
st:349 [in PE]
st:35 [in HoareAsLogic]
st:357 [in PE]
st:361 [in PE]
st:369 [in PE]
st:37 [in References]
st:37 [in PE]
st:373 [in PE]
st:38 [in Hoare]
st:383 [in PE]
st:392 [in PE]
st:4 [in Hoare]
st:4 [in HoareAsLogic]
st:40 [in PE]
st:40 [in HoareAsLogic]
st:400 [in PE]
st:407 [in PE]
st:41 [in References]
st:416 [in PE]
st:42 [in PE]
st:427 [in PE]
st:429 [in PE]
st:43 [in Hoare]
st:436 [in PE]
st:437 [in PE]
st:438 [in PE]
st:439 [in PE]
st:446 [in PE]
st:45 [in HoareAsLogic]
st:458 [in PE]
st:46 [in HoareAsLogic]
st:469 [in PE]
st:47 [in Hoare]
st:47 [in PE]
st:47 [in HoareAsLogic]
st:48 [in References]
st:52 [in References]
st:55 [in PE]
st:57 [in Hoare]
st:57 [in References]
st:6 [in Equiv]
st:60 [in References]
st:63 [in References]
st:66 [in Hoare]
st:66 [in References]
st:67 [in UseAuto]
st:67 [in Hoare]
st:68 [in UseTactics]
st:69 [in References]
st:7 [in Hoare]
st:70 [in Hoare]
st:70 [in PE]
st:71 [in UseAuto]
st:71 [in Hoare]
st:73 [in References]
st:73 [in Equiv]
st:74 [in PE]
st:75 [in UseAuto]
st:77 [in References]
st:79 [in UseAuto]
st:79 [in Equiv]
st:82 [in References]
st:83 [in UseAuto]
st:87 [in UseTactics]
st:88 [in References]
st:9 [in Equiv]
st:91 [in UseTactics]
st:92 [in References]
st:96 [in References]
st:98 [in References]
s':58 [in HoareAsLogic]
S1:113 [in Sub]
S1:139 [in UseAuto]
S1:144 [in UseAuto]
S1:155 [in RecordSub]
S1:162 [in RecordSub]
S1:167 [in RecordSub]
S1:174 [in Sub]
S1:178 [in Sub]
S1:182 [in Sub]
S1:186 [in Sub]
S1:42 [in Sub]
S1:77 [in RecordSub]
S1:85 [in RecordSub]
S1:88 [in Sub]
S1:97 [in Sub]
S2:100 [in Sub]
s2:114 [in Sub]
s2:140 [in UseAuto]
s2:145 [in UseAuto]
s2:156 [in RecordSub]
S2:165 [in RecordSub]
s2:168 [in RecordSub]
S2:175 [in Sub]
S2:179 [in Sub]
S2:183 [in Sub]
S2:187 [in Sub]
S2:43 [in Sub]
S2:78 [in RecordSub]
s2:89 [in Sub]
S:104 [in Sub]
s:11 [in Stlc]
s:13 [in References]
S:131 [in RecordSub]
S:134 [in Sub]
S:138 [in Sub]
S:142 [in Sub]
S:143 [in Norm]
S:146 [in Sub]
s:15 [in Stlc]
S:150 [in Sub]
s:151 [in RecordSub]
S:154 [in Sub]
S:158 [in Sub]
s:161 [in Norm]
S:162 [in Sub]
S:164 [in Sub]
S:166 [in Sub]
S:167 [in Sub]
S:169 [in Sub]
S:171 [in UseAuto]
S:171 [in Sub]
S:175 [in UseAuto]
S:181 [in UseAuto]
s:19 [in Stlc]
S:198 [in Sub]
S:219 [in Sub]
S:224 [in Sub]
s:24 [in RecordSub]
S:269 [in Norm]
s:27 [in Records]
S:38 [in Sub]
S:41 [in Sub]
s:57 [in HoareAsLogic]
s:6 [in MoreStlc]
s:6 [in Norm]
s:6 [in Sub]
S:67 [in Stlc]
S:73 [in RecordSub]
S:76 [in RecordSub]
s:81 [in Sub]
s:84 [in StlcProp]
s:84 [in Sub]
s:91 [in Sub]
S:94 [in RecordSub]
S:97 [in UseTactics]
S:99 [in RecordSub]
T
Tguard:21 [in Typechecking]Tguard:55 [in Typechecking]
Ti:100 [in Records]
Ti:102 [in RecordSub]
Ti:109 [in Records]
ti:110 [in Records]
Ti:128 [in RecordSub]
Ti:148 [in RecordSub]
Ti:88 [in Records]
Ti:98 [in RecordSub]
TL:201 [in Sub]
TL:205 [in Sub]
TL:209 [in Sub]
TL:213 [in Sub]
tr':102 [in Records]
tr':144 [in RecordSub]
tr2':68 [in Records]
tr2':69 [in RecordSub]
tr2:64 [in Records]
tr2:65 [in RecordSub]
tr2:67 [in Records]
tr2:68 [in RecordSub]
Tr2:88 [in RecordSub]
Tr3:93 [in RecordSub]
tr:101 [in Records]
tr:138 [in RecordSub]
Tr:139 [in RecordSub]
tr:143 [in RecordSub]
Tr:37 [in RecordSub]
tr:40 [in Records]
tr:41 [in RecordSub]
tr:58 [in Records]
tr:59 [in RecordSub]
Tr:70 [in Records]
Tr:89 [in Records]
tr:93 [in Records]
Tr:94 [in Records]
TS:200 [in Sub]
TS:203 [in Sub]
TS:207 [in Sub]
TS:211 [in Sub]
TS:221 [in Sub]
t':101 [in Norm]
t':103 [in StlcProp]
t':110 [in Smallstep]
t':112 [in UseAuto]
t':113 [in Records]
t':12 [in StlcProp]
t':127 [in UseAuto]
t':128 [in Records]
t':131 [in Sub]
t':136 [in UseAuto]
t':139 [in Smallstep]
t':143 [in Smallstep]
T':151 [in Norm]
t':153 [in Smallstep]
t':155 [in Norm]
t':156 [in Smallstep]
t':159 [in RecordSub]
t':167 [in Norm]
t':170 [in MoreStlc]
t':170 [in Norm]
t':172 [in References]
t':173 [in Norm]
t':176 [in Norm]
t':179 [in Norm]
t':184 [in Smallstep]
t':184 [in References]
t':185 [in RecordSub]
t':185 [in MoreStlc]
t':186 [in Smallstep]
t':203 [in References]
t':207 [in Norm]
t':210 [in Norm]
t':214 [in Norm]
t':22 [in Stlc]
t':243 [in References]
t':252 [in References]
t':264 [in Norm]
t':33 [in StlcProp]
t':36 [in StlcProp]
t':40 [in StlcProp]
t':43 [in Smallstep]
T':45 [in StlcProp]
t':46 [in Types]
t':47 [in Smallstep]
t':48 [in Types]
t':50 [in Smallstep]
t':51 [in Smallstep]
t':51 [in Types]
t':54 [in Types]
t':57 [in Types]
t':60 [in Types]
T':71 [in StlcProp]
t':87 [in UseAuto]
t':87 [in Typechecking]
t':9 [in StlcProp]
t':90 [in UseAuto]
t':90 [in Typechecking]
t':94 [in UseAuto]
t':94 [in Sub]
t':97 [in UseAuto]
t':99 [in StlcProp]
t0':44 [in Norm]
t0':48 [in Norm]
t0':67 [in MoreStlc]
t0:117 [in Norm]
t0:121 [in Norm]
t0:125 [in Norm]
T0:135 [in MoreStlc]
t0:145 [in MoreStlc]
T0:154 [in References]
t0:43 [in Norm]
t0:47 [in Norm]
T0:59 [in Typechecking]
t0:66 [in MoreStlc]
t0:80 [in Norm]
t0:84 [in Norm]
t1':100 [in References]
t1':106 [in Smallstep]
t1':106 [in References]
t1':113 [in References]
t1':118 [in Smallstep]
t1':145 [in Smallstep]
t1':170 [in Smallstep]
t1':18 [in Smallstep]
t1':180 [in Smallstep]
t1':20 [in Types]
t1':22 [in Sub]
t1':23 [in Types]
t1':24 [in Norm]
t1':26 [in Types]
t1':30 [in Stlc]
t1':32 [in MoreStlc]
t1':32 [in Sub]
t1':34 [in Norm]
t1':37 [in Smallstep]
t1':38 [in MoreStlc]
t1':38 [in Norm]
t1':40 [in Stlc]
t1':41 [in MoreStlc]
t1':46 [in MoreStlc]
t1':50 [in References]
t1':50 [in Records]
t1':51 [in RecordSub]
t1':52 [in MoreStlc]
t1':56 [in Records]
t1':57 [in RecordSub]
t1':61 [in MoreStlc]
t1':62 [in References]
t1':63 [in Smallstep]
t1':63 [in Records]
t1':64 [in RecordSub]
t1':68 [in References]
t1':76 [in References]
t1':78 [in Smallstep]
t1':85 [in References]
t1':85 [in MoreStlc]
t1':91 [in MoreStlc]
t1':92 [in Smallstep]
T11:114 [in Norm]
T11:116 [in RecordSub]
T11:79 [in Records]
t12:115 [in Norm]
T12:117 [in RecordSub]
t12:118 [in RecordSub]
T12:80 [in Records]
t12:81 [in Records]
T1:1 [in Typechecking]
t1:101 [in Smallstep]
t1:103 [in Smallstep]
t1:105 [in Smallstep]
t1:105 [in References]
t1:106 [in Sub]
t1:107 [in Norm]
T1:109 [in Sub]
t1:11 [in Types]
T1:11 [in Records]
t1:110 [in Norm]
T1:111 [in MoreStlc]
t1:112 [in References]
t1:113 [in Smallstep]
T1:114 [in MoreStlc]
t1:115 [in Smallstep]
T1:115 [in Sub]
t1:116 [in MoreStlc]
t1:117 [in Smallstep]
T1:117 [in MoreStlc]
t1:118 [in Norm]
T1:119 [in RecordSub]
t1:120 [in MoreStlc]
t1:122 [in RecordSub]
t1:122 [in Norm]
T1:124 [in UseAuto]
t1:126 [in Norm]
t1:129 [in MoreStlc]
t1:129 [in Norm]
t1:13 [in RecordSub]
t1:13 [in Types]
T1:130 [in References]
t1:132 [in MoreStlc]
t1:132 [in Norm]
T1:133 [in References]
t1:135 [in References]
T1:136 [in References]
t1:137 [in MoreStlc]
T1:138 [in MoreStlc]
t1:139 [in References]
t1:14 [in MoreStlc]
t1:14 [in Norm]
t1:14 [in Sub]
T1:141 [in UseAuto]
T1:142 [in MoreStlc]
t1:144 [in Smallstep]
t1:144 [in References]
T1:146 [in UseAuto]
t1:146 [in References]
T1:147 [in MoreStlc]
t1:148 [in References]
t1:148 [in MoreStlc]
t1:151 [in References]
T1:152 [in RecordSub]
T1:154 [in MoreStlc]
t1:156 [in MoreStlc]
T1:158 [in MoreStlc]
t1:159 [in References]
T1:16 [in Records]
T1:160 [in References]
t1:160 [in MoreStlc]
T1:161 [in MoreStlc]
t1:162 [in References]
T1:163 [in References]
t1:165 [in References]
t1:169 [in Smallstep]
T1:169 [in RecordSub]
t1:17 [in Smallstep]
t1:17 [in References]
T1:17 [in Typechecking]
T1:17 [in MoreStlc]
T1:172 [in Sub]
t1:175 [in Smallstep]
T1:176 [in Sub]
t1:177 [in Smallstep]
T1:177 [in UseAuto]
t1:179 [in Smallstep]
T1:18 [in Typechecking]
T1:18 [in RecordSub]
T1:180 [in Sub]
T1:184 [in Sub]
t1:19 [in Types]
T1:19 [in MoreStlc]
T1:19 [in Records]
t1:19 [in Sub]
T1:20 [in MoreStlc]
T1:21 [in RecordSub]
t1:21 [in Norm]
t1:21 [in Sub]
T1:22 [in Typechecking]
t1:22 [in Types]
t1:23 [in Norm]
t1:235 [in References]
T1:236 [in References]
t1:239 [in Norm]
t1:24 [in Records]
t1:25 [in Types]
t1:27 [in Stlc]
t1:27 [in Sub]
t1:29 [in Stlc]
t1:29 [in MoreStlc]
t1:29 [in Norm]
t1:29 [in Sub]
T1:3 [in StlcProp]
T1:31 [in Typechecking]
t1:31 [in MoreStlc]
t1:31 [in Norm]
t1:31 [in Sub]
t1:32 [in RecordSub]
t1:33 [in Norm]
t1:34 [in Types]
t1:35 [in Stlc]
t1:35 [in Records]
t1:36 [in Smallstep]
T1:37 [in Typechecking]
t1:37 [in Stlc]
t1:37 [in MoreStlc]
t1:37 [in Norm]
t1:38 [in Types]
t1:39 [in Stlc]
t1:39 [in Types]
t1:40 [in Types]
t1:40 [in MoreStlc]
T1:44 [in Typechecking]
T1:44 [in Sub]
t1:45 [in MoreStlc]
t1:46 [in References]
T1:47 [in Typechecking]
T1:47 [in Stlc]
t1:47 [in Records]
t1:48 [in RecordSub]
t1:49 [in References]
T1:49 [in Typechecking]
t1:49 [in StlcProp]
t1:49 [in Records]
t1:50 [in RecordSub]
T1:50 [in Stlc]
T1:50 [in Sub]
T1:51 [in Typechecking]
t1:51 [in StlcProp]
t1:51 [in MoreStlc]
t1:52 [in Stlc]
T1:53 [in Stlc]
T1:53 [in Sub]
T1:54 [in StlcProp]
t1:55 [in StlcProp]
t1:55 [in Records]
t1:55 [in Sub]
t1:56 [in Smallstep]
T1:56 [in Typechecking]
t1:56 [in StlcProp]
t1:56 [in RecordSub]
t1:56 [in Stlc]
T1:56 [in Norm]
T1:56 [in Sub]
t1:59 [in StlcProp]
T1:59 [in Norm]
t1:59 [in Sub]
t1:60 [in Stlc]
t1:60 [in MoreStlc]
t1:61 [in References]
T1:61 [in Typechecking]
t1:61 [in Norm]
t1:62 [in Smallstep]
t1:62 [in StlcProp]
T1:62 [in Norm]
t1:62 [in Records]
t1:63 [in RecordSub]
T1:63 [in Stlc]
t1:63 [in Sub]
T1:65 [in MoreStlc]
t1:65 [in Norm]
T1:66 [in Sub]
t1:67 [in References]
t1:69 [in MoreStlc]
t1:69 [in Norm]
T1:7 [in Typechecking]
t1:70 [in Sub]
T1:71 [in Sub]
T1:72 [in Norm]
t1:74 [in References]
t1:74 [in MoreStlc]
t1:75 [in Norm]
t1:77 [in Smallstep]
T1:77 [in Norm]
T1:79 [in RecordSub]
T1:8 [in RecordSub]
t1:80 [in MoreStlc]
T1:81 [in Norm]
T1:82 [in RecordSub]
T1:82 [in Records]
T1:83 [in MoreStlc]
t1:84 [in References]
t1:84 [in MoreStlc]
t1:84 [in Records]
T1:85 [in Norm]
T1:85 [in Sub]
T1:86 [in RecordSub]
t1:9 [in Smallstep]
t1:9 [in References]
t1:9 [in Stlc]
t1:90 [in MoreStlc]
t1:91 [in Smallstep]
T1:91 [in RecordSub]
T1:96 [in MoreStlc]
t1:99 [in References]
t2':119 [in References]
t2':149 [in Smallstep]
t2':174 [in Smallstep]
t2':22 [in Smallstep]
t2':26 [in Sub]
t2':28 [in Norm]
t2':34 [in Stlc]
t2':36 [in MoreStlc]
t2':41 [in Smallstep]
t2':42 [in Norm]
t2':50 [in MoreStlc]
t2':54 [in Records]
t2':55 [in RecordSub]
t2':56 [in References]
t2':64 [in MoreStlc]
t2':67 [in Smallstep]
t2':81 [in References]
t2':82 [in Smallstep]
t2':89 [in MoreStlc]
t2:10 [in Smallstep]
t2:102 [in Smallstep]
t2:103 [in MoreStlc]
t2:104 [in Smallstep]
t2:107 [in Smallstep]
t2:107 [in Sub]
t2:108 [in Norm]
T2:108 [in Sub]
t2:111 [in Norm]
t2:114 [in Smallstep]
t2:114 [in References]
T2:115 [in MoreStlc]
t2:116 [in Smallstep]
T2:116 [in Sub]
t2:118 [in References]
T2:118 [in MoreStlc]
t2:119 [in Smallstep]
t2:119 [in Norm]
t2:12 [in Types]
T2:12 [in Records]
T2:120 [in RecordSub]
t2:121 [in MoreStlc]
t2:123 [in RecordSub]
t2:123 [in Norm]
t2:127 [in Norm]
T2:13 [in MoreStlc]
T2:13 [in Norm]
T2:13 [in Sub]
t2:130 [in MoreStlc]
t2:130 [in Norm]
t2:133 [in MoreStlc]
t2:133 [in Norm]
T2:134 [in References]
T2:137 [in References]
T2:139 [in MoreStlc]
t2:14 [in RecordSub]
t2:14 [in Types]
t2:140 [in References]
t2:141 [in MoreStlc]
T2:142 [in UseAuto]
T2:143 [in MoreStlc]
t2:146 [in Smallstep]
T2:147 [in UseAuto]
t2:148 [in Smallstep]
t2:149 [in References]
T2:150 [in MoreStlc]
t2:151 [in MoreStlc]
t2:152 [in References]
T2:153 [in RecordSub]
t2:157 [in MoreStlc]
t2:162 [in MoreStlc]
t2:163 [in RecordSub]
t2:166 [in References]
T2:166 [in MoreStlc]
T2:167 [in References]
t2:17 [in Types]
T2:17 [in Records]
T2:170 [in RecordSub]
t2:171 [in Smallstep]
t2:173 [in Smallstep]
T2:173 [in Sub]
t2:176 [in Smallstep]
T2:177 [in Sub]
t2:178 [in Smallstep]
T2:178 [in UseAuto]
t2:18 [in References]
T2:18 [in Sub]
t2:181 [in Smallstep]
T2:181 [in Sub]
T2:185 [in Sub]
t2:19 [in Smallstep]
T2:19 [in Typechecking]
T2:19 [in RecordSub]
T2:2 [in Typechecking]
T2:20 [in Norm]
T2:20 [in Records]
t2:21 [in Smallstep]
T2:22 [in RecordSub]
T2:23 [in Typechecking]
t2:23 [in Sub]
t2:240 [in Norm]
t2:25 [in Norm]
t2:25 [in Records]
t2:25 [in Sub]
T2:26 [in Stlc]
t2:27 [in Norm]
T2:28 [in MoreStlc]
t2:28 [in Sub]
t2:30 [in Norm]
t2:30 [in Sub]
T2:31 [in RecordSub]
t2:31 [in Stlc]
T2:32 [in Typechecking]
t2:32 [in Norm]
t2:33 [in Stlc]
t2:33 [in MoreStlc]
t2:33 [in Sub]
T2:34 [in Records]
t2:35 [in Types]
t2:35 [in MoreStlc]
t2:35 [in Norm]
t2:36 [in Stlc]
t2:38 [in Smallstep]
T2:38 [in Typechecking]
t2:38 [in Stlc]
t2:39 [in Norm]
T2:4 [in StlcProp]
t2:40 [in Smallstep]
t2:41 [in Stlc]
t2:41 [in Norm]
T2:43 [in Typechecking]
T2:45 [in References]
T2:45 [in Typechecking]
T2:45 [in Sub]
T2:46 [in Records]
T2:47 [in RecordSub]
t2:47 [in MoreStlc]
t2:49 [in MoreStlc]
t2:50 [in StlcProp]
t2:51 [in References]
T2:51 [in Stlc]
t2:51 [in Records]
T2:52 [in Typechecking]
t2:52 [in StlcProp]
t2:52 [in RecordSub]
t2:53 [in MoreStlc]
t2:53 [in Records]
t2:54 [in RecordSub]
T2:54 [in Stlc]
T2:54 [in Sub]
t2:55 [in References]
t2:55 [in MoreStlc]
T2:57 [in Typechecking]
t2:57 [in StlcProp]
t2:57 [in Stlc]
T2:57 [in Sub]
t2:58 [in MoreStlc]
t2:60 [in StlcProp]
T2:60 [in Norm]
t2:60 [in Sub]
t2:61 [in Stlc]
T2:62 [in Typechecking]
T2:62 [in MoreStlc]
t2:63 [in StlcProp]
t2:63 [in MoreStlc]
T2:63 [in Norm]
t2:64 [in Smallstep]
t2:64 [in Sub]
t2:66 [in Smallstep]
t2:66 [in Norm]
t2:70 [in Norm]
t2:71 [in MoreStlc]
T2:72 [in Sub]
t2:75 [in References]
t2:76 [in MoreStlc]
t2:76 [in Norm]
T2:77 [in MoreStlc]
T2:78 [in Norm]
t2:79 [in Smallstep]
T2:8 [in References]
T2:8 [in Typechecking]
T2:8 [in Stlc]
t2:80 [in References]
T2:80 [in RecordSub]
t2:81 [in Smallstep]
t2:82 [in MoreStlc]
T2:82 [in Norm]
T2:83 [in RecordSub]
T2:83 [in Records]
t2:85 [in Records]
t2:86 [in References]
t2:86 [in MoreStlc]
T2:86 [in Norm]
T2:86 [in Sub]
t2:88 [in MoreStlc]
T2:9 [in RecordSub]
t2:90 [in References]
T2:92 [in RecordSub]
t2:92 [in MoreStlc]
t2:93 [in Smallstep]
t2:94 [in References]
t2:97 [in MoreStlc]
t2:98 [in Sub]
t3:100 [in MoreStlc]
t3:106 [in MoreStlc]
t3:108 [in Smallstep]
t3:120 [in Smallstep]
t3:134 [in MoreStlc]
T3:152 [in MoreStlc]
t3:153 [in References]
t3:165 [in MoreStlc]
T3:179 [in UseAuto]
t3:18 [in Types]
t3:182 [in Smallstep]
t3:34 [in Sub]
t3:36 [in Types]
t3:36 [in Norm]
t3:42 [in Stlc]
t3:54 [in MoreStlc]
t3:56 [in MoreStlc]
t3:58 [in StlcProp]
t3:59 [in MoreStlc]
t3:61 [in StlcProp]
t3:62 [in Stlc]
t3:64 [in StlcProp]
t3:65 [in Sub]
t3:71 [in Norm]
t3:87 [in References]
t3:91 [in References]
t3:95 [in References]
t3:95 [in MoreStlc]
T4:180 [in UseAuto]
t:1 [in StlcProp]
t:10 [in Typechecking]
t:10 [in StlcProp]
T:100 [in StlcProp]
T:100 [in RecordSub]
t:100 [in Norm]
t:101 [in UseAuto]
t:101 [in StlcProp]
T:101 [in UseTactics]
T:102 [in StlcProp]
T:102 [in Norm]
T:103 [in Sub]
t:104 [in UseAuto]
T:104 [in UseTactics]
t:104 [in Records]
T:105 [in Records]
t:107 [in UseAuto]
T:107 [in Records]
t:109 [in Smallstep]
T:11 [in StlcProp]
t:111 [in UseAuto]
t:111 [in Records]
T:111 [in Sub]
T:111 [in LibTactics]
T:112 [in Records]
T:113 [in UseAuto]
T:113 [in RecordSub]
t:116 [in Records]
T:117 [in Records]
t:119 [in Records]
t:119 [in Sub]
t:12 [in Stlc]
T:120 [in Records]
T:120 [in Sub]
t:122 [in References]
t:122 [in Sub]
T:123 [in Sub]
t:124 [in Records]
t:125 [in MoreStlc]
t:126 [in UseAuto]
t:126 [in RecordSub]
T:126 [in Records]
T:127 [in RecordSub]
t:127 [in MoreStlc]
t:127 [in Records]
t:127 [in Sub]
T:128 [in UseAuto]
T:129 [in Records]
T:129 [in Sub]
t:130 [in RecordSub]
t:130 [in Sub]
T:132 [in RecordSub]
T:132 [in Sub]
t:133 [in UseAuto]
T:134 [in UseAuto]
t:135 [in Norm]
T:135 [in Sub]
t:136 [in RecordSub]
T:137 [in RecordSub]
t:137 [in Norm]
t:138 [in Smallstep]
t:138 [in Norm]
T:139 [in Sub]
t:14 [in References]
t:14 [in Typechecking]
t:141 [in RecordSub]
t:142 [in Smallstep]
T:142 [in RecordSub]
t:142 [in Norm]
T:143 [in Sub]
T:146 [in RecordSub]
T:147 [in Sub]
t:148 [in Norm]
T:149 [in Norm]
t:15 [in StlcProp]
T:15 [in LibTactics]
t:150 [in Smallstep]
T:151 [in Sub]
t:152 [in Smallstep]
t:152 [in Norm]
T:153 [in Norm]
t:154 [in Norm]
t:155 [in Smallstep]
T:155 [in Sub]
t:157 [in RecordSub]
T:157 [in Norm]
t:158 [in Smallstep]
T:158 [in RecordSub]
t:158 [in Norm]
T:159 [in Sub]
T:16 [in StlcProp]
T:162 [in Norm]
t:163 [in Norm]
T:163 [in Sub]
T:164 [in RecordSub]
T:164 [in Norm]
t:165 [in Norm]
T:165 [in Sub]
t:166 [in Norm]
t:168 [in MoreStlc]
T:168 [in Norm]
T:168 [in Sub]
T:169 [in UseAuto]
T:169 [in References]
T:169 [in MoreStlc]
t:169 [in Norm]
t:170 [in References]
T:170 [in Sub]
T:171 [in Norm]
T:172 [in UseAuto]
t:172 [in Norm]
t:173 [in RecordSub]
t:173 [in MoreStlc]
T:174 [in RecordSub]
T:174 [in MoreStlc]
T:174 [in Norm]
t:175 [in Norm]
T:176 [in UseAuto]
t:176 [in RecordSub]
t:176 [in MoreStlc]
T:177 [in RecordSub]
T:177 [in MoreStlc]
T:177 [in Norm]
t:178 [in Norm]
t:18 [in StlcProp]
T:181 [in References]
t:181 [in RecordSub]
t:181 [in MoreStlc]
t:181 [in Norm]
T:182 [in UseAuto]
t:182 [in References]
t:183 [in Smallstep]
T:183 [in RecordSub]
T:183 [in MoreStlc]
t:184 [in RecordSub]
t:184 [in MoreStlc]
t:185 [in Smallstep]
T:186 [in RecordSub]
T:186 [in MoreStlc]
T:19 [in StlcProp]
T:19 [in LibTactics]
T:196 [in Sub]
T:199 [in References]
t:2 [in StlcProp]
T:201 [in Norm]
t:202 [in References]
T:202 [in Sub]
T:204 [in References]
T:204 [in Sub]
t:205 [in Norm]
T:206 [in Sub]
t:208 [in Norm]
T:208 [in Sub]
t:21 [in Stlc]
T:210 [in Sub]
t:211 [in References]
t:211 [in Norm]
T:212 [in References]
T:212 [in Sub]
T:214 [in Sub]
t:215 [in References]
T:215 [in Sub]
T:216 [in References]
t:216 [in Norm]
T:216 [in Sub]
T:217 [in Sub]
t:218 [in Norm]
T:218 [in Sub]
t:221 [in References]
T:222 [in Sub]
T:223 [in References]
t:223 [in Norm]
T:223 [in Sub]
t:225 [in Sub]
T:226 [in Sub]
t:227 [in References]
t:23 [in StlcProp]
t:231 [in References]
t:231 [in Norm]
T:232 [in References]
T:236 [in Norm]
t:237 [in Norm]
t:242 [in References]
T:244 [in References]
t:249 [in References]
T:25 [in StlcProp]
t:25 [in RecordSub]
T:250 [in References]
T:250 [in Norm]
t:251 [in Norm]
T:254 [in References]
t:257 [in Norm]
T:258 [in Norm]
t:26 [in Typechecking]
t:263 [in Norm]
t:268 [in Norm]
T:27 [in Typechecking]
t:27 [in Types]
t:272 [in Norm]
T:273 [in Norm]
t:276 [in Norm]
T:277 [in Norm]
t:28 [in Types]
t:28 [in Records]
t:29 [in Typechecking]
t:29 [in StlcProp]
t:29 [in Types]
t:3 [in Smallstep]
T:30 [in Typechecking]
T:31 [in StlcProp]
T:31 [in UseTactics]
t:32 [in StlcProp]
T:34 [in StlcProp]
t:35 [in StlcProp]
t:36 [in References]
T:36 [in Typechecking]
T:37 [in StlcProp]
T:37 [in Types]
T:37 [in Sub]
t:38 [in StlcProp]
t:39 [in StlcProp]
t:40 [in References]
t:40 [in Typechecking]
T:40 [in Sub]
T:41 [in StlcProp]
t:41 [in Types]
t:42 [in Smallstep]
t:42 [in Types]
t:43 [in Types]
T:44 [in StlcProp]
t:44 [in Types]
T:45 [in Types]
t:46 [in Smallstep]
t:47 [in Types]
t:49 [in Smallstep]
T:49 [in Types]
t:50 [in Types]
t:51 [in Norm]
t:52 [in Smallstep]
T:52 [in Types]
t:53 [in Types]
T:55 [in Types]
t:56 [in Types]
T:58 [in Types]
t:59 [in Types]
T:6 [in Typechecking]
T:61 [in Types]
t:64 [in Typechecking]
T:65 [in Typechecking]
t:65 [in StlcProp]
T:65 [in Stlc]
T:66 [in Stlc]
t:67 [in Typechecking]
T:68 [in Typechecking]
t:68 [in StlcProp]
T:68 [in Stlc]
t:69 [in Typechecking]
T:69 [in StlcProp]
t:7 [in StlcProp]
t:7 [in Types]
t:7 [in MoreStlc]
t:7 [in Norm]
t:7 [in Sub]
t:72 [in StlcProp]
T:72 [in RecordSub]
T:73 [in StlcProp]
t:74 [in Typechecking]
T:75 [in RecordSub]
t:75 [in UseTactics]
t:76 [in StlcProp]
T:77 [in StlcProp]
T:77 [in UseTactics]
T:77 [in Records]
T:8 [in StlcProp]
t:8 [in Types]
t:84 [in Typechecking]
t:85 [in Typechecking]
t:85 [in StlcProp]
t:86 [in UseAuto]
t:86 [in Typechecking]
t:87 [in Records]
T:88 [in UseAuto]
t:88 [in Typechecking]
t:89 [in UseAuto]
t:89 [in Typechecking]
t:89 [in Norm]
T:90 [in Norm]
T:91 [in UseAuto]
t:91 [in StlcProp]
t:91 [in Records]
t:92 [in UseAuto]
t:92 [in Norm]
T:92 [in Records]
t:92 [in Sub]
T:93 [in UseAuto]
T:93 [in Norm]
T:93 [in Sub]
t:94 [in Smallstep]
t:95 [in UseAuto]
T:95 [in RecordSub]
T:95 [in Records]
T:96 [in UseAuto]
t:96 [in StlcProp]
T:96 [in UseTactics]
T:97 [in StlcProp]
T:97 [in RecordSub]
t:97 [in Norm]
T:97 [in Records]
t:98 [in UseAuto]
t:98 [in StlcProp]
T:99 [in Norm]
T:99 [in Records]
T:99 [in Sub]
U
U1:107 [in RecordSub]U1:77 [in Sub]
U2:108 [in RecordSub]
U2:78 [in Sub]
U:104 [in RecordSub]
u:114 [in Equiv]
U:123 [in Records]
U:126 [in Sub]
U:136 [in Sub]
U:140 [in Sub]
U:144 [in Sub]
U:148 [in Sub]
U:152 [in Sub]
U:156 [in Sub]
U:160 [in Sub]
U:173 [in UseAuto]
U:180 [in RecordSub]
U:180 [in MoreStlc]
U:189 [in LibTactics]
U:22 [in StlcProp]
U:220 [in References]
U:28 [in StlcProp]
u:38 [in UseTactics]
U:39 [in Sub]
u:6 [in StlcProp]
U:73 [in Sub]
U:74 [in RecordSub]
U:74 [in UseTactics]
U:74 [in Sub]
U:79 [in Sub]
U:80 [in Sub]
U:82 [in Sub]
U:96 [in Norm]
V
varname:273 [in LibTactics]varname:274 [in LibTactics]
varname:275 [in LibTactics]
varname:276 [in LibTactics]
vi:149 [in RecordSub]
vi:60 [in Records]
vi:61 [in RecordSub]
vl:102 [in MoreStlc]
vr:35 [in RecordSub]
vr:38 [in Records]
V0:39 [in PE]
V0:62 [in PE]
V0:69 [in PE]
v0:72 [in MoreStlc]
v0:78 [in MoreStlc]
v1:101 [in MoreStlc]
V1:105 [in RecordSub]
v1:11 [in Smallstep]
v1:117 [in References]
v1:147 [in Smallstep]
v1:15 [in Smallstep]
v1:15 [in Norm]
v1:167 [in Smallstep]
v1:172 [in Smallstep]
v1:197 [in Smallstep]
v1:20 [in Smallstep]
v1:200 [in Smallstep]
v1:205 [in Smallstep]
v1:208 [in Smallstep]
v1:21 [in MoreStlc]
v1:213 [in Smallstep]
v1:216 [in Smallstep]
v1:222 [in Norm]
v1:224 [in Smallstep]
v1:227 [in Smallstep]
v1:23 [in MoreStlc]
v1:232 [in Smallstep]
v1:235 [in Smallstep]
v1:24 [in Sub]
v1:26 [in Norm]
v1:32 [in Stlc]
v1:34 [in Smallstep]
v1:34 [in RecordSub]
v1:34 [in MoreStlc]
v1:37 [in Records]
v1:39 [in Smallstep]
v1:40 [in Norm]
v1:45 [in Norm]
v1:48 [in MoreStlc]
v1:49 [in Norm]
v1:52 [in Records]
v1:53 [in RecordSub]
v1:54 [in References]
v1:60 [in Smallstep]
v1:65 [in Smallstep]
v1:66 [in Records]
v1:67 [in RecordSub]
v1:75 [in Smallstep]
V1:75 [in Sub]
v1:79 [in References]
v1:80 [in Smallstep]
v1:87 [in MoreStlc]
v1:89 [in Smallstep]
V2:106 [in RecordSub]
v2:12 [in Smallstep]
v2:16 [in Smallstep]
v2:16 [in Norm]
v2:168 [in Smallstep]
v2:20 [in Sub]
v2:201 [in Smallstep]
v2:209 [in Smallstep]
v2:217 [in Smallstep]
v2:22 [in MoreStlc]
v2:22 [in Norm]
v2:228 [in Smallstep]
v2:236 [in Smallstep]
v2:24 [in MoreStlc]
v2:28 [in Stlc]
v2:30 [in MoreStlc]
v2:35 [in Smallstep]
v2:46 [in Norm]
v2:47 [in References]
v2:48 [in Records]
v2:49 [in RecordSub]
v2:50 [in Norm]
v2:57 [in Smallstep]
v2:61 [in Smallstep]
v2:76 [in Smallstep]
V2:76 [in Sub]
v2:90 [in Smallstep]
V:10 [in HoareAsLogic]
V:101 [in PE]
v:102 [in UseAuto]
V:104 [in PE]
v:105 [in UseAuto]
v:106 [in Records]
v:108 [in UseAuto]
v:109 [in References]
V:115 [in PE]
V:123 [in PE]
v:125 [in Records]
v:128 [in Sub]
V:137 [in Sub]
V:141 [in Sub]
v:145 [in RecordSub]
V:145 [in Sub]
V:149 [in Sub]
V:153 [in Sub]
v:156 [in Norm]
V:157 [in Sub]
v:16 [in MoreStlc]
V:161 [in Sub]
v:18 [in MoreStlc]
v:182 [in RecordSub]
v:182 [in MoreStlc]
V:2 [in PE]
v:202 [in Norm]
v:21 [in Types]
v:213 [in Norm]
v:217 [in Norm]
v:221 [in Norm]
v:222 [in References]
v:230 [in Norm]
v:24 [in StlcProp]
v:24 [in Types]
V:26 [in PE]
v:262 [in Norm]
v:30 [in StlcProp]
V:366 [in PE]
v:39 [in UseTactics]
V:44 [in PE]
v:48 [in Smallstep]
V:57 [in PE]
V:6 [in PE]
V:61 [in PE]
V:64 [in PE]
V:67 [in PE]
v:68 [in Smallstep]
V:72 [in PE]
v:76 [in UseTactics]
V:76 [in PE]
V:80 [in PE]
v:83 [in Smallstep]
V:83 [in PE]
V:94 [in PE]
v:97 [in References]
v:98 [in Norm]
v:99 [in UseAuto]
W
w:40 [in UseTactics]X
xts:185 [in Norm]x':246 [in Norm]
x1:104 [in MoreStlc]
x1:118 [in Equiv]
x1:127 [in LibTactics]
x1:130 [in LibTactics]
x1:135 [in LibTactics]
x1:142 [in LibTactics]
x1:146 [in MoreStlc]
x1:151 [in LibTactics]
x1:162 [in LibTactics]
x1:163 [in MoreStlc]
x1:175 [in LibTactics]
x1:201 [in LibTactics]
x1:209 [in LibTactics]
x1:217 [in LibTactics]
x1:220 [in Norm]
x1:224 [in LibTactics]
x1:231 [in LibTactics]
x1:237 [in LibTactics]
x1:243 [in LibTactics]
x1:248 [in LibTactics]
x1:253 [in LibTactics]
x1:257 [in LibTactics]
x1:261 [in LibTactics]
x1:264 [in LibTactics]
x1:267 [in LibTactics]
x1:269 [in LibTactics]
x1:271 [in LibTactics]
x1:272 [in LibTactics]
x1:35 [in LibTactics]
x1:37 [in LibTactics]
x1:40 [in LibTactics]
x1:44 [in LibTactics]
x1:49 [in LibTactics]
x1:58 [in LibTactics]
x1:61 [in LibTactics]
x1:63 [in UseTactics]
x1:63 [in LibTactics]
x1:66 [in LibTactics]
x1:68 [in MoreStlc]
x1:69 [in LibTactics]
x1:73 [in MoreStlc]
x1:73 [in LibTactics]
x1:77 [in LibTactics]
x1:79 [in MoreStlc]
x1:82 [in LibTactics]
x1:87 [in LibTactics]
x1:93 [in MoreStlc]
x1:93 [in LibTactics]
x1:98 [in MoreStlc]
x1:99 [in LibTactics]
x2:100 [in LibTactics]
x2:105 [in MoreStlc]
x2:119 [in Equiv]
x2:132 [in LibTactics]
x2:137 [in LibTactics]
x2:144 [in LibTactics]
x2:149 [in MoreStlc]
x2:153 [in LibTactics]
x2:164 [in MoreStlc]
x2:164 [in LibTactics]
x2:177 [in LibTactics]
x2:202 [in LibTactics]
x2:210 [in LibTactics]
x2:218 [in LibTactics]
x2:225 [in LibTactics]
x2:232 [in LibTactics]
x2:238 [in LibTactics]
x2:244 [in LibTactics]
x2:249 [in LibTactics]
x2:254 [in LibTactics]
x2:258 [in LibTactics]
x2:262 [in LibTactics]
x2:265 [in LibTactics]
x2:268 [in LibTactics]
x2:270 [in LibTactics]
x2:38 [in LibTactics]
x2:41 [in LibTactics]
x2:45 [in LibTactics]
x2:50 [in LibTactics]
x2:64 [in UseTactics]
x2:64 [in LibTactics]
x2:67 [in LibTactics]
x2:70 [in MoreStlc]
x2:70 [in LibTactics]
x2:74 [in LibTactics]
x2:75 [in MoreStlc]
x2:78 [in LibTactics]
x2:81 [in MoreStlc]
x2:83 [in LibTactics]
x2:88 [in LibTactics]
x2:94 [in MoreStlc]
x2:94 [in LibTactics]
x2:99 [in MoreStlc]
x3:101 [in LibTactics]
x3:139 [in LibTactics]
x3:146 [in LibTactics]
x3:155 [in LibTactics]
x3:166 [in LibTactics]
x3:179 [in LibTactics]
x3:203 [in LibTactics]
x3:211 [in LibTactics]
x3:219 [in LibTactics]
x3:226 [in LibTactics]
x3:233 [in LibTactics]
x3:239 [in LibTactics]
x3:245 [in LibTactics]
x3:250 [in LibTactics]
x3:255 [in LibTactics]
x3:259 [in LibTactics]
x3:263 [in LibTactics]
x3:266 [in LibTactics]
x3:42 [in LibTactics]
x3:46 [in LibTactics]
x3:51 [in LibTactics]
x3:71 [in LibTactics]
x3:75 [in LibTactics]
x3:79 [in LibTactics]
x3:84 [in LibTactics]
x3:89 [in LibTactics]
x3:95 [in LibTactics]
x4:102 [in LibTactics]
x4:148 [in LibTactics]
x4:157 [in LibTactics]
x4:168 [in LibTactics]
x4:181 [in LibTactics]
x4:204 [in LibTactics]
x4:212 [in LibTactics]
x4:220 [in LibTactics]
x4:227 [in LibTactics]
x4:234 [in LibTactics]
x4:240 [in LibTactics]
x4:246 [in LibTactics]
x4:251 [in LibTactics]
x4:256 [in LibTactics]
x4:260 [in LibTactics]
x4:47 [in LibTactics]
x4:52 [in LibTactics]
x4:80 [in LibTactics]
x4:85 [in LibTactics]
x4:90 [in LibTactics]
x4:96 [in LibTactics]
x5:103 [in LibTactics]
x5:159 [in LibTactics]
x5:170 [in LibTactics]
x5:183 [in LibTactics]
x5:205 [in LibTactics]
x5:213 [in LibTactics]
x5:221 [in LibTactics]
x5:228 [in LibTactics]
x5:235 [in LibTactics]
x5:241 [in LibTactics]
x5:247 [in LibTactics]
x5:252 [in LibTactics]
x5:53 [in LibTactics]
x5:91 [in LibTactics]
x5:97 [in LibTactics]
x6:104 [in LibTactics]
x6:172 [in LibTactics]
x6:185 [in LibTactics]
x6:206 [in LibTactics]
x6:214 [in LibTactics]
x6:222 [in LibTactics]
x6:229 [in LibTactics]
x6:236 [in LibTactics]
x6:242 [in LibTactics]
x7:187 [in LibTactics]
x7:207 [in LibTactics]
x7:215 [in LibTactics]
x7:223 [in LibTactics]
x7:230 [in LibTactics]
x8:208 [in LibTactics]
x8:216 [in LibTactics]
X:1 [in Records]
x:10 [in Stlc]
x:10 [in UseTactics]
x:100 [in UseTactics]
x:102 [in Sub]
x:103 [in UseTactics]
x:105 [in UseTactics]
x:105 [in Norm]
x:106 [in Norm]
x:109 [in Norm]
x:110 [in MoreStlc]
x:112 [in RecordSub]
x:112 [in Norm]
x:112 [in Sub]
x:113 [in MoreStlc]
x:113 [in Equiv]
x:115 [in RecordSub]
x:116 [in Norm]
x:116 [in LibTactics]
x:119 [in UseAuto]
x:12 [in References]
x:12 [in MoreStlc]
x:12 [in Norm]
x:12 [in Sub]
x:120 [in Norm]
X:121 [in Smallstep]
x:122 [in Equiv]
x:122 [in Records]
x:124 [in Norm]
x:125 [in Smallstep]
x:125 [in Sub]
x:126 [in Smallstep]
x:127 [in Hoare]
x:128 [in Norm]
X:129 [in Smallstep]
x:129 [in References]
x:131 [in Smallstep]
x:131 [in Norm]
x:132 [in References]
X:133 [in Smallstep]
x:133 [in Equiv]
x:134 [in Norm]
x:135 [in Smallstep]
x:136 [in Norm]
x:138 [in UseAuto]
x:139 [in Norm]
X:140 [in Smallstep]
x:143 [in UseAuto]
x:144 [in Norm]
x:145 [in Equiv]
x:145 [in Norm]
x:147 [in Norm]
X:15 [in UseTactics]
x:154 [in RecordSub]
x:155 [in UseAuto]
x:156 [in UseAuto]
x:157 [in UseAuto]
x:158 [in UseAuto]
x:16 [in Stlc]
x:160 [in UseAuto]
X:161 [in Hoare]
x:161 [in RecordSub]
x:162 [in UseAuto]
x:164 [in UseAuto]
x:165 [in UseAuto]
x:166 [in UseAuto]
x:166 [in RecordSub]
x:17 [in Sub]
x:175 [in Hoare]
x:179 [in RecordSub]
x:179 [in MoreStlc]
x:183 [in UseAuto]
x:185 [in UseAuto]
x:188 [in UseAuto]
X:188 [in Norm]
x:189 [in References]
x:19 [in UseTactics]
x:19 [in Norm]
x:190 [in UseAuto]
x:192 [in LibTactics]
x:193 [in UseAuto]
X:193 [in Norm]
x:199 [in UseAuto]
x:20 [in Stlc]
x:20 [in UseTactics]
x:200 [in Norm]
x:205 [in UseAuto]
x:206 [in Norm]
x:209 [in Norm]
x:21 [in StlcProp]
X:21 [in LibTactics]
x:212 [in Hoare]
x:212 [in Norm]
x:215 [in UseAuto]
x:215 [in Norm]
x:219 [in References]
x:219 [in Norm]
x:22 [in LibTactics]
x:229 [in Norm]
X:23 [in Smallstep]
x:23 [in References]
x:23 [in RecordSub]
x:233 [in Norm]
x:235 [in Norm]
x:237 [in Hoare]
x:239 [in References]
X:24 [in Smallstep]
x:242 [in Norm]
x:245 [in Norm]
X:248 [in Hoare]
x:249 [in Norm]
x:25 [in Stlc]
X:252 [in Hoare]
X:254 [in Hoare]
X:255 [in References]
x:256 [in Norm]
x:259 [in References]
x:26 [in Smallstep]
X:26 [in Hoare]
x:26 [in Records]
x:26 [in LibTactics]
x:261 [in References]
x:261 [in Norm]
x:267 [in Hoare]
x:27 [in StlcProp]
x:27 [in MoreStlc]
x:274 [in Norm]
x:275 [in Norm]
x:28 [in Hoare]
x:28 [in LibTactics]
x:282 [in LibTactics]
X:30 [in Hoare]
x:30 [in References]
x:30 [in RecordSub]
X:316 [in Hoare]
x:32 [in Hoare]
x:33 [in References]
x:33 [in Records]
x:35 [in PE]
x:38 [in UseAuto]
x:41 [in UseAuto]
x:41 [in UseTactics]
x:41 [in Equiv]
X:42 [in Equiv]
X:44 [in Smallstep]
x:44 [in References]
x:45 [in UseAuto]
x:45 [in Records]
x:46 [in StlcProp]
x:46 [in RecordSub]
x:46 [in Stlc]
x:47 [in UseAuto]
x:48 [in UseTactics]
x:49 [in Stlc]
x:49 [in Sub]
x:5 [in StlcProp]
X:5 [in UseTactics]
x:5 [in MoreStlc]
x:5 [in Norm]
x:5 [in Sub]
x:50 [in UseAuto]
x:52 [in Sub]
X:54 [in Hoare]
x:55 [in Norm]
x:58 [in Norm]
X:59 [in Hoare]
x:59 [in UseTactics]
X:6 [in Hoare2]
x:61 [in Hoare2]
x:62 [in Equiv]
x:64 [in UseAuto]
x:65 [in Hoare2]
x:66 [in StlcProp]
x:66 [in Hoare2]
x:67 [in StlcProp]
x:7 [in References]
x:7 [in Stlc]
x:73 [in UseTactics]
x:76 [in Records]
x:78 [in StlcProp]
x:78 [in Records]
x:8 [in UseTactics]
x:83 [in StlcProp]
x:87 [in Sub]
x:89 [in PE]
x:9 [in UseTactics]
X:94 [in Hoare2]
x:95 [in UseTactics]
x:95 [in Norm]
x:96 [in Sub]
X:98 [in Hoare2]
Y
y1:128 [in LibTactics]y1:131 [in LibTactics]
y1:136 [in LibTactics]
y1:143 [in LibTactics]
y1:152 [in LibTactics]
y1:163 [in LibTactics]
y1:176 [in LibTactics]
y1:27 [in Smallstep]
y1:59 [in LibTactics]
y1:60 [in LibTactics]
y1:65 [in UseTactics]
y1:65 [in LibTactics]
y1:72 [in LibTactics]
y1:81 [in LibTactics]
y1:92 [in LibTactics]
y2:133 [in LibTactics]
y2:138 [in LibTactics]
y2:145 [in LibTactics]
y2:154 [in LibTactics]
y2:165 [in LibTactics]
y2:178 [in LibTactics]
y2:28 [in Smallstep]
y2:66 [in UseTactics]
y3:140 [in LibTactics]
y3:147 [in LibTactics]
y3:156 [in LibTactics]
y3:167 [in LibTactics]
y3:180 [in LibTactics]
y4:149 [in LibTactics]
y4:158 [in LibTactics]
y4:169 [in LibTactics]
y4:182 [in LibTactics]
y5:160 [in LibTactics]
y5:171 [in LibTactics]
y5:184 [in LibTactics]
y6:173 [in LibTactics]
y6:186 [in LibTactics]
y7:188 [in LibTactics]
y:113 [in Norm]
y:117 [in LibTactics]
y:126 [in Equiv]
y:127 [in Smallstep]
y:132 [in Smallstep]
y:136 [in Smallstep]
y:146 [in Norm]
y:184 [in UseAuto]
y:186 [in UseAuto]
y:189 [in UseAuto]
y:191 [in UseAuto]
y:193 [in LibTactics]
y:194 [in UseAuto]
y:200 [in UseAuto]
y:206 [in UseAuto]
y:260 [in References]
y:262 [in References]
y:283 [in LibTactics]
y:33 [in Hoare]
y:36 [in PE]
y:42 [in UseTactics]
y:49 [in UseTactics]
y:53 [in StlcProp]
y:60 [in UseTactics]
y:87 [in PE]
y:96 [in Records]
Z
z:128 [in Smallstep]z:137 [in Smallstep]
z:187 [in UseAuto]
z:195 [in UseAuto]
z:201 [in UseAuto]
z:207 [in UseAuto]
z:263 [in References]
z:43 [in UseTactics]
z:61 [in UseTactics]
Module Index
C
CImp [in Smallstep]Combined [in Smallstep]
D
DeterministicImp [in UseAuto]E
EqualityExamples [in UseTactics]ExamplePrettyAssertions [in Hoare]
ExamplesLets [in UseTactics]
ExAssertions [in Hoare]
F
FirstTry [in Typechecking]G
GenExample [in UseTactics]H
Himp [in Hoare]Himp [in Equiv]
Himp2 [in Hoare2]
HoareAssertAssume [in Hoare]
I
If1 [in Hoare]IntrovExamples [in UseTactics]
InvertsExamples [in UseTactics]
InvertsExamples1 [in UseTactics]
L
LibTacticsCompatibility [in LibTactics]Loop [in PE]
N
NaryExamples [in UseTactics]P
PreservationProgressReferences [in UseAuto]PreservationProgressStlc [in UseAuto]
R
RecordSub [in RecordSub]RecordSub.Examples [in RecordSub]
RecordSub.Examples2 [in RecordSub]
RepeatExercise [in Hoare]
RingDemo [in UseAuto]
S
Semantics [in UseAuto]SimpleArith1 [in Smallstep]
SimpleArith2 [in Smallstep]
SimpleArith3 [in Smallstep]
SkipExample [in UseTactics]
SortExamples [in UseTactics]
StepFunction [in Typechecking]
STLC [in Stlc]
STLCArith [in StlcProp]
STLCChecker [in Typechecking]
STLCExtended [in MoreStlc]
STLCExtendedRecords [in Records]
STLCExtendedRecords.FirstTry [in Records]
STLCExtended.Examples [in MoreStlc]
STLCExtended.Examples.FixTest1 [in MoreStlc]
STLCExtended.Examples.FixTest2 [in MoreStlc]
STLCExtended.Examples.FixTest3 [in MoreStlc]
STLCExtended.Examples.FixTest4 [in MoreStlc]
STLCExtended.Examples.LetTest [in MoreStlc]
STLCExtended.Examples.ListTest [in MoreStlc]
STLCExtended.Examples.Numtest [in MoreStlc]
STLCExtended.Examples.ProdTest [in MoreStlc]
STLCExtended.Examples.Sumtest1 [in MoreStlc]
STLCExtended.Examples.Sumtest2 [in MoreStlc]
StlcImpl [in Typechecking]
STLCProp [in StlcProp]
STLCRef [in References]
STLCRef.ExampleVariables [in References]
STLCRef.RefsAndNontermination [in References]
STLCSub [in Sub]
STLCSub.Examples [in Sub]
STLCSub.Examples2 [in Sub]
STLCSub.FormalThoughtExercises [in Sub]
STLCTypes [in Typechecking]
SubtypingInversion [in UseAuto]
T
Temp1 [in Smallstep]Temp2 [in Smallstep]
Temp3 [in Smallstep]
Temp4 [in Smallstep]
Temp4.Temp5 [in Smallstep]
TM [in Types]
TypecheckerExtensions [in Typechecking]
U
UnfoldsExample [in UseTactics]Variable Index
E
equatesLemma.A0 [in LibTactics]equatesLemma.A1 [in LibTactics]
equatesLemma.A2 [in LibTactics]
equatesLemma.A3 [in LibTactics]
equatesLemma.A4 [in LibTactics]
equatesLemma.A5 [in LibTactics]
equatesLemma.A6 [in LibTactics]
F
FuncEq.A1 [in LibTactics]FuncEq.A2 [in LibTactics]
FuncEq.A3 [in LibTactics]
FuncEq.A4 [in LibTactics]
FuncEq.A5 [in LibTactics]
FuncEq.A6 [in LibTactics]
FuncEq.A7 [in LibTactics]
FuncEq.B [in LibTactics]
Library Index
B
BibE
EquivH
HoareHoareAsLogic
Hoare2
L
LibTacticsM
MoreStlcN
NormP
PEPostscript
Preface
R
RecordsRecordSub
References
S
SmallstepStlc
StlcProp
Sub
T
TypecheckingTypes
U
UseAutoUseTactics
Lemma Index
A
aequiv_example [in Equiv]aeval_weakening [in Equiv]
always_loop_hoare [in Hoare]
applys_eq_step [in LibTactics]
applys_eq_step_dep [in LibTactics]