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)

other

_ |=> _ (assoc_scope) [notation, in seplog.begcd.simu]
_ \U+ _ (assoc_scope) [notation, in seplog.begcd.simu]
|_ _ , _ _| (core_scope) [notation, in seplog.lib.Init_ext]
|_ _ _| (core_scope) [notation, in seplog.lib.Init_ext]
[ _ ]gb (C_expr_scope) [notation, in seplog.seplogC.C_expr_ground]
[ _ ]gb (C_expr_scope) [notation, in seplog.seplogC.C_expr_ground]
[ _ ]ge (C_expr_scope) [notation, in seplog.seplogC.C_expr_ground]
[ _ ]ge (C_expr_scope) [notation, in seplog.seplogC.C_expr_ground]
:* _ (C_types_scope) [notation, in seplog.seplogC.C_types]
_ .-ityp: _ (C_types_scope) [notation, in seplog.seplogC.C_types]
ityp: _ (C_types_scope) [notation, in seplog.seplogC.C_types]
_ .-env (C_types_scope) [notation, in seplog.seplogC.C_types]
_ .-typ (C_types_scope) [notation, in seplog.seplogC.C_types]
_ .-typ: _ (C_types_scope) [notation, in seplog.seplogC.C_types]
\wfctxt{ _ \} (C_types_scope) [notation, in seplog.seplogC.C_types]
\O (C_types_scope) [notation, in seplog.seplogC.C_types]
_ |> _ \, _ (C_types_scope) [notation, in seplog.seplogC.C_types]
_ =t= _ (C_types_scope) [notation, in seplog.seplogC.C_types]
\b _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
\~b _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
[ _ ]b_ _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ |pe~> _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ |le~> _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
(phyint) _ (C_value_scope) [notation, in seplog.seplogC.C_expr]
(UINT) _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
{; _ ;} _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
(int) _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
[; _ ;] _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \? _ \: _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ &-> _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \|| _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \&& _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \>= _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \> _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \<= _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \< _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \!= _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \% _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \<< _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \* _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \- _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \| _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \& _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \= _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ \+ _ (C_expr_scope) [notation, in seplog.seplogC.C_expr]
[ _ ]uc (C_expr_scope) [notation, in seplog.seplogC.C_expr]
[ _ ]sc (C_expr_scope) [notation, in seplog.seplogC.C_expr]
[ _ ]pc (C_expr_scope) [notation, in seplog.seplogC.C_expr]
[ _ ]c (C_expr_scope) [notation, in seplog.seplogC.C_expr]
_ =b _ (C_expr_scope) [notation, in seplog.seplogC.C_expr_equiv]
_ =s _ (C_expr_scope) [notation, in seplog.seplogC.C_expr_equiv]
_ |x| _ (C_value_scope) [notation, in seplog.seplogC.C_value]
phy<=log (C_value_scope) [notation, in seplog.seplogC.C_value]
_ |pV~> _ (C_value_scope) [notation, in seplog.seplogC.C_value]
_ |pZ~> _ (C_value_scope) [notation, in seplog.seplogC.C_value]
_ .-log (C_value_scope) [notation, in seplog.seplogC.C_value]
[ _ ]u (C_value_scope) [notation, in seplog.seplogC.C_value]
[ _ ]s (C_value_scope) [notation, in seplog.seplogC.C_value]
[ _ ]p (C_value_scope) [notation, in seplog.seplogC.C_value]
phy<=ptr (C_value_scope) [notation, in seplog.seplogC.C_value]
phy<=i64 (C_value_scope) [notation, in seplog.seplogC.C_value]
phy<=si32 (C_value_scope) [notation, in seplog.seplogC.C_value]
phy<=ui32 (C_value_scope) [notation, in seplog.seplogC.C_value]
phy<=si8 (C_value_scope) [notation, in seplog.seplogC.C_value]
phy<=ui8 (C_value_scope) [notation, in seplog.seplogC.C_value]
ptr<=phy (C_value_scope) [notation, in seplog.seplogC.C_value]
i64<=phy (C_value_scope) [notation, in seplog.seplogC.C_value]
i8<=phy (C_value_scope) [notation, in seplog.seplogC.C_value]
si32<=phy (C_value_scope) [notation, in seplog.seplogC.C_value]
ui32<=phy (C_value_scope) [notation, in seplog.seplogC.C_value]
_ .-phy (C_value_scope) [notation, in seplog.seplogC.C_value]
i64<=i8 (C_value_scope) [notation, in seplog.seplogC.C_value]
oi64<=i8 (C_value_scope) [notation, in seplog.seplogC.C_value]
i8<=i64 (C_value_scope) [notation, in seplog.seplogC.C_value]
ptr<=i8 (C_value_scope) [notation, in seplog.seplogC.C_value]
i16<=i8 (C_value_scope) [notation, in seplog.seplogC.C_value]
i32<=i8 (C_value_scope) [notation, in seplog.seplogC.C_value]
oi32<=i8 (C_value_scope) [notation, in seplog.seplogC.C_value]
i8<=i32 (C_value_scope) [notation, in seplog.seplogC.C_value]
optr<=i8 (C_value_scope) [notation, in seplog.seplogC.C_value]
i8<=ptr (C_value_scope) [notation, in seplog.seplogC.C_value]
_ |-- _ (entail_scope) [notation, in seplog.seplog.frag_list_entail]
_ \** _ (entail_scope) [notation, in seplog.seplog.frag_list_entail]
_ =m _ {{ _ }} (eqmod_scope) [notation, in seplog.lib.ZArith_ext]
{{{ _ }}} _ {{{ _ }}} (frag_list_scope) [notation, in seplog.seplog.frag_list_entail]
ifte _ thendo _ elsedo _ (frag_list_vc_scope) [notation, in seplog.seplog.frag_list_vcg]
_ ; _ (frag_list_vc_scope) [notation, in seplog.seplog.frag_list_vcg]
_ <-malloc _ (frag_list_vc_scope) [notation, in seplog.seplog.frag_list_vcg]
_ *<- _ (frag_list_vc_scope) [notation, in seplog.seplog.frag_list_vcg]
_ <-* _ (frag_list_vc_scope) [notation, in seplog.seplog.frag_list_vcg]
_ <- _ (frag_list_vc_scope) [notation, in seplog.seplog.frag_list_vcg]
_ \d\ _ (heap_scope) [notation, in seplog.cryptoasm.mips_bipl]
_ \D\ _ (heap_scope) [notation, in seplog.cryptoasm.mips_bipl]
_ \U _ (heap_scope) [notation, in seplog.cryptoasm.mips_bipl]
_ # _ (heap_scope) [notation, in seplog.cryptoasm.mips_bipl]
_ |P| _ (heap_scope) [notation, in seplog.begcd.simu]
_ \D\ _ (heap_scope) [notation, in seplog.begcd.simu]
_ # _ (heap_scope) [notation, in seplog.begcd.simu]
_ \U _ (heap_scope) [notation, in seplog.begcd.simu]
_ \d\ _ (heap_scope) [notation, in seplog.begcd.simu]
_ |P| _ (heap_scope) [notation, in seplog.seplogC.C_value]
_ \D\ _ (heap_scope) [notation, in seplog.seplogC.C_value]
_ # _ (heap_scope) [notation, in seplog.seplogC.C_value]
_ \U _ (heap_scope) [notation, in seplog.seplogC.C_value]
_ \d\ _ (heap_scope) [notation, in seplog.seplogC.C_value]
_ `32_ _ (machine_int_scope) [notation, in seplog.lib.machine_int]
_ `_ _ (machine_int_scope) [notation, in seplog.lib.machine_int]
u32<=Z (machine_int_scope) [notation, in seplog.lib.machine_int]
Z<=s (machine_int_scope) [notation, in seplog.lib.machine_int]
nat<=s (machine_int_scope) [notation, in seplog.lib.machine_int]
Z<=u (machine_int_scope) [notation, in seplog.lib.machine_int]
nat<=u (machine_int_scope) [notation, in seplog.lib.machine_int]
_ -- _ ---> _ (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
While _ {{ _ }} (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
If_bgez _ Then _ Else _ (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
If_bgtz _ Then _ Else _ (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
If_blez _ Then _ Else _ (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
If_bltz _ Then _ Else _ (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
If_bne _ , _ Then _ Else _ (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
If_beq _ , _ Then _ Else _ (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
If _ Then _ Else _ (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
_ ; _ (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
_ -- _ ----> _ (mips_cmd_scope) [notation, in seplog.cryptoasm.mips_cmd]
{{{ _ }}} _ {{{ _ }}} (mips_hoare_scope) [notation, in seplog.cryptoasm.mips_seplog]
{{ _ }} _ {{ _ }} (mips_hoare_scope) [notation, in seplog.cryptoasm.mips_seplog]
wp_semantics (mips_hoare_scope) [notation, in seplog.cryptoasm.mips_seplog]
hoare_semantics (mips_hoare_scope) [notation, in seplog.cryptoasm.mips_seplog]
hoare_semantics_total (mips_hoare_scope) [notation, in seplog.cryptoasm.mips_seplog]
{{[ _ ]}} _ {{[ _ ]}} (mips_hoare_scope) [notation, in seplog.cryptoasm.mips_seplog]
_assert (mips_hoare_scope) [notation, in seplog.cryptoasm.mips_seplog]
_ -- _ ---> _ (mips_cmd_scope) [notation, in seplog.begcd.multi_sub_s_u_simu]
_ -- _ ---> _ (mips_cmd_scope) [notation, in seplog.begcd.multi_sub_s_u_simu]
_ -- _ ---> _ (mips_cmd_scope) [notation, in seplog.begcd.multi_sub_s_s_simu]
hoare_semantics (mips_hoare_scope) [notation, in seplog.begcd.multi_sub_s_s_simu]
_ -- _ ---> _ (mips_cmd_scope) [notation, in seplog.begcd.multi_sub_s_s_simu]
hoare_semantics (mips_hoare_scope) [notation, in seplog.begcd.multi_sub_s_s_simu]
\S_{ _ } _ (multi_int_scope) [notation, in seplog.lib.multi_int]
_ ^ _ (nat_scope) [notation, in seplog.cryptoasm.bbs_triple]
_ ^ _ (nat_scope) [notation, in seplog.lib.ZArith_ext]
sha1_update( _ , _ , _ ) (POLAR_scope) [notation, in seplog.seplogC.POLAR_library_functions]
md5_update( _ , _ , _ ) (POLAR_scope) [notation, in seplog.seplogC.POLAR_library_functions]
_ <-memset( _ , _ , _ ) (POLAR_scope) [notation, in seplog.seplogC.POLAR_library_functions]
_ <-memcpy( _ , _ , _ ) (POLAR_scope) [notation, in seplog.seplogC.POLAR_library_functions]
_ <-ssl_fetch_input( _ , _ ) (POLAR_scope) [notation, in seplog.seplogC.POLAR_library_functions]
\0x _ (rfc5246_scope) [notation, in seplog.seplogC.rfc5246]
Zmax( _ , _ ) (rfc5246_scope) [notation, in seplog.seplogC.rfc5246]
_ |{ _ , _ ) (seq_ext_scope) [notation, in seplog.lib.seq_ext]
_ <=( _ , _ ) _ (simu_scope) [notation, in seplog.begcd.simu]
uniq( _ , .. , _ ) (uniq_scope) [notation, in seplog.lib.uniq_tac]
divZ (zarith_ext_scope) [notation, in seplog.lib.ssrZ]
sgZ (zarith_ext_scope) [notation, in seplog.lib.ssrZ]
gcdZ (zarith_ext_scope) [notation, in seplog.lib.ssrZ]
'| _ | (zarith_ext_scope) [notation, in seplog.lib.ssrZ]
Z<=nat (zarith_ext_scope) [notation, in seplog.lib.ssrZ]
`| _ | (zarith_ext_scope) [notation, in seplog.lib.ssrZ]
\B^ _ (zarith_ext_scope) [notation, in seplog.lib.ZArith_ext]
_ ^^ _ (zarith_ext_scope) [notation, in seplog.lib.ZArith_ext]
_ |~> _ [notation, in seplog.seplogC.C_swap]
_ |P| _ [notation, in seplog.begcd.simu]
_ \d\ _ [notation, in seplog.begcd.simu]
_ \D\ _ [notation, in seplog.begcd.simu]
_ \U _ [notation, in seplog.begcd.simu]
_ # _ [notation, in seplog.begcd.simu]
dom _ [notation, in seplog.begcd.simu]
[ _ ]_ _ [notation, in seplog.seplogC.C_expr]



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)