Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (39074 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (477 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (30413 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (242 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (554 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (249 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3616 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (570 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (583 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (102 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (68 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (114 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (45 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (5 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2012 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (24 entries)

S (lemma)

safety_monotonicity [in seplog.cryptoasm.mips_syntax]
safety_monotonicity0 [in seplog.cryptoasm.mips_syntax]
safe_termination_copy_s_s [in seplog.begcd.copy_s_s_safe_termination]
safe_termination_one_u [in seplog.begcd.multi_one_u_safe_termination]
safe_termination_multi_add_s_u [in seplog.begcd.multi_add_s_u_safe_termination]
safe_termination_multi_sub_s_s_u [in seplog.begcd.multi_sub_s_s_u_safe_termination]
safe_termination_multi_sub_s_s_s [in seplog.begcd.multi_sub_s_s_s_safe_termination]
safe_termination_multi_add_s_s_u [in seplog.begcd.multi_add_s_s_u_safe_termination]
safe_termination_multi_sub_s_u [in seplog.begcd.multi_sub_s_u_safe_termination]
safe_cast_phy_uchar_zext [in seplog.seplogC.C_expr]
scale_mod [in seplog.lib.machine_int]
sepClst_equiv [in seplog.seplogC.C_reverse_list_header]
sepClst_ind_new [in seplog.seplogC.C_reverse_list_header]
seplogClst_inde [in seplog.seplogC.C_reverse_list_header]
Seplog.ArrayI_disj_heap [in seplog.seplog.seplog]
Seplog.ArrayI_inde_store [in seplog.seplog.seplog]
Seplog.Array_concat [in seplog.seplog.seplog]
Seplog.Array_disj [in seplog.seplog.seplog]
Seplog.Array_split [in seplog.seplog.seplog]
Seplog.Array_concat_split [in seplog.seplog.seplog]
Seplog.Array_inde_list [in seplog.seplog.seplog]
Seplog.Array_inde [in seplog.seplog.seplog]
Seplog.Array_inde_store [in seplog.seplog.seplog]
Seplog.cmd0_terminate [in seplog.seplog.seplog]
Seplog.Data_destructive_upd_inv [in seplog.seplog.seplog]
Seplog.Data_destructive_upd_inv2 [in seplog.seplog.seplog]
Seplog.entails_wp_assigns [in seplog.seplog.seplog]
Seplog.exec0_to_wp0 [in seplog.seplog.seplog]
Seplog.exec0_from_wp0 [in seplog.seplog.seplog]
Seplog.exec0_free_not_None [in seplog.seplog.seplog]
Seplog.exec0_mutation_not_None [in seplog.seplog.seplog]
Seplog.exec0_lookup_not_None [in seplog.seplog.seplog]
Seplog.exec0_assign_inv [in seplog.seplog.seplog]
Seplog.forward_reasoning [in seplog.seplog.seplog]
Seplog.frame_rule'' [in seplog.seplog.seplog]
Seplog.frame_rule' [in seplog.seplog.seplog]
Seplog.frame_rule_R [in seplog.seplog.seplog]
Seplog.frame_rule0 [in seplog.seplog.seplog]
Seplog.fresh_lst_inde [in seplog.seplog.seplog]
Seplog.from_none0 [in seplog.seplog.seplog]
Seplog.hoare_mutation_frame_rule [in seplog.seplog.seplog]
Seplog.hoare_mutation_backwards'' [in seplog.seplog.seplog]
Seplog.hoare_mutation_backwards' [in seplog.seplog.seplog]
Seplog.hoare_mutation_backwards_alternative [in seplog.seplog.seplog]
Seplog.hoare_mutation_backwards [in seplog.seplog.seplog]
Seplog.hoare_mutation_global_alternative [in seplog.seplog.seplog]
Seplog.hoare_mutation_global [in seplog.seplog.seplog]
Seplog.hoare_free_global_backwards [in seplog.seplog.seplog]
Seplog.hoare_frame_rule_and [in seplog.seplog.seplog]
Seplog.hoare_frame_rule_and0 [in seplog.seplog.seplog]
Seplog.hoare_frame_rule_and'0 [in seplog.seplog.seplog]
Seplog.hoare_mutation'' [in seplog.seplog.seplog]
Seplog.hoare_mutation' [in seplog.seplog.seplog]
Seplog.hoare_mutation_local [in seplog.seplog.seplog]
Seplog.hoare_lookup_back_strictly_exact [in seplog.seplog.seplog]
Seplog.hoare_lookup_back_alternative [in seplog.seplog.seplog]
Seplog.hoare_lookup_back'' [in seplog.seplog.seplog]
Seplog.hoare_lookup_back' [in seplog.seplog.seplog]
Seplog.hoare_lookup_back [in seplog.seplog.seplog]
Seplog.hoare_lookup'' [in seplog.seplog.seplog]
Seplog.hoare_lookup' [in seplog.seplog.seplog]
Seplog.hoare_lookup_simple [in seplog.seplog.seplog]
Seplog.hoare_assign [in seplog.seplog.seplog]
Seplog.hoare_assign' [in seplog.seplog.seplog]
Seplog.hoare_skip' [in seplog.seplog.seplog]
Seplog.hoare_complete [in seplog.seplog.seplog]
Seplog.hoare_false [in seplog.seplog.seplog]
Seplog.hoare_false0 [in seplog.seplog.seplog]
Seplog.inde_ifte [in seplog.seplog.seplog]
Seplog.inde_seq [in seplog.seplog.seplog]
Seplog.intro_fresh_var' [in seplog.seplog.seplog]
Seplog.mapstos_to_array [in seplog.seplog.seplog]
Seplog.semop_m.eval_b_neg [in seplog.seplog.seplog]
Seplog.soundness [in seplog.seplog.seplog]
Seplog.soundness_alternative [in seplog.seplog.seplog]
Seplog.soundness0 [in seplog.seplog.seplog]
Seplog.vc_soundness [in seplog.seplog.seplog]
Seplog.wp_vc_util [in seplog.seplog.seplog]
Seplog.wp_mutation_sep_con' [in seplog.seplog.seplog]
Seplog.wp_mutation_sep_con [in seplog.seplog.seplog]
Seplog.wp_semantics_sound [in seplog.seplog.seplog]
Seplog.wp_semantics_sound0 [in seplog.seplog.seplog]
Seplog.wp_assigns_fresh' [in seplog.seplog.seplog]
Seplog.wp_assigns_fresh [in seplog.seplog.seplog]
Seplog.wp_assigns_lookup [in seplog.seplog.seplog]
Seplog.wp_assigns_subst_b_lst [in seplog.seplog.seplog]
Seplog.wp_assigns_mapsto_inv [in seplog.seplog.seplog]
Seplog.wp_assigns_mapsto [in seplog.seplog.seplog]
Seplog.wp_assigns_sepimp [in seplog.seplog.seplog]
Seplog.wp_assigns_sepcon [in seplog.seplog.seplog]
Seplog.wp_assigns_exists [in seplog.seplog.seplog]
Seplog.wp_assigns_and [in seplog.seplog.seplog]
Seplog.wp_assigns_and_inv [in seplog.seplog.seplog]
Seplog.wp_assigns_imp [in seplog.seplog.seplog]
Seplog.wp_assigns' [in seplog.seplog.seplog]
Seplog.wp_assigns_app [in seplog.seplog.seplog]
Seplog.wp0_no_err [in seplog.seplog.seplog]
sequiv_s2Z_si32_of_phy [in seplog.seplogC.C_expr_ground]
sequiv_ge [in seplog.seplogC.C_expr_ground]
sequiv_intsa_uchar_sc [in seplog.seplogC.C_expr_equiv]
sequiv_sub_e_sc [in seplog.seplogC.C_expr_equiv]
sequiv_gt_sym [in seplog.seplogC.C_expr_equiv]
sequiv_ge_sym [in seplog.seplogC.C_expr_equiv]
sequiv_add_p_cst [in seplog.seplogC.C_expr_equiv]
sequiv_add_e_sc_pos4 [in seplog.seplogC.C_expr_equiv]
sequiv_add_e_sc_pos3 [in seplog.seplogC.C_expr_equiv]
sequiv_add_e_sc_pos [in seplog.seplogC.C_expr_equiv]
sequiv_add_e_sc [in seplog.seplogC.C_expr_equiv]
sequiv_add_pe_0 [in seplog.seplogC.C_expr_equiv]
sequiv_bop_re_sc [in seplog.seplogC.C_expr_equiv]
seq_forall_exists [in seplog.lib.seq_ext]
set_in_left_ssl_ctxt [in seplog.seplogC.POLAR_ssl_ctxt]
set_max_minor_ver_ssl_ctxt [in seplog.seplogC.POLAR_ssl_ctxt]
set_max_major_ver_sl_ctxt [in seplog.seplogC.POLAR_ssl_ctxt]
set_minor_ver_ssl_ctxt [in seplog.seplogC.POLAR_ssl_ctxt]
set_major_ver_ssl_ctxt [in seplog.seplogC.POLAR_ssl_ctxt]
set_state_ssl_ctxt [in seplog.seplogC.POLAR_ssl_ctxt]
sext_0 [in seplog.lib.machine_int]
SGoto_Hoare.hoare_sgoto_complete [in seplog.lib.sgoto_hoare]
SGoto_Hoare.wlp_completeness [in seplog.lib.sgoto_hoare]
SGoto_Hoare.hoare_sgoto_sound [in seplog.lib.sgoto_hoare]
SGoto_Hoare.restrict_cplt_dom [in seplog.lib.sgoto_hoare]
SGoto_Hoare.restrict_dom [in seplog.lib.sgoto_hoare]
SGoto.determinacy [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_refl [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_refl' [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_seq1 [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_seq1' [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_seq0 [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_seq0' [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_jmp [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_cjmp_false [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_cjmp_true [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_cmd [in seplog.lib.sgoto]
SGoto.exec_sgoto_inv_cmd' [in seplog.lib.sgoto]
SGoto.exec_sgoto_nil [in seplog.lib.sgoto]
SGoto.In_U_In_sdom [in seplog.lib.sgoto]
SGoto.lbl_sdom_dec [in seplog.lib.sgoto]
SGoto.neutrality [in seplog.lib.sgoto]
SGoto.not_in_sdom_sS' [in seplog.lib.sgoto]
SGoto.not_in_sdom_sS [in seplog.lib.sgoto]
SGoto.postlabels [in seplog.lib.sgoto]
SGoto.postlabels_cmd [in seplog.lib.sgoto]
SGoto.preservation [in seplog.lib.sgoto]
SGoto.redseq_sC_inv_none [in seplog.lib.sgoto]
SGoto.redseq_trans_inv2 [in seplog.lib.sgoto]
SGoto.redseq_trans_inv [in seplog.lib.sgoto]
SGoto.reflection_of_stuck_redseq [in seplog.lib.sgoto]
SGoto.sdom_dom [in seplog.lib.sgoto]
SGoto.sdom_dec [in seplog.lib.sgoto]
SGoto.sem_equ_com [in seplog.lib.sgoto]
SGoto.sem_equ_com' [in seplog.lib.sgoto]
SGoto.sem_equ_neu [in seplog.lib.sgoto]
SGoto.sem_equ_ass [in seplog.lib.sgoto]
SGoto.U_ass [in seplog.lib.sgoto]
SGoto.wellformed_wellformed_goto [in seplog.lib.sgoto]
SGoto.wellformed_ass' [in seplog.lib.sgoto]
SGoto.wellformed_ass [in seplog.lib.sgoto]
SGoto.wellformed_neu [in seplog.lib.sgoto]
SGoto.wellformed_In_R [in seplog.lib.sgoto]
SGoto.wellformed_In_L [in seplog.lib.sgoto]
SGoto.wellformed_inv_R [in seplog.lib.sgoto]
SGoto.wellformed_inv_L [in seplog.lib.sgoto]
sha1_update_triple [in seplog.seplogC.POLAR_library_functions_triple]
shl_Z2u [in seplog.lib.machine_int]
shl_0 [in seplog.lib.machine_int]
shrl_2 [in seplog.lib.machine_int]
sigma_impl_correct [in seplog.seplog.frag_list_entail]
sigma_eq_correct [in seplog.seplog.frag_list_entail]
Sigma_get_cell_val_correct [in seplog.seplog.frag]
Sigma_term_term_eq_correct [in seplog.seplog.frag]
Sigma_elt_term_extract'_correct [in seplog.seplog.frag]
Sigma_elt_term_extract_correct [in seplog.seplog.frag]
Sigma_elt_eq_correct [in seplog.seplog.frag]
Sigma_clean_epsi_correct' [in seplog.seplog.frag]
Sigma_clean_epsi_correct [in seplog.seplog.frag]
simpl_orlist_correct [in seplog.seplog.expr_b_dp]
simpl_andlist_correct [in seplog.seplog.expr_b_dp]
simpl_expr_b_correct [in seplog.seplog.expr_b_dp]
simpl_constraint_correct [in seplog.seplog.expr_b_dp]
simpl_varlist_constraint_correct [in seplog.seplog.expr_b_dp]
simpl_expr_correct [in seplog.seplog.expr_b_dp]
simpl_expr_fp_correct [in seplog.seplog.expr_b_dp]
simpl_expr'_correct [in seplog.seplog.expr_b_dp]
Simu.equiv_pcode_example3 [in seplog.begcd.simu]
Simu.equiv_pcode_example2 [in seplog.begcd.simu]
Simu.equiv_pcode_example [in seplog.begcd.simu]
Simu.equiv_pcode_expr [in seplog.begcd.simu]
Simu.equiv_pcode_seq [in seplog.begcd.simu]
Simu.equiv_pcode_example_assign [in seplog.begcd.simu]
Simu.equiv_pcode_uop [in seplog.begcd.simu]
Simu.equiv_pcode_op [in seplog.begcd.simu]
Simu.equiv_pcode_sym [in seplog.begcd.simu]
Simu.equiv_pcode_trans [in seplog.begcd.simu]
Simu.fwd_sim_ifte_spec [in seplog.begcd.simu]
Simu.fwd_sim_ifte [in seplog.begcd.simu]
Simu.fwd_sim_while_alt [in seplog.begcd.simu]
Simu.fwd_sim_while [in seplog.begcd.simu]
Simu.fwd_sim_b_cond_neg [in seplog.begcd.simu]
Simu.fwd_sim_b_cond [in seplog.begcd.simu]
Simu.fwd_sim_b_stren [in seplog.begcd.simu]
Simu.fwd_sim_b_fwd_sim_b' [in seplog.begcd.simu]
Simu.fwd_sim_b_pull_out [in seplog.begcd.simu]
Simu.fwd_sim_bck_sim [in seplog.begcd.simu]
Simu.fwd_sim_seq [in seplog.begcd.simu]
Simu.fwd_sim_pcode_equiv [in seplog.begcd.simu]
Simu.fwd_sim_assoc_R [in seplog.begcd.simu]
Simu.fwd_sim_assoc_L [in seplog.begcd.simu]
Simu.fwd_sim_stren [in seplog.begcd.simu]
Simu.invariant_equiv [in seplog.begcd.simu]
Simu.pfwd_sim_fwd_sim_spec [in seplog.begcd.simu]
Simu.pfwd_sim_fwd_sim [in seplog.begcd.simu]
Simu.pfwd_sim_stren [in seplog.begcd.simu]
Simu.rela_hoare_ignore_R [in seplog.begcd.simu]
Simu.rela_hoare_ifte [in seplog.begcd.simu]
Simu.rela_hoare_seq [in seplog.begcd.simu]
Simu.rela_hoare_weak [in seplog.begcd.simu]
Simu.rela_hoare_stren [in seplog.begcd.simu]
Simu.safe_termination_pull_out [in seplog.begcd.simu]
Simu.safe_termination_stren [in seplog.begcd.simu]
sim_begcd_prelude [in seplog.begcd.begcd_mips_prelude]
sint_shl_e_to_i32_ge [in seplog.seplogC.C_expr_ground]
sint_of_logK [in seplog.seplogC.C_value]
sizeof_leq_foldl [in seplog.seplogC.C_types_fp]
sizeof_gt0 [in seplog.seplogC.C_types_fp]
sizeof_ind [in seplog.seplogC.C_types_fp]
sizeof_foldl [in seplog.seplogC.C_types_fp]
sizeof_ptyp [in seplog.seplogC.C_types_fp]
sizeof_ityp [in seplog.seplogC.C_types_fp]
size_sc [in seplog.seplogC.C_expr]
size_Z2ints [in seplog.lib.multi_int]
size_listbit_to_ints [in seplog.lib.multi_int]
size_idel_last' [in seplog.lib.seq_ext]
size_idel_last [in seplog.lib.seq_ext]
size_idel [in seplog.lib.seq_ext]
size_upd_nth [in seplog.lib.seq_ext]
size_slice_exact [in seplog.lib.seq_ext]
size_slice_leq [in seplog.lib.seq_ext]
size_phy2seq [in seplog.seplogC.C_value]
size0_get_fields [in seplog.seplogC.C_types]
si2s_Z2u [in seplog.cryptoasm.mips_pp]
si2s_Z2s [in seplog.cryptoasm.mips_pp]
si32_of_phy_gb_or_e [in seplog.seplogC.C_expr_ground]
si32_of_phy_gb_add_e [in seplog.seplogC.C_expr_ground]
si32_of_phy_binop_ne [in seplog.seplogC.C_expr]
si32_of_phy_sc [in seplog.seplogC.C_expr]
si32_of_phy_safe_cast_phy_uchar [in seplog.seplogC.C_expr]
si32_of_phyK [in seplog.seplogC.C_value]
si32_of_phy_inj [in seplog.seplogC.C_value]
slices_sem [in seplog.lib.seq_ext]
slice_app [in seplog.lib.seq_ext]
slice_shift [in seplog.lib.seq_ext]
soundness [in seplog.cryptoasm.mips_seplog]
soundness0 [in seplog.cryptoasm.mips_seplog]
soundness0_total [in seplog.cryptoasm.mips_seplog]
split_verif2 [in seplog.seplog.topsy_hmAlloc2]
split_verif [in seplog.seplog.topsy_hmAlloc]
ssl_fetch_input_inde [in seplog.seplogC.POLAR_library_functions_triple]
ssl_fetch_input_triple [in seplog.seplogC.POLAR_library_functions_triple]
star_com_correct' [in seplog.seplog.frag_list_entail]
star_com_correct [in seplog.seplog.frag_list_entail]
star_assoc_left_correct' [in seplog.seplog.frag_list_entail]
star_assoc_left_correct [in seplog.seplog.frag_list_entail]
StateBiplProp.and_L_1 [in seplog.lib.while_bipl]
StateBiplProp.and_L_1 [in seplog.lib.while_proc_bipl]
StateBiplProp.ent_L_or [in seplog.lib.while_bipl]
StateBiplProp.ent_R_or_2 [in seplog.lib.while_bipl]
StateBiplProp.ent_R_or_1 [in seplog.lib.while_bipl]
StateBiplProp.ent_R_T [in seplog.lib.while_bipl]
StateBiplProp.ent_L_F [in seplog.lib.while_bipl]
StateBiplProp.ent_trans [in seplog.lib.while_bipl]
StateBiplProp.ent_id [in seplog.lib.while_bipl]
StateBiplProp.ent_L_or [in seplog.lib.while_proc_bipl]
StateBiplProp.ent_R_or_2 [in seplog.lib.while_proc_bipl]
StateBiplProp.ent_R_or_1 [in seplog.lib.while_proc_bipl]
StateBiplProp.ent_R_T [in seplog.lib.while_proc_bipl]
StateBiplProp.ent_L_F [in seplog.lib.while_proc_bipl]
StateBiplProp.ent_trans [in seplog.lib.while_proc_bipl]
StateBiplProp.ent_id [in seplog.lib.while_proc_bipl]
StateBiplProp.equiv_imp2 [in seplog.lib.while_bipl]
StateBiplProp.equiv_imp [in seplog.lib.while_bipl]
StateBiplProp.equiv_def [in seplog.lib.while_bipl]
StateBiplProp.equiv_trans [in seplog.lib.while_bipl]
StateBiplProp.equiv_sym [in seplog.lib.while_bipl]
StateBiplProp.equiv_refl [in seplog.lib.while_bipl]
StateBiplProp.equiv_def [in seplog.lib.while_proc_bipl]
StateBiplProp.equiv_trans [in seplog.lib.while_proc_bipl]
StateBiplProp.equiv_sym [in seplog.lib.while_proc_bipl]
StateBiplProp.equiv_refl [in seplog.lib.while_proc_bipl]
StateBiplProp.equiv1 [in seplog.lib.while_proc_bipl]
StateBiplProp.equiv2 [in seplog.lib.while_proc_bipl]
StateBiplProp.False_lhs [in seplog.lib.while_proc_bipl]
StateBiplProp.F_is_not_T [in seplog.lib.while_bipl]
StateBiplProp.F_is_not_T [in seplog.lib.while_proc_bipl]
state_mint_inj [in seplog.begcd.simu]
state_mint_part2_three_variables [in seplog.begcd.simu]
state_mint_part2_two_variables [in seplog.begcd.simu]
state_mint_part2_one_variable_unsign [in seplog.begcd.simu]
state_mint_part2_one_variable [in seplog.begcd.simu]
state_mint_store_upd [in seplog.begcd.simu]
state_mint_invariant [in seplog.begcd.simu]
state_mint_signed_slen_L [in seplog.begcd.simu]
state_mint_signed_fit_ptr [in seplog.begcd.simu]
state_mint_head_unsign_fit [in seplog.begcd.simu]
state_mint_align [in seplog.begcd.simu]
state_mint_var_mint [in seplog.begcd.simu]
store_get_upd_neq [in seplog.seplogC.C_expr]
store_upd_get_eq [in seplog.seplogC.C_expr]
store_get_upd_eq [in seplog.seplogC.C_expr]
store_upd_helper [in seplog.seplogC.C_expr]
store_get_helper2 [in seplog.seplogC.C_expr]
store_get_helper [in seplog.seplogC.C_expr]
store_irrelevance [in seplog.seplogC.C_expr]
store.acxhi_zero [in seplog.cryptoasm.mips_bipl]
store.acx_mflhxu_op [in seplog.cryptoasm.mips_bipl]
store.acx_mtlo_op [in seplog.cryptoasm.mips_bipl]
store.acx_mthi_op [in seplog.cryptoasm.mips_bipl]
store.acx_upd [in seplog.cryptoasm.mips_bipl]
store.acx_size_min [in seplog.cryptoasm.mips_bipl]
store.concat_acx_hilo [in seplog.cryptoasm.mips_bipl]
Store.extensionality [in seplog.seplog.bipl]
Store.get_difs' [in seplog.seplog.bipl]
Store.get_difs [in seplog.seplog.bipl]
Store.get_proj [in seplog.seplog.bipl]
Store.get_proj' [in seplog.seplog.bipl]
Store.get_upd' [in seplog.seplog.bipl]
Store.get_upds [in seplog.seplog.bipl]
Store.get_upd [in seplog.seplog.bipl]
Store.get_emp [in seplog.seplog.bipl]
store.get_mtlo_op [in seplog.cryptoasm.mips_bipl]
store.get_mthi_op [in seplog.cryptoasm.mips_bipl]
store.get_msubu_op [in seplog.cryptoasm.mips_bipl]
store.get_maddu_op [in seplog.cryptoasm.mips_bipl]
store.get_mflhxu_op [in seplog.cryptoasm.mips_bipl]
store.get_multu_op [in seplog.cryptoasm.mips_bipl]
store.get_r0 [in seplog.cryptoasm.mips_bipl]
store.get_upd' [in seplog.cryptoasm.mips_bipl]
store.get_upd_p' [in seplog.cryptoasm.mips_bipl]
store.get_upd [in seplog.cryptoasm.mips_bipl]
store.get_upd_p [in seplog.cryptoasm.mips_bipl]
store.hi_mflhxu_op [in seplog.cryptoasm.mips_bipl]
store.hi_zero [in seplog.cryptoasm.mips_bipl]
store.hi_mtlo_op [in seplog.cryptoasm.mips_bipl]
store.hi_mthi_op [in seplog.cryptoasm.mips_bipl]
store.hi_upd [in seplog.cryptoasm.mips_bipl]
store.lo_mflhxu_op [in seplog.cryptoasm.mips_bipl]
store.lo_remainder [in seplog.cryptoasm.mips_bipl]
store.lo_remainder' [in seplog.cryptoasm.mips_bipl]
store.lo_mtlo_op [in seplog.cryptoasm.mips_bipl]
store.lo_mthi_op [in seplog.cryptoasm.mips_bipl]
store.lo_upd [in seplog.cryptoasm.mips_bipl]
store.maddu_upd [in seplog.cryptoasm.mips_bipl]
store.mflhxu_kbeta1_utoZ [in seplog.cryptoasm.mips_bipl]
store.mflhxu_beta2_utoZ [in seplog.cryptoasm.mips_bipl]
store.mflhxu_utoZ [in seplog.cryptoasm.mips_bipl]
store.mflhxu_upd [in seplog.cryptoasm.mips_bipl]
store.msubu_utoZ_overflow [in seplog.cryptoasm.mips_bipl]
store.msubu_utoZ [in seplog.cryptoasm.mips_bipl]
store.multi_null_lo [in seplog.cryptoasm.mips_bipl]
store.multi_null_upd [in seplog.cryptoasm.mips_bipl]
store.multi_null_utoZ [in seplog.cryptoasm.mips_bipl]
Store.upd_upd_eq [in seplog.seplog.bipl]
Store.upd_upd [in seplog.seplog.bipl]
store.upd_r0 [in seplog.cryptoasm.mips_bipl]
store.upd_upd_eq [in seplog.cryptoasm.mips_bipl]
store.upd_upd_p [in seplog.cryptoasm.mips_bipl]
store.utoZ_multu [in seplog.cryptoasm.mips_bipl]
store.utoZ_maddu [in seplog.cryptoasm.mips_bipl]
store.utoZ_multi_null [in seplog.cryptoasm.mips_bipl]
store.utoZ_lo_beta1 [in seplog.cryptoasm.mips_bipl]
store.utoZ_acx_beta2 [in seplog.cryptoasm.mips_bipl]
store.utoZ_pos [in seplog.cryptoasm.mips_bipl]
store.utoZ_upd [in seplog.cryptoasm.mips_bipl]
store.utoZ_def [in seplog.cryptoasm.mips_bipl]
StringOrder.ltA_irr [in seplog.lib.order]
StringOrder.ltA_total [in seplog.lib.order]
StringOrder.ltA_trans [in seplog.lib.order]
string_decxx [in seplog.lib.String_ext]
string2asciis_inj [in seplog.lib.String_ext]
styp_frec_ind [in seplog.seplogC.C_types_fp]
styp_frec0_ext [in seplog.seplogC.C_types_fp]
subset_undup [in seplog.lib.seq_ext]
subset_cat [in seplog.lib.seq_ext]
subset_nil [in seplog.lib.seq_ext]
substitution_uniq [in seplog.lib.uniq_tac]
substitution_Permutation [in seplog.lib.seq_ext]
subst_Assert2store_update [in seplog.seplog.frag_list_triple]
subst_Sigma2store_update' [in seplog.seplog.frag_list_triple]
subst_Sigma2store_update [in seplog.seplog.frag_list_triple]
subst_bexp_store_upd [in seplog.seplogC.C_expr]
subst_exp_store_upd [in seplog.seplogC.C_expr]
subst_Sigma2store_update' [in seplog.seplog.frag]
subst_Sigma2store_update [in seplog.seplog.frag]
subZKC [in seplog.lib.ssrZ]
sub_reg [in seplog.lib.machine_int]
sub_substitution [in seplog.lib.seq_ext]
SumOfFirstNaturals.prf [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_1 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_2 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_3 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_4 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_5 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_6 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_7 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_8 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_9 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_10 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_11 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_12 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_13 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_14 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_15 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_16 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_17 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_18 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_19 [in seplog.cryptoasm.sgoto_hoare_example]
SumOfFirstNaturals.step_20 [in seplog.cryptoasm.sgoto_hoare_example]
sum_Z_pos_pos [in seplog.lib.littleop]
Sum_sem_conv [in seplog.lib.littleop]
Sum_distrib [in seplog.lib.littleop]
Sum_rearrangement [in seplog.lib.littleop]
Sum_perm_eq [in seplog.lib.littleop]
Sum_op [in seplog.lib.littleop]
Sum_cat [in seplog.lib.littleop]
Sum_cons [in seplog.lib.littleop]
Sum_eq4 [in seplog.lib.littleop]
Sum_eq3 [in seplog.lib.littleop]
Sum_eq2 [in seplog.lib.littleop]
Sum_eq1 [in seplog.lib.littleop]
Sum_hole_shift [in seplog.lib.multi_int]
Sum_hole_upd_nth [in seplog.lib.multi_int]
Sum_hole_last' [in seplog.lib.multi_int]
Sum_hole_last [in seplog.lib.multi_int]
sum_k_S [in seplog.lib.multi_int]
sum_k_0 [in seplog.lib.multi_int]
sum_k_nil [in seplog.lib.multi_int]
swap_correct [in seplog.seplogC.C_swap]
swap_verif' [in seplog.seplog.frag_list_swap]
swap_verif_step_by_step [in seplog.seplog.frag_list_swap]
swap_verif [in seplog.seplog.frag_list_swap]
swap_verif' [in seplog.seplog.LSF_LWP_comparation]
swap_verif [in seplog.seplog.LSF_LWP_comparation]
Swap.swap [in seplog.seplog.examples]
Swap.vc_swap [in seplog.seplog.examples]
Syntax.exec_deter [in seplog.seplog.syntax]
Syntax.exec0_proj [in seplog.seplog.syntax]
Syntax.exec0_deter [in seplog.seplog.syntax]
Syntax.In_cmd_vars [in seplog.seplog.syntax]
Syntax.no_malloc_heap_invariant [in seplog.seplog.syntax]
Syntax.no_malloc_heap_invariant0 [in seplog.seplog.syntax]
Syntax.var_unchanged [in seplog.seplog.syntax]
Syntax.var_unchanged' [in seplog.seplog.syntax]
Syntax.var_unchanged0' [in seplog.seplog.syntax]
S_Zabs_nat [in seplog.lib.ZArith_ext]
s2Z_ge_s_cst_e [in seplog.seplogC.C_expr_ground]
s2Z_Z2u' [in seplog.seplogC.C_pp]
s2Z_Z2u [in seplog.seplogC.C_pp]
s2Z_sumop [in seplog.lib.littleop]
s2Z_si32_of_phy_safe_cast [in seplog.seplogC.C_expr]
s2Z_sc [in seplog.seplogC.C_expr]
s2Z_add_new [in seplog.lib.machine_int]


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (39074 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (477 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (30413 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (242 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (554 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (249 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3616 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (570 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (583 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (102 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (68 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (114 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (45 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (5 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2012 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (24 entries)