| 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 | (1518 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 | (358 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 | (71 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 | (460 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 | (39 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 | (1 entry) |
| 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 | (21 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 | (53 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 | (21 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 | (494 entries) |
Global Index
A
Ack [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]Ackgen [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
ackgen [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Ackgen_4 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Ackgen_n [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Ackgen_Behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
Ackor [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
Ackor_true_RequestsToArbitrate [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
Ackor_4 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Ackor_n [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Ackor_false [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Ackor_ltReq_false [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Ackor_dmap_false_4 [lemma, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_dmap_true_4 [lemma, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_dmap_false_2 [lemma, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_dmap_true_2 [lemma, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_false_fth [lemma, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_false_thd [lemma, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_false_scd [lemma, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_false_fst [lemma, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ack_Behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
Ack_behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
ack_behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
active_bits [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
ACTIVE_A [constructor, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
act_bits [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
Additional_Def_and_Lemmas.eq_dec [variable, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Additional_Def_and_Lemmas.A [variable, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Additional_Def_and_Lemmas [section, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
all_True [definition, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
all_False [definition, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
all_same [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
All_Thd_of_l3 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
All_Scd_of_l3 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
All_Fst_of_l3 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
All_Ports [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
andb_negb_true_l [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_negb_true_r [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_true_r [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_true_l [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_true [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_false [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_sym [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
ANDL [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
ANDL3 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
ANDL4 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
and_sym [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
AND2 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
AND3 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
AND4 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
AO [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
ARBITER_XY_Behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp_Behaviour]
Arbiter_last [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Arbiter_last_ff [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Arbiter_last_ft [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Arbiter_last_tf [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Arbiter_last_tt [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Arbiter_Y_behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
Arbiter_X_behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
Arbiter4_Specif [library]
Arbiter4_Proof_lemmas [library]
Arbiter4_Proof [library]
Arbitration [library]
Arbitration_Structure.Input_vector_type [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Arbitration_Structure [section, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Arbitration_Structure.Input_vector_type [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Arbitration_Structure [section, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Arbitration_Correctness.p_0 [variable, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.o_a4_0 [variable, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.g22_0 [variable, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.g21_0 [variable, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.g12_0 [variable, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.g11_0 [variable, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.Input_type [variable, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness [section, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_between_several_inputs.requests [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
Arbitration_between_several_inputs.Inportno [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
Arbitration_between_several_inputs [section, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
Arbitration_Specification.Output_type [variable, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Arbitration_Specification.Input_type [variable, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Arbitration_Specification [section, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Arbitration_beh.Input_type [variable, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Arbitration_beh [section, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Arbitration_Proof [library]
Arbitration_Specif [library]
Arbitration_beh_sc [library]
Arbx [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Arby [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Arb_xel [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Arb_yel [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Arith_Compl [library]
At_least_one_of_2_active [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
AT_LEAST_ONE_IS_ACTIVE_a4 [constructor, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
A_Moore [lemma, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
a_Mealy [lemma, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
A1A2 [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
A1A2 [abbreviation, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
B
Base_Struct [library]Base_Behaviour [library]
Basic_composition_rules [library]
BehaviourSC_ARBITRATION [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Behaviour_FOUR_ARBITERS [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Behaviour_TIMING [definition, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Behaviour_PRIORITY_DECODE [definition, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Behaviour_IDENTITY [definition, in Fairisle.Libraries.Lib_Automata.Identity]
Behaviour_ARBITRATION [definition, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Behaviour_TIMINGPDECODE_ID [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Behaviour_TIMING_PDECODE [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Behaviour_Struct_lemmas [library]
bool_dec [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
bool_to_nat [definition, in Fairisle.Libraries.Lib_Lists.Conversions]
bool_nat [definition, in Fairisle.Libraries.Lib_Lists.Conversions]
Bool_Compl [library]
C
Compact [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]Compact_PC_id [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Compact_dlist [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Compare_Nat [library]
comparison [definition, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comparisonE [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comparisonG [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comparisonL [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comp_sym_E [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comp_sym_GL [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comp_sym_LG [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
construct_with_i_last [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
construct_with_i_first [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Conversions [library]
Convert_list2_port [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Convert_port_list2_ter [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Convert_port_list2_bis [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Convert_port_list2 [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Convert_and_filter [definition, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Convert_list2_nat [definition, in Fairisle.Libraries.Lib_Lists.Conversions]
Convert_list2 [definition, in Fairisle.Libraries.Lib_Lists.Conversions]
Correct_TIMING [lemma, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Correct_ARBITRATION [lemma, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Correct_PRIORITY_DECODE [lemma, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Correct_FOUR_ARBITERS [lemma, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Correct_ARBITRATION_end [lemma, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Cst_True_inv_t [lemma, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Cst_True_inv_pdecode [lemma, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
C_Inv [constructor, in Fairisle.Libraries.Lib_Automata.Mealy]
C_Inp [abbreviation, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
C_Inv_t [constructor, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
D
DATASWITCHC [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]DATASWITCHC_AUX [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
DATASWITCH_N [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
DATASWITCH_N_AUX [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Decode [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Decode_4 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Decode_n [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
DECODE_p [constructor, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Definitions_and_lemmas_about_ports.Outportno [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Definitions_and_lemmas_about_ports.Inportno [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Definitions_and_lemmas_about_ports.o [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Definitions_and_lemmas_about_ports.i [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Definitions_and_lemmas_about_ports [section, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Dependent_lists.A [variable, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
Dependent_lists [section, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
Dependent_lists [library]
Dependent_lists_Compl [library]
Derived_composition_rules [library]
DFFd [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
DFFRD [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
DFFrd [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
dif_0_pred_eq_0_eq_1 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
div [definition, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
div_minus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
div_plus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
div_odd_odd [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
div_odd_even [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
dlist_to_Stream [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
dlist_List [definition, in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
dlist_Compl [library]
dmap_Stream_to_dlist [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
dmap_dlist_to_Stream [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
DMUX2B4CA11 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
DMUX2B4CA11_AUX [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
DMUX4T2 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Dmux4t2 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
DMUX4T2FFC [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
dmux4t2ffc [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
DMUX4T2FFC_Behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp_Behaviour]
DMUX4T2FFC_AUX [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Dmux4t2ffc_Behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
Dmux4t2ffc_Behaviour' [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
d_In_SUCSUCSUC_SSSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUCSUCSUC_SO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUCSUC_SSSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC_SSSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUCSUCSUC_SSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUCSUC_SSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC_SSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUCSUC1_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC1_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC2_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC1_l3 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC0_l2 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In [definition, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
d_map4 [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_map3 [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_map2 [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_map [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_Hd [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_tl [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_Head [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_head [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_hd [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_cons [constructor, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_nil [constructor, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_list [inductive, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_Map_List2_pdt_Grant [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
d_Map_List4_pdt_Grant [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof_lemmas]
d_Lists_Compl.d_List [variable, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
d_Lists_Compl.C [variable, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
d_Lists_Compl.B [variable, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
d_Lists_Compl.A [variable, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
d_Lists_Compl [section, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
E
E [constructor, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]eight [abbreviation, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
ElementComb [library]
ElementComb_Behaviour [library]
ElementTemp [library]
ElementTemp_Behaviour [library]
empty [lemma, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
empty_dep [lemma, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
eqp1 [lemma, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
eqp2 [lemma, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
eqp3 [lemma, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
eqp4 [lemma, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
eqp5 [lemma, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
eqS [constructor, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS [inductive, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_Compact [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_S_Snd_of_3 [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_S_Thd_of_3 [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_sym [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_reflex [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_trans [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_Moore [lemma, in Fairisle.Libraries.Lib_Automata.Moore]
eqS_about_P [lemma, in Fairisle.Libraries.Lib_Automata.Mealy]
EqS_States_Mealy [lemma, in Fairisle.Libraries.Lib_Automata.Mealy]
EqS_Mealy [lemma, in Fairisle.Libraries.Lib_Automata.Mealy]
eqS_Inv_P_Timing [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
EqS_transf [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
EqS_Snd_SC_TIMING [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
EqS_IDENTITY [lemma, in Fairisle.Libraries.Lib_Automata.Identity]
EqS_S_Fth_of_l4 [lemma, in Fairisle.Libraries.Lib_Lists.Proj_lists]
EqS_S_Thd_of_l4 [lemma, in Fairisle.Libraries.Lib_Lists.Proj_lists]
EqS_S_Scd_of_l4 [lemma, in Fairisle.Libraries.Lib_Lists.Proj_lists]
EqS_S_Fst_of_l4 [lemma, in Fairisle.Libraries.Lib_Lists.Proj_lists]
EqS_const_stream [lemma, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_2_Mealy.R [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.P_is_true [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.P [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.States_A2 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.States_A1 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.A2 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.A1 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Out2 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Out1 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Trans2 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Trans1 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.State_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.State_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy [section, in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_Mealy_to_Moore2.Out_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.Trans_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.State_type_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.A_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.Out_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.Trans_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.State_type_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2 [section, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Out_Mealy2 [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Trans_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.A_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Out_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Trans_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.State_type [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2 [section, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.A_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Out_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Trans_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.State_type_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.A_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Out_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Trans_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.State_type_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1 [section, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.A_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.Trans_Mealy [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.A_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.Out_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.Trans_Moore [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.state_type [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1 [section, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equiv_States_PC [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
equiv_SC' [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
equiv_SC [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.B2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.B1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.A2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.A1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Outb2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Outb1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Transb2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Transb1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Outa2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Outa1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Transa2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Transa1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.State_type_b2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.State_type_b1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.State_type_a2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.State_type_a1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Output_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Output_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC [section, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
equiv_PC [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.output [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.f [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.B2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.B1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.A2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.A1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Outb2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Outb1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Transb2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Transb1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Outa2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Outa1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Transa2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Transa1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.State_type_b2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.State_type_b1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.State_type_a2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.State_type_a1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Output_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Output_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Input_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Input_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC [section, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_S1S1_PC_part [lemma, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Equiv_Four_Arbiters_Moore_Mealy [lemma, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
equiv_out_Four_Arbiters_Moore_Mealy [lemma, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Equiv_2_Mealy_tool [lemma, in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_about_P.P [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_about_P.State_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_about_P.State_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_about_P.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_about_P [section, in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_2_Mealy [lemma, in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_A1A2_FC [lemma, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Equiv_A1A2_SC [lemma, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Equiv_States_A1A2_PC [lemma, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Equiv_A1A2_PC [lemma, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Equiv_Timing_Moore_Mealy [lemma, in Fairisle.Fairisle.PROOFS.Timing_Proof]
equiv_out_Timing [lemma, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Equiv_Behaviour_TIMINGPDECODE_ID [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Equiv_PriorityDecode_Moore_Mealy [lemma, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
equiv_out_PriorityDecode [lemma, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Equiv_Arbitration_Moore_Mealy [lemma, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
equiv_out_Arbitration_Moore_Mealy [lemma, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Equiv_Mealy_Moore [lemma, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equiv_Moore_Mealy [lemma, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equiv_Struct_Beh_Arbitration [lemma, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Equiv_a4 [lemma, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Equiv_tpi [lemma, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Equiv_Struct_Beh_Arbitration [library]
equiv1 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
equiv2 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
eq_n_SM4_4_times [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
eq_d_list [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
eq_dlist_of_Stream [inductive, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
eq_Square_exp_n [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
eq_pred [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
eq_minus_plus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
eq_or_not_bis [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Dec]
eq_fs_and_RouteE_false [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
eq_exp_2_exp_n [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
eq_dlist_Head [lemma, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Eq_dlist_to_Stream_List4 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
eq_List4_map [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
eq_pair [lemma, in Fairisle.Libraries.Lib_Basis.Product]
eq4_LS1 [constructor, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
eq4_LSO [constructor, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Even [inductive, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
even [inductive, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
Even_or_Odd [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
Even_intro [constructor, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
even_odd [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
even_or_odd [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
even_intro [constructor, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
Exist [abbreviation, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
exists1_exact [definition, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
exists1_atleast [definition, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
Exists1_atleast_or_not [lemma, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
Exists1_atleast [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
exp_n_pos [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n_plus_p1 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n_permut [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n_plus_mult [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n_neutre [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n_incr [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_n_plus_m [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_incr [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_pos [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_le_pn_n [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_plus_pn_pn [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_n_plus_n [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n [definition, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2 [definition, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
Ex_n_lt_gen [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
F
factorial [definition, in Fairisle.Libraries.Lib_Arithmetic.Lib_Fact]fact_pred [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Fact]
false_andb_true [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
false_neg_true [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
false_andb_b [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
false_orb_r [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
false_orb_l [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
FC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.upd_s2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.upd_s1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.out [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.input [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.A2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.A1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Out2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Out1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Trans2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Trans1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.State_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.State_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Output_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Input_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition [section, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Filter_and_Pick.and3 [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.and2 [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.eq_true [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.d_map_andb [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.requests [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.priorities [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.actives [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.Inportno [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick [section, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
First [constructor, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
first_of_list [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
five [abbreviation, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
fixed_lists.A [variable, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
fixed_lists [section, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Fixed_dLists [library]
Fold_List [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
fold_with_f [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Fold_with_f_S [definition, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Fold_with_f_S_p [definition, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Fold_with_f [definition, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
For_ltReq.H8 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H7 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H6 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H5 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H4 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H3 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H2 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H1 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.o22 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.o21 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.o12 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.o11 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.g22 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.g21 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.g12 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.g11 [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.o [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.g [variable, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq [section, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
four [abbreviation, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
Four_Arbiters_Specif.Reg_type [variable, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Four_Arbiters_Specif.Output_type [variable, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Four_Arbiters_Specif.Input_type [variable, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Four_Arbiters_Specif [section, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Four_Arbiters_Proof_Correctness.g22_0 [variable, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness.g21_0 [variable, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness.g12_0 [variable, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness.g11_0 [variable, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness.Reg_type [variable, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness.Input_type [variable, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness [section, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Freg [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Freg2 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
From_init_states.p_0 [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.g22_0 [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.g21_0 [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.g12_0 [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.g11_0 [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.fs_act_signals [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.fs_0 [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.Route [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.Pri [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.Act [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.Fs [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.i [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.Input_type [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states [section, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Fst_Compact [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Fst_3 [abbreviation, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
fst_3 [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
fst_list2 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Fst_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Fst_of_l3 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Fst_of_l2 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Fth_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
f_four_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
f_two_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
f_arbiter [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
f_four_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
f_two_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
f_arbiter [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
f_tp [definition, in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
f_tpi [definition, in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
G
G [constructor, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]Gates [library]
Gates_Del [library]
genReq [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Genreq [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Gen_Gates_Del [library]
Grant [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
grant [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
Grant_for_Out [definition, in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Grant' [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
grant' [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
H
hds [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]hiReq [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Hireq [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
I
IBUF [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]IDENTITY [constructor, in Fairisle.Libraries.Lib_Automata.Identity]
Identity [section, in Fairisle.Libraries.Lib_Automata.Identity]
Identity [library]
Identity_and_TimingPDecode.output_tpi [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Identity_and_TimingPDecode.f_tpi [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Identity_and_TimingPDecode.Input_vector_type [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Identity_and_TimingPDecode [section, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Identity_and_TimingPDecode.output_tpi [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Identity_and_TimingPDecode.f_tpi [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Identity_and_TimingPDecode.Input_vector_type [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Identity_and_TimingPDecode [section, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Identity_and_TimingPDecode_beh.output_tpi [variable, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Identity_and_TimingPDecode_beh.f_tpi [variable, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Identity_and_TimingPDecode_beh.Input_type [variable, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Identity_and_TimingPDecode_beh [section, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Identity.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Identity]
id_list' [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
id_list3_thd [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
id_list3_scd [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
id_list3_fst [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
id_list3 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
id_list [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
If [abbreviation, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
ifProp [definition, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
ifProp_or [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
if_bool [definition, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
Ilatch [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
ILATCH [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
impl_no_no [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
INFFd [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
Infinite_List.B [variable, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Infinite_List.A [variable, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Infinite_List [section, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Infinite_lists [library]
Injections [library]
Inj1 [definition, in Fairisle.Libraries.Lib_Basis.Injections]
Inj2 [definition, in Fairisle.Libraries.Lib_Basis.Injections]
Inv [inductive, in Fairisle.Libraries.Lib_Automata.Mealy]
INV [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
Invariant_relation_t [lemma, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Invariant_relation_A [lemma, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Invariant_Init_states_A [lemma, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Invariant_a4_SSS [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
Invariant_relation_p [axiom, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Invariant_relation_a4 [lemma, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Invariant_Init_states_a4 [lemma, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Invariant_a4_S [library]
Inv_under_P [definition, in Fairisle.Libraries.Lib_Automata.Mealy]
Inv_Ok [lemma, in Fairisle.Libraries.Lib_Automata.Mealy]
inv_comparison [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
inv_comparisonG [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
inv_comparisonE [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
inv_comparisonL [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
Inv_a4' [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Inv_a4 [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Inv_t_a4_Ok [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Inv_Init_states_t_a4 [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Inv_t_a4 [definition, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Inv_P_Timing [inductive, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Inv_P_Timing_Inv_A [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
In_latch [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
In_Buf [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
IN_LATCH [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
IN_BUF [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
In_or_not [lemma, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Is_Inv_P_Timing [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
I' [constructor, in Fairisle.Libraries.Lib_Automata.Mealy]
J
Jk [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]JkE [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
JKFFce [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
JKFF_qBar [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
JKFF_q [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
J_Arby [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
K
K_Arby [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]L
L [constructor, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]label_a4 [inductive, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
label_t [inductive, in Fairisle.Fairisle.PROOFS.Timing_Proof]
label_p [inductive, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
label_A [inductive, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
last_of_list [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Latch [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
LATCH [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
Lemmas_Struct [library]
Lemmas_on_fcts [library]
Lemmas_on_Basic_rules [library]
Lemmas_Comb_Behaviour [library]
Lemmas_for_Arbitration [library]
less_or_eq [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
less_div [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
le_number_P [lemma, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
le_8_8 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_7_8 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_7_7 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_6_8 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_5_8 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_5_7 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_5_6 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_4_8 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_4_4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_3_7 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_3_4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_3_3 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_2_4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_2_3 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_1_7 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_1_4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_1_3 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_1_2 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_n_Square [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
le_mult_r [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
le_mult_l [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
le_lt_plus_mult [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
le_mult_csts [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
le_mult_cst [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
le_reg_minus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
le_minus_n_Sn [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
le_minus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
le_exp_n_mult [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
le_SSS_bool_nat [lemma, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
le_S_bool_nat [lemma, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
le_transp_r [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
le_transp_l [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
le_lt_plus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
le_le_assoc_plus_minus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
le_minus_plus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
le_minusSS [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_n_mult_S_n [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_mult_l [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_Sn_le_n_pred [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_S_lt_O [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_leS [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_le_Sminus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_minusS [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le8_le6 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le8_lt7 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
Lib_Set_Products [library]
Lib_Plus [library]
Lib_Pred [library]
Lib_Minus [library]
Lib_Zerob [library]
Lib_Exp [library]
Lib_Square [library]
Lib_Eq_Le_Lt [library]
Lib_Prop [library]
Lib_Bool [library]
Lib_Fact [library]
Lib_Dec [library]
Lib_Mult [library]
Lib_Div_Even_Odd [library]
Lists_of_lists [library]
list_of_seg [definition, in Fairisle.Libraries.Lib_Lists.Lists_of_lists]
list_of_nth [definition, in Fairisle.Libraries.Lib_Lists.Lists_of_lists]
list_of_tails [definition, in Fairisle.Libraries.Lib_Lists.Lists_of_lists]
list_of_heads [definition, in Fairisle.Libraries.Lib_Lists.Lists_of_lists]
list_no_port_bool [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
list_of_segment [definition, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
List_of_scd_of_l2 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
List_of_tails_of_l2 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
List_of_fst_of_l2 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
List_dlist_cons [lemma, in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
list_dlist [definition, in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
List_dlist [definition, in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
List2 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List2Bool_dec [lemma, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
List2_pdt [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List2_access [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List3 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List4 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List4_transf [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List4_map [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List4_of_pdt [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Loop [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Loop2 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Loop3 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Loop3_permut [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
ltReq_false_G4 [lemma, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof_lemmas]
ltReq_false_G3 [lemma, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof_lemmas]
ltReq_false_G2 [lemma, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof_lemmas]
ltReq_false_G1 [lemma, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof_lemmas]
ltReq_1111 [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_111O [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_11O1 [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_11OO [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_1O11 [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_1O1O [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_1OO1 [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_1OOO [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_O111 [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_O11O [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_O1O1 [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_O1OO [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_OO11 [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_OO1O [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_OOO1 [lemma, in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
lt_4_4cases [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
lt_8_S8 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_7_S8 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_3_S3 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_2_S3 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_1_S3 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_3_4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_2_4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_1_4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_2_S2 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_1_S2 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_4_S4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_3_S4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_2_S4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_1_S4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_8 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_7 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_6 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_5 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_3 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_2 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_1 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_le_pred [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
lt_pred [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
lt_nm_mult [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult_S_S [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_SO_mult [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult_csts [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult_cst [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult_n_Sn [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult_lt_O [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_no_out_o [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
lt_no_in_i [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
lt_neq_O_pred [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
lt_transp_r [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
lt_O_minus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
Lt_eq_Gt [lemma, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
lt_SO_or_eq_O_or_SO_dec [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Dec]
lt_or_eq_O_dec [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Dec]
lt_m_neq [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Eq_Le_Lt]
lt_Ex_n [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Eq_Le_Lt]
lt_O [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Eq_Le_Lt]
lt_quotient2_n [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
lt_no_zerob [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
lt_plus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
lt_le_pred [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
lt_eq_lt [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
lt_S_le [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
l2_tt [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l2_tf [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l2_ft [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l2_ff [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ftff [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_fftf [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tfff [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ffft [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tttt [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tfft [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_fttf [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tttf [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ttft [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ttff [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tftt [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tftf [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_fttt [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ftft [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_fftt [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ffff [definition, in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
M
make_list_of_v [definition, in Fairisle.Libraries.Lib_Lists.dlist_Compl]Manip_BoolLists [library]
MAP_map_g [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
MAP_g [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Mealy [definition, in Fairisle.Libraries.Lib_Automata.Mealy]
Mealy [library]
Mealy_Description.Out [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Mealy_Description.Trans [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Mealy_Description.State_type [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Mealy_Description.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Mealy_Description.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Mealy_Description [section, in Fairisle.Libraries.Lib_Automata.Mealy]
merge [definition, in Fairisle.Libraries.Lib_Lists.Lists_of_lists]
minus_Sn_n [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
minus_minus_plus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
minus_pred_S [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
minus_S [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
minus_SS_n [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
Moore [definition, in Fairisle.Libraries.Lib_Automata.Moore]
Moore [library]
Moore_Description.Out [variable, in Fairisle.Libraries.Lib_Automata.Moore]
Moore_Description.Trans [variable, in Fairisle.Libraries.Lib_Automata.Moore]
Moore_Description.State_type [variable, in Fairisle.Libraries.Lib_Automata.Moore]
Moore_Description.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Moore]
Moore_Description.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Moore]
Moore_Description [section, in Fairisle.Libraries.Lib_Automata.Moore]
Moore_Mealy [library]
mult_eq_zero_bis [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_reg_l_bis [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_reg_l [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_S_O [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_eq_zero [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_minus_distr_left [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_plus_distr_left [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_odd_odd [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
mult_even [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
N
NAND2 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]NAND3 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
NAND4 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
nat_order_dec [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Dec]
nat_bool [definition, in Fairisle.Libraries.Lib_Lists.Conversions]
neg_b_true_b_false [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
neg_orb_neg_andb [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
neg_andb_neg_orb [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
neg_neg [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
neq_O_le [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Eq_Le_Lt]
NextPort [library]
Non_empty_Hd [lemma, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
non_empty [lemma, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
non_empty_dep [lemma, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
NORL [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
NORL3 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
NOR2 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
NOR3 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
NOR4 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
not_d_In_SUCSUCSUC_SSSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUCSUCSUC_SO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUCSUC_SSSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC_SSSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUCSUCSUC_SSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUCSUC_SSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC_SSO_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUCSUC1_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC1_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC2_l4 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC1_l3 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC0_l2 [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_lt_4 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
not_S_eq [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Eq_Le_Lt]
NOT_TRIGGER_A [constructor, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
no_true_false [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
No_Inv [definition, in Fairisle.Libraries.Lib_Automata.Mealy]
No_P [definition, in Fairisle.Libraries.Lib_Automata.Mealy]
no_in [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
no_out [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
no_zero_div [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
no_or_l [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_or_r [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_no_A [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_or_and_inv [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_or_and [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_or_inv [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_or [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_and_r [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_and_l [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_zerob_true [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
nth [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Nth [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Nth_func [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
nth_S [constructor, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
nth_O [constructor, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
nth_spec [inductive, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
number_P [definition, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
NXOR2 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
NXOR3 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
NXOR4 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
O
OBUF [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]Odd [inductive, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
odd [inductive, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
Odd_odd [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
Odd_intro [constructor, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
odd_even [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
odd_intro [constructor, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
Olatch [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
OLATCH [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
one [abbreviation, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
orb_false_r [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
orb_false_l [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
orb_false [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
orb_sym [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
orb_b_false [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
orb_sym [lemma, in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
order [inductive, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
OR2 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
Or3 [inductive, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
or3 [inductive, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
OR3 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
or3_Right [constructor, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
or3_Middle [constructor, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
or3_Left [constructor, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
OR4 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
outdis [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
OUTDIS_Behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp_Behaviour]
Outdis_behaviour [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
OUTFFd [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
OutPC_TimingPDecode_Id [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
OutPC_Timing_PDecode [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
OutPC_arbiter [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
OutPC_TimingPDecode_Id [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OutPC_Timing_PDecode [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OutPC_arbiter [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OutputDisable [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
OutputDisable' [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
outputDisable' [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
output_is_identity.H_output [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.output [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.f [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.States_A2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.States_A1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.A2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.A1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Out2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Out1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Trans2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Trans1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.State_type_a2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.State_type_a1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Output_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Output_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Input_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Input_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity [section, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Output_requested [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
output_four_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
output_two_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
output_arbiter [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Output_rel [definition, in Fairisle.Libraries.Lib_Automata.Mealy]
Output_relation_t [lemma, in Fairisle.Fairisle.PROOFS.Timing_Proof]
output_four_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
output_two_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
output_arbiter [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Output_relation_A [lemma, in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Output_relation_p [lemma, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Output_relation_a4 [lemma, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
OutSC_Arbitration [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
OutSC_Arbitration [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OutSC_Arbitration_beh [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Out_latch [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
Out_Buf [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
Out_PC_part [definition, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Out_Four_Arbiters_Mealy [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Out_Four_Arbiters [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Out_priority_decode [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_Struct_four_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_Struct_two_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_ArbiterXY [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_outdis [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_Struct_Timing [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_FC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Out_SC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Out_PC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Out_Timing_Mealy [definition, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Out_Timing [definition, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Out_priority_decode [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Out_Struct_four_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Out_Struct_two_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Out_ArbiterXY [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Out_outdis [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Out_Struct_Timing [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OUT_LATCH [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
OUT_BUF [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
Out_PriorityDecode_Mealy [definition, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Out_PriorityDecode [definition, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Out_id [definition, in Fairisle.Libraries.Lib_Automata.Identity]
Out_Arbitration_Mealy [definition, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Out_Arbitration [definition, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Out_Mealy [definition, in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Out_TimingPDecode_Id [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Out_Timing_PDecode [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
O_minus_S [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
O_or_no_dec [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Dec]
P
pair_fst_snd [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]pair_eq [lemma, in Fairisle.Libraries.Lib_Basis.Product]
Parallel_Composition.output [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.f [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.States_A2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.States_A1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.A2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.A1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Out2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Out1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Trans2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Trans1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.State_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.State_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Output_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Output_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Input_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Input_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition [section, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Particular_Parallel_Composition.output_part [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.f [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.S1' [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.S1 [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Out1 [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Trans1 [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.State_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Output_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Input_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition [section, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Pause [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
PAUSE [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
PC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
PC_Mealy [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
PC_part [definition, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Pdt_List4_List3 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
pdt_List2 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
PickSuccessfulInput [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
PickSuccessfulInput [library]
plus_m_mult_n_m [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
plus_mult [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
plus_odd_odd [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
plus_odd_even [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
plus_even_odd [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
plus_even_even [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
plus_eq_zero [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
plus_opp [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
PolyList_dlist [library]
Ports [section, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.TypePorts]
PortsCompl [library]
Ports.i [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.TypePorts]
Ports.o [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.TypePorts]
pred_no_O [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
pred_O [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
pred_n_O [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
pred_diff_lt [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
pred_diff_O [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
pred_mult [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
pred_minus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
pred_minus_minus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
pred_odd_even [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
Prifilunit [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Prifil4clb [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
PriorityDecode_Correctness.Cst_True [variable, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
PriorityDecode_Correctness.Reg_type [variable, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
PriorityDecode_Correctness.Output_type [variable, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
PriorityDecode_Correctness.Input_type [variable, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
PriorityDecode_Correctness [section, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
PriorityDecode_Proof [library]
PriorityRequests [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Priority_Decode_Less_Pause [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Priority_4 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
priority_bits [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
pri_bits [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
Product [library]
prod_3 [inductive, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
programming_3.C [variable, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
programming_3.B [variable, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
programming_3.A [variable, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
programming_3 [section, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
Projections_on_fixed_dlists.A [variable, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Projections_on_fixed_dlists [section, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Proj_lists [library]
proof_outportno [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
proof_inportno [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
proof_in [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
proof_out [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
put_end [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
P_a4 [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
P_a4_Ok [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
P_a4_inv [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
P_Timing [definition, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
P_A [definition, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
R
Reg [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]Regf [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Remove_i [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
remove_i [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
RequestsToArbitrate [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
Rev [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Rewrite_Snd [lemma, in Fairisle.Libraries.Lib_Basis.Product]
Rewrite_Fst [lemma, in Fairisle.Libraries.Lib_Basis.Product]
Rlatch [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
rlatch [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
RLATCH [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
RLATCH2 [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
RoundRobin [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
RoundRobin [library]
RoundRobinArbiter [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
RoundRobinArbiter_simpl [lemma, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
Round_Robin_function.k [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
Round_Robin_function.Outportno [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
Round_Robin_function.Inportno [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
Round_Robin_function.o [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
Round_Robin_function.i [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
Round_Robin_function [section, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
ROUTE_t [constructor, in Fairisle.Fairisle.PROOFS.Timing_Proof]
route_bits [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
rou_bits [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
R_a4 [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
R_Timing [definition, in Fairisle.Fairisle.PROOFS.Timing_Proof]
R_Priority_Decode [definition, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
R_A [definition, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
S
same_quotient_order [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]SC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
scd_list2 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Scd_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Scd_of_l3 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Scd_of_l2 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Second [constructor, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
seg [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Seg [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Segment [definition, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
segment [definition, in Fairisle.Libraries.Lib_Lists.dlist_Compl]
seg' [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Seg' [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Series_Composition.A2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.A1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Out2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Out1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Trans2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Trans1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.State_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.State_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Output_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Output_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition [section, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
seven [abbreviation, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
sig_true [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
sig_false [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
simplification1 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
simplification2 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
simplification3 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
six [abbreviation, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
SM4 [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
Snd_Compact [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Snd_3 [abbreviation, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
snd_3 [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
split_d_list [lemma, in Fairisle.Libraries.Lib_Lists.Dependent_lists]
split_List4 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
split_List3 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
split_List2 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Square [definition, in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
Square_strict_inc [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
Square_inc [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
Square_exp_2 [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
START_a4 [constructor, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
START_t [constructor, in Fairisle.Fairisle.PROOFS.Timing_Proof]
START_p [constructor, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
START_A [constructor, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
StatesSC_ARBITRATION [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
StatesSC_ARBITRATION [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
States_SC_simpl [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
States_PC_part [definition, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
States_FOUR_ARBITERS [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
States_TIMINGPDECODE_ID [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
States_TIMING_PDECODE [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
States_Mealy [definition, in Fairisle.Libraries.Lib_Automata.Mealy]
States_FC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
States_SC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
States_A1A2 [abbreviation, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
States_PC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
States_Structure_TIMING [definition, in Fairisle.Fairisle.PROOFS.Timing_Proof]
States_TIMING [definition, in Fairisle.Fairisle.PROOFS.Timing_Proof]
States_TIMINGPDECODE_ID [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
States_TIMING_PDECODE [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
States_Structure_PRIORITY_DECODE [definition, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
States_PRIORITY_DECODE [definition, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
States_IDENTITY [definition, in Fairisle.Libraries.Lib_Automata.Identity]
States_ARBITRATION [definition, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
States_Beh_SC_ARBITRATION [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
States_Beh_TIMINGPDECODE_ID [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
States_Beh_TIMING_PDECODE [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
STATE_a4 [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
STATE_p [definition, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
state_id [inductive, in Fairisle.Libraries.Lib_Automata.Identity]
STATE_A [definition, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Stream [inductive, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Stream_to_dlist [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
strip_off_last [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
strip_off_first [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Structure_ARBITRATION [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_TIMINGPDECODE_ID [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_TIMING_PDECODE [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_PRIORITY_DECODE [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_FOUR_ARBITERS [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_TWO_ARBITERS [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_ARBITER [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_ArbiterXY [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_Outdis [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_TIMING [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_ARBITRATION [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_TIMINGPDECODE_ID [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_TIMING_PDECODE [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_PRIORITY_DECODE [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_FOUR_ARBITERS [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_TWO_ARBITERS [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_ARBITER [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_ArbiterXY [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_Outdis [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_TIMING [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_States_FOUR_ARBITERS [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Struct_Beh_Arbitration.p_0 [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.g22_0 [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.g21_0 [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.g12_0 [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.g11_0 [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.fs_act_signals [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.fs_0 [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.Act [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.Fs [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.i [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.Input_type [variable, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration [section, in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
subst [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
SuccessfulInput [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
SuccessfulInput [library]
Successor_Modulo_NbPorts.no [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
Successor_Modulo_NbPorts.Inportno [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
Successor_Modulo_NbPorts.i [variable, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
Successor_Modulo_NbPorts [section, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
SUC_MODN [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
sym_or [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
sym_and [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Prop]
Syntactic_Def [library]
S_head_States_SC [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
S_tail_States_SC [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
S_head_States_PC [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
S_tail_States_PC [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
S_map_output [lemma, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
S_head_Compact [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_tail_Compact [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_tail_dlist_to_Stream [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_head_S_map [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_tail_S_map [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Thd_of_3_Compact [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Snd_of_3_Compact [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Two_Fst [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Snd_pdt [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Fst_pdt [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Fth_of_4 [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Thd_of_4 [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Snd_of_4 [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Thd_of_3 [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Snd_of_3 [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Snd [abbreviation, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Fst [abbreviation, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_list_of_seg [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_list_of_nth [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Fold_List [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Unfold_List [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Remove_i [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Seg [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Nth [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map_f [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map_id [lemma, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_tls [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_hds [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map4 [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map3 [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map2 [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_tail [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_head [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_cons [constructor, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_head_Moore [lemma, in Fairisle.Libraries.Lib_Automata.Moore]
S_tail_Moore [lemma, in Fairisle.Libraries.Lib_Automata.Moore]
S_head_States_Mealy [lemma, in Fairisle.Libraries.Lib_Automata.Mealy]
S_tail_States_Mealy [lemma, in Fairisle.Libraries.Lib_Automata.Mealy]
S_tail_Mealy [lemma, in Fairisle.Libraries.Lib_Automata.Mealy]
S_tail_Structure_States_FOUR_ARBITERS [lemma, in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_tail_States_FOUR_ARBITERS [lemma, in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_head_States_Structure_TIMING [lemma, in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_tail_States_Structure_TIMING [lemma, in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_head_States_TIMING [lemma, in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_tail_States_TIMING [lemma, in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_tail_Behaviour_PDECODE [lemma, in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_head_Behaviour_PDECODE [lemma, in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_head_Behaviour_TIMING [lemma, in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_tail_Behaviour_TIMING [lemma, in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_pred_n [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
S_tail_Behaviour_TIMINGPDECODE_ID [lemma, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
S_even_odd [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
S_odd_even [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
S_map_Fth_of_l4 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
S_map_Thd_of_l4 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
S_map_Scd_of_l4 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
S_map_Fst_of_l4 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
S_Ackor [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
S_plus [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
S_Fst_S_f_tp_simpl [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
S_Snd_S_f_tpi_simpl [lemma, in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
S_tail_Behaviour_IDENTITY [lemma, in Fairisle.Libraries.Lib_Automata.Identity]
S_three_fst_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_List_of_scd_of_l2 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_List_of_tails_of_l2 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_List_of_fst_of_l2 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Fth_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Thd_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Scd_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Fst_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Scd_of_l2 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Fst_of_l2 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_pred [lemma, in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
S1S1 [abbreviation, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
T
Tests_in_dlists.d_List [variable, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]Tests_in_dlists.P_dec [variable, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
Tests_in_dlists.P [variable, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
Tests_in_dlists.A [variable, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
Tests_in_dlists [section, in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
Tests_in_d_lists [library]
test_port [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
Thd_3 [abbreviation, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
thd_3 [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
Thd_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Thd_of_l3 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Third [constructor, in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
three [abbreviation, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
three_fst_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Timing [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Timing_and_PDecode.output_tp [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Timing_and_PDecode.f_tp [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Timing_and_PDecode.Input_vector_type [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Timing_and_PDecode [section, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Timing_Aux [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Timing_Correctness.Cst_True [variable, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Timing_Correctness.Reg_type [variable, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Timing_Correctness.Output_type [variable, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Timing_Correctness.Input_type [variable, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Timing_Correctness [section, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Timing_and_PDecode.output_tp [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Timing_and_PDecode.f_tp [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Timing_and_PDecode.Input_vector_type [variable, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Timing_and_PDecode [section, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Timing_Aux [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Timing_Arbiter_Proof.fs_act_signals [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Timing_Arbiter_Proof.fs_0 [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Timing_Arbiter_Proof.Act [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Timing_Arbiter_Proof.Fs [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Timing_Arbiter_Proof [section, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Timing_and_PDecode_beh.output_tp [variable, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Timing_and_PDecode_beh.f_tp [variable, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Timing_and_PDecode_beh.Input_type [variable, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Timing_and_PDecode_beh [section, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Timing_Arbiter [library]
Timing_Proof [library]
tls [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
tls_simpl [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Tools_Inf [library]
Tool_about_Lemma_on_rules.output [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.f [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.B2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.B1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.A2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.A1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Outb2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Outb1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Transb2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Transb1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Outa2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Outa1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Transa2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Transa1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.State_type_b2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.State_type_b1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.State_type_a2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.State_type_a1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Output_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Output_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Input_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Input_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules [section, in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Equivalence_2_Mealy.A2 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.A1 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Out2 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Out1 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Trans2 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Trans1 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.State_type_2 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.State_type_1 [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Output_type [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Input_type [variable, in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy [section, in Fairisle.Libraries.Lib_Automata.Mealy]
transf [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Transformation [section, in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
Transformation.A [variable, in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
transf_List4_List3 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf_simpl [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf1 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf2 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf3 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf4 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
TransPC_TimingPDecode_Id [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
TransPC_Timing_PDecode [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
TransPC_arbiter [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
TransPC_TimingPDecode_Id [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
TransPC_Timing_PDecode [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
TransPC_arbiter [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
TransSC_Arbitration [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
TransSC_Arbitration [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
TransSC_Arbitration_beh [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Trans_PC_part [definition, in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Trans_Four_Arbiters [definition, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Trans_priority_decode [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Trans_Struct_four_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Trans_Struct_two_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Trans_ArbiterXY [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Trans_outdis [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Trans_FC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Trans_SC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Trans_PC [definition, in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Trans_Timing [definition, in Fairisle.Fairisle.PROOFS.Timing_Proof]
Trans_priority_decode [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Trans_Struct_four_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Trans_Struct_two_arbiters [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Trans_ArbiterXY [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Trans_outdis [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Trans_PriorityDecode [definition, in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Trans_id [definition, in Fairisle.Libraries.Lib_Automata.Identity]
Trans_Arbitration [definition, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Trans_TimingPDecode_Id [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Trans_Timing_PDecode [definition, in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
TRIGGER_A [constructor, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Triplet [abbreviation, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
triplet [constructor, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
triplet_fst_snd_thd [lemma, in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
triplet_simpl [lemma, in Fairisle.Libraries.Lib_Basis.Product]
true_orb_intro [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
True' [inductive, in Fairisle.Libraries.Lib_Automata.Mealy]
two [abbreviation, in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
Two_List2_List4 [abbreviation, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Two_last_of_l3 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Two_fst_of_l3 [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Two_last_of_l4' [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Two_Fst_of_l4' [definition, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Two_last_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
Two_Fst_of_l4 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
two_fst_of_l3 [definition, in Fairisle.Libraries.Lib_Lists.Proj_lists]
TypePorts [library]
T_Outportno [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.TypePorts]
T_Inportno [definition, in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.TypePorts]
U
UnCompact [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]Unfold_List [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Unfold_tls_4 [lemma, in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Upper_Bound_Bool [lemma, in Fairisle.Libraries.Lib_Lists.Conversions]
upper_bound_bool [lemma, in Fairisle.Libraries.Lib_Lists.Conversions]
V
Verif_hyp.fs_act_signals [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]Verif_hyp.fs_0 [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.Route [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.Pri [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.Act [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.Fs [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.i [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.Input_type [variable, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp [section, in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
W
WAIT_a4 [constructor, in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]WAIT_t [constructor, in Fairisle.Fairisle.PROOFS.Timing_Proof]
WAIT_BEGIN_A [constructor, in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
wcat [definition, in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Wire [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
Wire_bool [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
X
xGrant' [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]Xnor [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
Xor [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
XOR2 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
XOR3 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
XOR4 [definition, in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
x_Grant' [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
x_Grant [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
x_1_or_y_0 [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
Y
yGrant' [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]y_eq_multxy [lemma, in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
y_Grant' [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
y_Grant [definition, in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
Z
zerob_pred_false [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]zerob_lt [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
zerob_pred_no [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
zerob_If [lemma, in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
zeros [definition, in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Variable Index
A
Additional_Def_and_Lemmas.eq_dec [in Fairisle.Libraries.Lib_Lists.dlist_Compl]Additional_Def_and_Lemmas.A [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Arbitration_Structure.Input_vector_type [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Arbitration_Structure.Input_vector_type [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Arbitration_Correctness.p_0 [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.o_a4_0 [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.g22_0 [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.g21_0 [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.g12_0 [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.g11_0 [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_Correctness.Input_type [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_between_several_inputs.requests [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
Arbitration_between_several_inputs.Inportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
Arbitration_Specification.Output_type [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Arbitration_Specification.Input_type [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Arbitration_beh.Input_type [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
D
Definitions_and_lemmas_about_ports.Outportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]Definitions_and_lemmas_about_ports.Inportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Definitions_and_lemmas_about_ports.o [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Definitions_and_lemmas_about_ports.i [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Dependent_lists.A [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_Lists_Compl.d_List [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
d_Lists_Compl.C [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
d_Lists_Compl.B [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
d_Lists_Compl.A [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
E
Equivalence_2_Mealy.R [in Fairisle.Libraries.Lib_Automata.Mealy]Equivalence_2_Mealy.P_is_true [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.P [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.States_A2 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.States_A1 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.A2 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.A1 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Out2 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Out1 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Trans2 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Trans1 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.State_type_2 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.State_type_1 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Output_type [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_2_Mealy.Input_type [in Fairisle.Libraries.Lib_Automata.Mealy]
Equivalence_Mealy_to_Moore2.Out_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.Trans_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.State_type_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.A_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.Out_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.Trans_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.State_type_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.Output_type [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore2.Input_type [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Out_Mealy2 [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Trans_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.A_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Out_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Trans_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.State_type [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Output_type [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2.Input_type [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.A_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Out_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Trans_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.State_type_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.A_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Out_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Trans_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.State_type_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Output_type [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1.Input_type [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.A_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.Trans_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.A_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.Out_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.Trans_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.state_type [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.Output_type [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1.Input_type [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equiv_on_rule_SC.B2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.B1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.A2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.A1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Outb2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Outb1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Transb2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Transb1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Outa2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Outa1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Transa2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Transa1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.State_type_b2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.State_type_b1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.State_type_a2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.State_type_a1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Output_type_2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Output_type_1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_SC.Input_type [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.output [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.f [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.B2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.B1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.A2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.A1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Outb2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Outb1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Transb2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Transb1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Outa2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Outa1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Transa2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Transa1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.State_type_b2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.State_type_b1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.State_type_a2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.State_type_a1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Output_type_2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Output_type_1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Input_type [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Input_type_2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC.Input_type_1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_about_P.P [in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_about_P.State_type_2 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_about_P.State_type_1 [in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_about_P.Input_type [in Fairisle.Libraries.Lib_Automata.Mealy]
F
Feedback_Composition.upd_s2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]Feedback_Composition.upd_s1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.out [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.input [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.A2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.A1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Out2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Out1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Trans2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Trans1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.State_type_2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.State_type_1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Output_type_2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Output_type [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Input_type_1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Feedback_Composition.Input_type [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Filter_and_Pick.and3 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.and2 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.eq_true [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.d_map_andb [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.requests [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.priorities [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.actives [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Filter_and_Pick.Inportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
fixed_lists.A [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
For_ltReq.H8 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H7 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H6 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H5 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H4 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H3 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H2 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.H1 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.o22 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.o21 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.o12 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.o11 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.g22 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.g21 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.g12 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.g11 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.o [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
For_ltReq.g [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
Four_Arbiters_Specif.Reg_type [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Four_Arbiters_Specif.Output_type [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Four_Arbiters_Specif.Input_type [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Four_Arbiters_Proof_Correctness.g22_0 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness.g21_0 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness.g12_0 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness.g11_0 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness.Reg_type [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Four_Arbiters_Proof_Correctness.Input_type [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
From_init_states.p_0 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.g22_0 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.g21_0 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.g12_0 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.g11_0 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.fs_act_signals [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.fs_0 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.Route [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.Pri [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.Act [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.Fs [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.i [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
From_init_states.Input_type [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
I
Identity_and_TimingPDecode.output_tpi [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]Identity_and_TimingPDecode.f_tpi [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Identity_and_TimingPDecode.Input_vector_type [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Identity_and_TimingPDecode.output_tpi [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Identity_and_TimingPDecode.f_tpi [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Identity_and_TimingPDecode.Input_vector_type [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Identity_and_TimingPDecode_beh.output_tpi [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Identity_and_TimingPDecode_beh.f_tpi [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Identity_and_TimingPDecode_beh.Input_type [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Identity.Input_type [in Fairisle.Libraries.Lib_Automata.Identity]
Infinite_List.B [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Infinite_List.A [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
M
Mealy_Description.Out [in Fairisle.Libraries.Lib_Automata.Mealy]Mealy_Description.Trans [in Fairisle.Libraries.Lib_Automata.Mealy]
Mealy_Description.State_type [in Fairisle.Libraries.Lib_Automata.Mealy]
Mealy_Description.Output_type [in Fairisle.Libraries.Lib_Automata.Mealy]
Mealy_Description.Input_type [in Fairisle.Libraries.Lib_Automata.Mealy]
Moore_Description.Out [in Fairisle.Libraries.Lib_Automata.Moore]
Moore_Description.Trans [in Fairisle.Libraries.Lib_Automata.Moore]
Moore_Description.State_type [in Fairisle.Libraries.Lib_Automata.Moore]
Moore_Description.Output_type [in Fairisle.Libraries.Lib_Automata.Moore]
Moore_Description.Input_type [in Fairisle.Libraries.Lib_Automata.Moore]
O
output_is_identity.H_output [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]output_is_identity.output [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.f [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.States_A2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.States_A1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.A2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.A1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Out2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Out1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Trans2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Trans1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.State_type_a2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.State_type_a1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Output_type_2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Output_type_1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Input_type [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Input_type_2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
output_is_identity.Input_type_1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
P
Parallel_Composition.output [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]Parallel_Composition.f [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.States_A2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.States_A1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.A2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.A1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Out2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Out1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Trans2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Trans1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.State_type_2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.State_type_1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Output_type [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Output_type_2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Output_type_1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Input_type [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Input_type_2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Parallel_Composition.Input_type_1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Particular_Parallel_Composition.output_part [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.f [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.S1' [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.S1 [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Out1 [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Trans1 [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.State_type_1 [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Output_type [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Output_type_1 [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Input_type [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Particular_Parallel_Composition.Input_type_1 [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Ports.i [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.TypePorts]
Ports.o [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.TypePorts]
PriorityDecode_Correctness.Cst_True [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
PriorityDecode_Correctness.Reg_type [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
PriorityDecode_Correctness.Output_type [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
PriorityDecode_Correctness.Input_type [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
programming_3.C [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
programming_3.B [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
programming_3.A [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
Projections_on_fixed_dlists.A [in Fairisle.Libraries.Lib_Lists.Proj_lists]
R
Round_Robin_function.k [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]Round_Robin_function.Outportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
Round_Robin_function.Inportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
Round_Robin_function.o [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
Round_Robin_function.i [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
S
Series_Composition.A2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]Series_Composition.A1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Out2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Out1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Trans2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Trans1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.State_type_2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.State_type_1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Output_type_2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Output_type_1 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Series_Composition.Input_type [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Struct_Beh_Arbitration.p_0 [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.g22_0 [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.g21_0 [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.g12_0 [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.g11_0 [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.fs_act_signals [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.fs_0 [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.Act [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.Fs [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.i [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Struct_Beh_Arbitration.Input_type [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Successor_Modulo_NbPorts.no [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
Successor_Modulo_NbPorts.Inportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
Successor_Modulo_NbPorts.i [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
T
Tests_in_dlists.d_List [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]Tests_in_dlists.P_dec [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
Tests_in_dlists.P [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
Tests_in_dlists.A [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
Timing_and_PDecode.output_tp [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Timing_and_PDecode.f_tp [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Timing_and_PDecode.Input_vector_type [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Timing_Correctness.Cst_True [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Timing_Correctness.Reg_type [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Timing_Correctness.Output_type [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Timing_Correctness.Input_type [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Timing_and_PDecode.output_tp [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Timing_and_PDecode.f_tp [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Timing_and_PDecode.Input_vector_type [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Timing_Arbiter_Proof.fs_act_signals [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Timing_Arbiter_Proof.fs_0 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Timing_Arbiter_Proof.Act [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Timing_Arbiter_Proof.Fs [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Timing_and_PDecode_beh.output_tp [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Timing_and_PDecode_beh.f_tp [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Timing_and_PDecode_beh.Input_type [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Tool_about_Lemma_on_rules.output [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.f [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.B2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.B1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.A2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.A1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Outb2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Outb1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Transb2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Transb1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Outa2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Outa1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Transa2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Transa1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.State_type_b2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.State_type_b1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.State_type_a2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.State_type_a1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Output_type_2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Output_type_1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Input_type [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Input_type_2 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Lemma_on_rules.Input_type_1 [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Equivalence_2_Mealy.A2 [in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.A1 [in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Out2 [in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Out1 [in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Trans2 [in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Trans1 [in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.State_type_2 [in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.State_type_1 [in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Output_type [in Fairisle.Libraries.Lib_Automata.Mealy]
Tool_about_Equivalence_2_Mealy.Input_type [in Fairisle.Libraries.Lib_Automata.Mealy]
Transformation.A [in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
V
Verif_hyp.fs_act_signals [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]Verif_hyp.fs_0 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.Route [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.Pri [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.Act [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.Fs [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.i [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Verif_hyp.Input_type [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Library Index
A
Arbiter4_SpecifArbiter4_Proof_lemmas
Arbiter4_Proof
Arbitration
Arbitration_Proof
Arbitration_Specif
Arbitration_beh_sc
Arith_Compl
B
Base_StructBase_Behaviour
Basic_composition_rules
Behaviour_Struct_lemmas
Bool_Compl
C
Compare_NatConversions
D
Dependent_listsDependent_lists_Compl
Derived_composition_rules
dlist_Compl
E
ElementCombElementComb_Behaviour
ElementTemp
ElementTemp_Behaviour
Equiv_Struct_Beh_Arbitration
F
Fixed_dListsG
GatesGates_Del
Gen_Gates_Del
I
IdentityInfinite_lists
Injections
Invariant_a4_S
L
Lemmas_StructLemmas_on_fcts
Lemmas_on_Basic_rules
Lemmas_Comb_Behaviour
Lemmas_for_Arbitration
Lib_Set_Products
Lib_Plus
Lib_Pred
Lib_Minus
Lib_Zerob
Lib_Exp
Lib_Square
Lib_Eq_Le_Lt
Lib_Prop
Lib_Bool
Lib_Fact
Lib_Dec
Lib_Mult
Lib_Div_Even_Odd
Lists_of_lists
M
Manip_BoolListsMealy
Moore
Moore_Mealy
N
NextPortP
PickSuccessfulInputPolyList_dlist
PortsCompl
PriorityDecode_Proof
Product
Proj_lists
R
RoundRobinS
SuccessfulInputSyntactic_Def
T
Tests_in_d_listsTiming_Arbiter
Timing_Proof
Tools_Inf
TypePorts
Lemma Index
A
Ackor_true_RequestsToArbitrate [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]Ackor_false [in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Ackor_ltReq_false [in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Ackor_dmap_false_4 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_dmap_true_4 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_dmap_false_2 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_dmap_true_2 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_false_fth [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_false_thd [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_false_scd [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
Ackor_false_fst [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Lemmas_Struct]
andb_negb_true_l [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_negb_true_r [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_true_r [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_true_l [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_true [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_false [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
andb_sym [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
and_sym [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
Arbiter_last [in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Arbiter_last_ff [in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Arbiter_last_ft [in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Arbiter_last_tf [in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Arbiter_last_tt [in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
A_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
a_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
B
bool_dec [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]C
Compact_PC_id [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]comparisonE [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comparisonG [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comparisonL [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comp_sym_E [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comp_sym_GL [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
comp_sym_LG [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
Correct_TIMING [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Correct_ARBITRATION [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Correct_PRIORITY_DECODE [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Correct_FOUR_ARBITERS [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Correct_ARBITRATION_end [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Cst_True_inv_t [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Cst_True_inv_pdecode [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
D
dif_0_pred_eq_0_eq_1 [in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]div_minus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
div_plus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
div_odd_odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
div_odd_even [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
d_In_SUCSUCSUC_SSSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUCSUCSUC_SO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUCSUC_SSSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC_SSSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUCSUCSUC_SSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUCSUC_SSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC_SSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUCSUC1_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC1_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC2_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC1_l3 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
d_In_SUC0_l2 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
E
empty [in Fairisle.Libraries.Lib_Lists.Dependent_lists]empty_dep [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
eqp1 [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
eqp2 [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
eqp3 [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
eqp4 [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
eqp5 [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
EqS_Compact [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_S_Snd_of_3 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_S_Thd_of_3 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_sym [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_reflex [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_trans [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
EqS_Moore [in Fairisle.Libraries.Lib_Automata.Moore]
eqS_about_P [in Fairisle.Libraries.Lib_Automata.Mealy]
EqS_States_Mealy [in Fairisle.Libraries.Lib_Automata.Mealy]
EqS_Mealy [in Fairisle.Libraries.Lib_Automata.Mealy]
eqS_Inv_P_Timing [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
EqS_transf [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
EqS_Snd_SC_TIMING [in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
EqS_IDENTITY [in Fairisle.Libraries.Lib_Automata.Identity]
EqS_S_Fth_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
EqS_S_Thd_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
EqS_S_Scd_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
EqS_S_Fst_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
EqS_const_stream [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equiv_States_PC [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
equiv_SC' [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
equiv_SC [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
equiv_PC [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_S1S1_PC_part [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Equiv_Four_Arbiters_Moore_Mealy [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
equiv_out_Four_Arbiters_Moore_Mealy [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Equiv_2_Mealy_tool [in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_2_Mealy [in Fairisle.Libraries.Lib_Automata.Mealy]
Equiv_A1A2_FC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Equiv_A1A2_SC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Equiv_States_A1A2_PC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Equiv_A1A2_PC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Equiv_Timing_Moore_Mealy [in Fairisle.Fairisle.PROOFS.Timing_Proof]
equiv_out_Timing [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Equiv_Behaviour_TIMINGPDECODE_ID [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Equiv_PriorityDecode_Moore_Mealy [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
equiv_out_PriorityDecode [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Equiv_Arbitration_Moore_Mealy [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
equiv_out_Arbitration_Moore_Mealy [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Equiv_Mealy_Moore [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equiv_Moore_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equiv_Struct_Beh_Arbitration [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Equiv_a4 [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Equiv_tpi [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
equiv1 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
equiv2 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
eq_n_SM4_4_times [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
eq_Square_exp_n [in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
eq_pred [in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
eq_minus_plus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
eq_or_not_bis [in Fairisle.Libraries.Lib_Arithmetic.Lib_Dec]
eq_fs_and_RouteE_false [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
eq_exp_2_exp_n [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
eq_dlist_Head [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Eq_dlist_to_Stream_List4 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
eq_List4_map [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
eq_pair [in Fairisle.Libraries.Lib_Basis.Product]
Even_or_Odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
even_odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
even_or_odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
Exists1_atleast_or_not [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
exp_n_pos [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n_plus_p1 [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n_permut [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n_plus_mult [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n_neutre [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_n_incr [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_n_plus_m [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_incr [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_pos [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_le_pn_n [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_plus_pn_pn [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2_n_plus_n [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
Ex_n_lt_gen [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
F
fact_pred [in Fairisle.Libraries.Lib_Arithmetic.Lib_Fact]false_andb_true [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
false_neg_true [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
false_andb_b [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
false_orb_r [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
false_orb_l [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
Fst_Compact [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
fst_3 [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
fst_list2 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
I
id_list' [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]id_list3_thd [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
id_list3_scd [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
id_list3_fst [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
id_list3 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
id_list [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
ifProp_or [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
impl_no_no [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
Invariant_relation_t [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Invariant_relation_A [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Invariant_Init_states_A [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Invariant_a4_SSS [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
Invariant_relation_a4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Invariant_Init_states_a4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
Inv_Ok [in Fairisle.Libraries.Lib_Automata.Mealy]
inv_comparison [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
inv_comparisonG [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
inv_comparisonE [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
inv_comparisonL [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
Inv_a4' [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Inv_a4 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Inv_t_a4_Ok [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Inv_Init_states_t_a4 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Inv_P_Timing_Inv_A [in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
In_or_not [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Is_Inv_P_Timing [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
L
less_or_eq [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]less_div [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
le_number_P [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
le_8_8 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_7_8 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_7_7 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_6_8 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_5_8 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_5_7 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_5_6 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_4_8 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_4_4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_3_7 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_3_4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_3_3 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_2_4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_2_3 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_1_7 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_1_4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_1_3 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_1_2 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le_n_Square [in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
le_mult_r [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
le_mult_l [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
le_lt_plus_mult [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
le_mult_csts [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
le_mult_cst [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
le_reg_minus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
le_minus_n_Sn [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
le_minus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
le_exp_n_mult [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
le_SSS_bool_nat [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
le_S_bool_nat [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
le_transp_r [in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
le_transp_l [in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
le_lt_plus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
le_le_assoc_plus_minus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
le_minus_plus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
le_minusSS [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_n_mult_S_n [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_mult_l [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_Sn_le_n_pred [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_S_lt_O [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_leS [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_le_Sminus [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le_minusS [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
le8_le6 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
le8_lt7 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
List_dlist_cons [in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
List2Bool_dec [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
List2_access [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List4_map [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List4_of_pdt [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
ltReq_false_G4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof_lemmas]
ltReq_false_G3 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof_lemmas]
ltReq_false_G2 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof_lemmas]
ltReq_false_G1 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof_lemmas]
ltReq_1111 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_111O [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_11O1 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_11OO [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_1O11 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_1O1O [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_1OO1 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_1OOO [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_O111 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_O11O [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_O1O1 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_O1OO [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_OO11 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_OO1O [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
ltReq_OOO1 [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
lt_4_4cases [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
lt_8_S8 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_7_S8 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_3_S3 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_2_S3 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_1_S3 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_3_4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_2_4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_1_4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_2_S2 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_1_S2 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_4_S4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_3_S4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_2_S4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_1_S4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_8 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_7 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_6 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_5 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_3 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_2 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_O_1 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
lt_le_pred [in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
lt_pred [in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
lt_nm_mult [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult_S_S [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_SO_mult [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult_csts [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult_cst [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult_n_Sn [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_mult_lt_O [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
lt_no_out_o [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
lt_no_in_i [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
lt_neq_O_pred [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
lt_transp_r [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
lt_O_minus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
Lt_eq_Gt [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
lt_SO_or_eq_O_or_SO_dec [in Fairisle.Libraries.Lib_Arithmetic.Lib_Dec]
lt_or_eq_O_dec [in Fairisle.Libraries.Lib_Arithmetic.Lib_Dec]
lt_m_neq [in Fairisle.Libraries.Lib_Arithmetic.Lib_Eq_Le_Lt]
lt_Ex_n [in Fairisle.Libraries.Lib_Arithmetic.Lib_Eq_Le_Lt]
lt_O [in Fairisle.Libraries.Lib_Arithmetic.Lib_Eq_Le_Lt]
lt_quotient2_n [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
lt_no_zerob [in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
lt_plus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
lt_le_pred [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
lt_eq_lt [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
lt_S_le [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
M
minus_Sn_n [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]minus_minus_plus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
minus_pred_S [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
minus_S [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
minus_SS_n [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
mult_eq_zero_bis [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_reg_l_bis [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_reg_l [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_S_O [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_eq_zero [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_minus_distr_left [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_plus_distr_left [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
mult_odd_odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
mult_even [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
N
nat_order_dec [in Fairisle.Libraries.Lib_Arithmetic.Lib_Dec]neg_b_true_b_false [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
neg_orb_neg_andb [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
neg_andb_neg_orb [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
neg_neg [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
neq_O_le [in Fairisle.Libraries.Lib_Arithmetic.Lib_Eq_Le_Lt]
Non_empty_Hd [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
non_empty [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
non_empty_dep [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
not_d_In_SUCSUCSUC_SSSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUCSUCSUC_SO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUCSUC_SSSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC_SSSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUCSUCSUC_SSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUCSUC_SSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC_SSO_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUCSUC1_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC1_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC2_l4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC1_l3 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_d_In_SUC0_l2 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
not_lt_4 [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
not_S_eq [in Fairisle.Libraries.Lib_Arithmetic.Lib_Eq_Le_Lt]
no_true_false [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
no_zero_div [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
no_or_l [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_or_r [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_no_A [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_or_and_inv [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_or_and [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_or_inv [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_or [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_and_r [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_and_l [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
no_zerob_true [in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
O
Odd_odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]odd_even [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
orb_false_r [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
orb_false_l [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
orb_false [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
orb_sym [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
orb_b_false [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
orb_sym [in Fairisle.Libraries.Lib_Boolean.Bool_Compl]
Output_relation_t [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Output_relation_A [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Output_relation_p [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Output_relation_a4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
O_minus_S [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
O_or_no_dec [in Fairisle.Libraries.Lib_Arithmetic.Lib_Dec]
P
pair_fst_snd [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]pair_eq [in Fairisle.Libraries.Lib_Basis.Product]
PC_Mealy [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
plus_m_mult_n_m [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
plus_mult [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
plus_odd_odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
plus_odd_even [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
plus_even_odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
plus_even_even [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
plus_eq_zero [in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
plus_opp [in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
pred_no_O [in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
pred_O [in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
pred_n_O [in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
pred_diff_lt [in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
pred_diff_O [in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
pred_mult [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]
pred_minus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
pred_minus_minus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Minus]
pred_odd_even [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
proof_outportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
proof_inportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
P_a4_Ok [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
P_a4_inv [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
R
Rewrite_Snd [in Fairisle.Libraries.Lib_Basis.Product]Rewrite_Fst [in Fairisle.Libraries.Lib_Basis.Product]
RoundRobinArbiter_simpl [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
S
same_quotient_order [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]scd_list2 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
simplification1 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
simplification2 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
simplification3 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Snd_Compact [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
snd_3 [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
split_d_list [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
split_List4 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
split_List3 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
split_List2 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Square_strict_inc [in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
Square_inc [in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
Square_exp_2 [in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
States_SC_simpl [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
sym_or [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
sym_and [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
S_head_States_SC [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
S_tail_States_SC [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
S_head_States_PC [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
S_tail_States_PC [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
S_map_output [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
S_head_Compact [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_tail_Compact [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_tail_dlist_to_Stream [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_head_S_map [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_tail_S_map [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Thd_of_3_Compact [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Snd_of_3_Compact [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map_f [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map_id [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_head_Moore [in Fairisle.Libraries.Lib_Automata.Moore]
S_tail_Moore [in Fairisle.Libraries.Lib_Automata.Moore]
S_head_States_Mealy [in Fairisle.Libraries.Lib_Automata.Mealy]
S_tail_States_Mealy [in Fairisle.Libraries.Lib_Automata.Mealy]
S_tail_Mealy [in Fairisle.Libraries.Lib_Automata.Mealy]
S_tail_Structure_States_FOUR_ARBITERS [in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_tail_States_FOUR_ARBITERS [in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_head_States_Structure_TIMING [in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_tail_States_Structure_TIMING [in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_head_States_TIMING [in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_tail_States_TIMING [in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_tail_Behaviour_PDECODE [in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_head_Behaviour_PDECODE [in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_head_Behaviour_TIMING [in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_tail_Behaviour_TIMING [in Fairisle.Fairisle.PROOFS.Behaviour_Struct_lemmas]
S_pred_n [in Fairisle.Libraries.Lib_Arithmetic.Lib_Pred]
S_tail_Behaviour_TIMINGPDECODE_ID [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
S_even_odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
S_odd_even [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
S_map_Fth_of_l4 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
S_map_Thd_of_l4 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
S_map_Scd_of_l4 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
S_map_Fst_of_l4 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
S_plus [in Fairisle.Libraries.Lib_Arithmetic.Lib_Plus]
S_Fst_S_f_tp_simpl [in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
S_Snd_S_f_tpi_simpl [in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
S_tail_Behaviour_IDENTITY [in Fairisle.Libraries.Lib_Automata.Identity]
S_pred [in Fairisle.Libraries.Lib_Arithmetic.Arith_Compl]
T
thd_3 [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]tls_simpl [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf_simpl [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
triplet_fst_snd_thd [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
triplet_simpl [in Fairisle.Libraries.Lib_Basis.Product]
true_orb_intro [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
U
Unfold_tls_4 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]Upper_Bound_Bool [in Fairisle.Libraries.Lib_Lists.Conversions]
upper_bound_bool [in Fairisle.Libraries.Lib_Lists.Conversions]
X
x_1_or_y_0 [in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]Y
y_eq_multxy [in Fairisle.Libraries.Lib_Arithmetic.Lib_Mult]Z
zerob_pred_false [in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]zerob_lt [in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
zerob_pred_no [in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
zerob_If [in Fairisle.Libraries.Lib_Boolean.Lib_Zerob]
Constructor Index
A
ACTIVE_A [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]AT_LEAST_ONE_IS_ACTIVE_a4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
C
C_Inv [in Fairisle.Libraries.Lib_Automata.Mealy]C_Inv_t [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
D
DECODE_p [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]d_cons [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_nil [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
E
E [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]eqS [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
eq4_LS1 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
eq4_LSO [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Even_intro [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
even_intro [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
F
First [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]G
G [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]I
IDENTITY [in Fairisle.Libraries.Lib_Automata.Identity]I' [in Fairisle.Libraries.Lib_Automata.Mealy]
L
L [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]N
NOT_TRIGGER_A [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]nth_S [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
nth_O [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
O
Odd_intro [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]odd_intro [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
or3_Right [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
or3_Middle [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
or3_Left [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
R
ROUTE_t [in Fairisle.Fairisle.PROOFS.Timing_Proof]S
Second [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]START_a4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
START_t [in Fairisle.Fairisle.PROOFS.Timing_Proof]
START_p [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
START_A [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
S_cons [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
T
Third [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]TRIGGER_A [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
triplet [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
W
WAIT_a4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]WAIT_t [in Fairisle.Fairisle.PROOFS.Timing_Proof]
WAIT_BEGIN_A [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Axiom Index
I
Invariant_relation_p [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]Inductive Index
D
d_list [in Fairisle.Libraries.Lib_Lists.Dependent_lists]E
EqS [in Fairisle.Libraries.Lib_Lists.Infinite_lists]eq_dlist_of_Stream [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Even [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
even [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
I
Inv [in Fairisle.Libraries.Lib_Automata.Mealy]Inv_P_Timing [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
L
label_a4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]label_t [in Fairisle.Fairisle.PROOFS.Timing_Proof]
label_p [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
label_A [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
N
nth_spec [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]O
Odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]odd [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
order [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
Or3 [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
or3 [in Fairisle.Libraries.Lib_Basis.Lib_Prop]
P
prod_3 [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]S
state_id [in Fairisle.Libraries.Lib_Automata.Identity]Stream [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
T
True' [in Fairisle.Libraries.Lib_Automata.Mealy]Section Index
A
Additional_Def_and_Lemmas [in Fairisle.Libraries.Lib_Lists.dlist_Compl]Arbitration_Structure [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Arbitration_Structure [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Arbitration_Correctness [in Fairisle.Fairisle.PROOFS.Arbitration_Proof]
Arbitration_between_several_inputs [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
Arbitration_Specification [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Arbitration_beh [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
D
Definitions_and_lemmas_about_ports [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]Dependent_lists [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_Lists_Compl [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
E
Equivalence_2_Mealy [in Fairisle.Libraries.Lib_Automata.Mealy]Equivalence_Mealy_to_Moore2 [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy2 [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Mealy_to_Moore1 [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equivalence_Moore_to_Mealy1 [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Equiv_on_rule_SC [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_on_rule_PC [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Equiv_about_P [in Fairisle.Libraries.Lib_Automata.Mealy]
F
Feedback_Composition [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]Filter_and_Pick [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
fixed_lists [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
For_ltReq [in Fairisle.Fairisle.PROOFS.Invariant_a4_S]
Four_Arbiters_Specif [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Four_Arbiters_Proof_Correctness [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
From_init_states [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
I
Identity [in Fairisle.Libraries.Lib_Automata.Identity]Identity_and_TimingPDecode [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Identity_and_TimingPDecode [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Identity_and_TimingPDecode_beh [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Infinite_List [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
M
Mealy_Description [in Fairisle.Libraries.Lib_Automata.Mealy]Moore_Description [in Fairisle.Libraries.Lib_Automata.Moore]
O
output_is_identity [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]P
Parallel_Composition [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]Particular_Parallel_Composition [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Ports [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.TypePorts]
PriorityDecode_Correctness [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
programming_3 [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
Projections_on_fixed_dlists [in Fairisle.Libraries.Lib_Lists.Proj_lists]
R
Round_Robin_function [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]S
Series_Composition [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]Struct_Beh_Arbitration [in Fairisle.Fairisle.PROOFS.Equiv_Struct_Beh_Arbitration]
Successor_Modulo_NbPorts [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
T
Tests_in_dlists [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]Timing_and_PDecode [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Timing_Correctness [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Timing_and_PDecode [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Timing_Arbiter_Proof [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
Timing_and_PDecode_beh [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Tool_about_Lemma_on_rules [in Fairisle.Libraries.Lib_Automata.Lemmas_on_Basic_rules]
Tool_about_Equivalence_2_Mealy [in Fairisle.Libraries.Lib_Automata.Mealy]
Transformation [in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
V
Verif_hyp [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]Abbreviation Index
A
A1A2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]C
C_Inp [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]E
eight [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]Exist [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
F
five [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]four [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
Fst_3 [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
I
If [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]O
one [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]S
seven [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]six [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
Snd_3 [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
States_A1A2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
S_Snd [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Fst [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S1S1 [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
T
Thd_3 [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]three [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
Triplet [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
two [in Fairisle.Libraries.Lib_Arithmetic.Syntactic_Def]
Two_List2_List4 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Definition Index
A
Ack [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]Ackgen [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
ackgen [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Ackgen_4 [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Ackgen_n [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Ackgen_Behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
Ackor [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
Ackor_4 [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Ackor_n [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Ack_Behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
Ack_behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
ack_behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
active_bits [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
act_bits [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
all_True [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
all_False [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
all_same [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
All_Thd_of_l3 [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
All_Scd_of_l3 [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
All_Fst_of_l3 [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
All_Ports [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
ANDL [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
ANDL3 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
ANDL4 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
AND2 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
AND3 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
AND4 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
AO [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
ARBITER_XY_Behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp_Behaviour]
Arbiter_Y_behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
Arbiter_X_behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
Arbx [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Arby [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Arb_xel [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Arb_yel [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
At_least_one_of_2_active [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
A1A2 [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
B
BehaviourSC_ARBITRATION [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]Behaviour_FOUR_ARBITERS [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Behaviour_TIMING [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Behaviour_PRIORITY_DECODE [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Behaviour_IDENTITY [in Fairisle.Libraries.Lib_Automata.Identity]
Behaviour_ARBITRATION [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Behaviour_TIMINGPDECODE_ID [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Behaviour_TIMING_PDECODE [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
bool_to_nat [in Fairisle.Libraries.Lib_Lists.Conversions]
bool_nat [in Fairisle.Libraries.Lib_Lists.Conversions]
C
Compact [in Fairisle.Libraries.Lib_Lists.Infinite_lists]Compact_dlist [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
comparison [in Fairisle.Libraries.Lib_Arithmetic.Compare_Nat]
construct_with_i_last [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
construct_with_i_first [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Convert_list2_port [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Convert_port_list2_ter [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Convert_port_list2_bis [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Convert_port_list2 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
Convert_and_filter [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Convert_list2_nat [in Fairisle.Libraries.Lib_Lists.Conversions]
Convert_list2 [in Fairisle.Libraries.Lib_Lists.Conversions]
D
DATASWITCHC [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]DATASWITCHC_AUX [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
DATASWITCH_N [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
DATASWITCH_N_AUX [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Decode [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Decode_4 [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Decode_n [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
DFFd [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
DFFRD [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
DFFrd [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
div [in Fairisle.Libraries.Lib_Arithmetic.Lib_Div_Even_Odd]
dlist_to_Stream [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
dlist_List [in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
dmap_Stream_to_dlist [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
dmap_dlist_to_Stream [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
DMUX2B4CA11 [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
DMUX2B4CA11_AUX [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
DMUX4T2 [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Dmux4t2 [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
DMUX4T2FFC [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
dmux4t2ffc [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
DMUX4T2FFC_Behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp_Behaviour]
DMUX4T2FFC_AUX [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Dmux4t2ffc_Behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
Dmux4t2ffc_Behaviour' [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
d_In [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
d_map4 [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_map3 [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_map2 [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_map [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_Hd [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_tl [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_Head [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_head [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_hd [in Fairisle.Libraries.Lib_Lists.Dependent_lists]
d_Map_List2_pdt_Grant [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
d_Map_List4_pdt_Grant [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof_lemmas]
E
eq_d_list [in Fairisle.Libraries.Lib_Lists.Dependent_lists]exists1_exact [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
exists1_atleast [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
Exists1_atleast [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
exp_n [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
exp_2 [in Fairisle.Libraries.Lib_Arithmetic.Lib_Exp]
F
factorial [in Fairisle.Libraries.Lib_Arithmetic.Lib_Fact]FC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
first_of_list [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Fold_List [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
fold_with_f [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Fold_with_f_S [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Fold_with_f_S_p [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Fold_with_f [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
Freg [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Freg2 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Fst_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
Fst_of_l3 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
Fst_of_l2 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
Fth_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
f_four_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
f_two_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
f_arbiter [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
f_four_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
f_two_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
f_arbiter [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
f_tp [in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
f_tpi [in Fairisle.Fairisle.PROOFS.Lemmas_for_Arbitration]
G
genReq [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]Genreq [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Grant [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
grant [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
Grant_for_Out [in Fairisle.Fairisle.PROOFS.Lemmas_Comb_Behaviour]
Grant' [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
grant' [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
H
hds [in Fairisle.Libraries.Lib_Lists.Infinite_lists]hiReq [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Hireq [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
I
IBUF [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]ifProp [in Fairisle.Libraries.Lib_Basis.Lib_Set_Products]
if_bool [in Fairisle.Libraries.Lib_Boolean.Lib_Bool]
Ilatch [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
ILATCH [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
INFFd [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
Inj1 [in Fairisle.Libraries.Lib_Basis.Injections]
Inj2 [in Fairisle.Libraries.Lib_Basis.Injections]
INV [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
Inv_under_P [in Fairisle.Libraries.Lib_Automata.Mealy]
Inv_t_a4 [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
In_latch [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
In_Buf [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
IN_LATCH [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
IN_BUF [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
J
Jk [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]JkE [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
JKFFce [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
JKFF_qBar [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
JKFF_q [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
J_Arby [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
K
K_Arby [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]L
last_of_list [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]Latch [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
LATCH [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
list_of_seg [in Fairisle.Libraries.Lib_Lists.Lists_of_lists]
list_of_nth [in Fairisle.Libraries.Lib_Lists.Lists_of_lists]
list_of_tails [in Fairisle.Libraries.Lib_Lists.Lists_of_lists]
list_of_heads [in Fairisle.Libraries.Lib_Lists.Lists_of_lists]
list_no_port_bool [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
list_of_segment [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
List_of_scd_of_l2 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
List_of_tails_of_l2 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
List_of_fst_of_l2 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
list_dlist [in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
List_dlist [in Fairisle.Libraries.Lib_Lists.PolyList_dlist]
List2 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List2_pdt [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List3 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List4 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
List4_transf [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Loop [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Loop2 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Loop3 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Loop3_permut [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
l2_tt [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l2_tf [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l2_ft [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l2_ff [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ftff [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_fftf [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tfff [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ffft [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tttt [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tfft [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_fttf [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tttf [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ttft [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ttff [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tftt [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_tftf [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_fttt [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ftft [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_fftt [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
l4_ffff [in Fairisle.Libraries.Lib_Lists.Manip_BoolLists]
M
make_list_of_v [in Fairisle.Libraries.Lib_Lists.dlist_Compl]MAP_map_g [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
MAP_g [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
Mealy [in Fairisle.Libraries.Lib_Automata.Mealy]
merge [in Fairisle.Libraries.Lib_Lists.Lists_of_lists]
Moore [in Fairisle.Libraries.Lib_Automata.Moore]
N
NAND2 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]NAND3 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
NAND4 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
nat_bool [in Fairisle.Libraries.Lib_Lists.Conversions]
NORL [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
NORL3 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
NOR2 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
NOR3 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
NOR4 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
No_Inv [in Fairisle.Libraries.Lib_Automata.Mealy]
No_P [in Fairisle.Libraries.Lib_Automata.Mealy]
no_in [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
no_out [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
nth [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Nth [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Nth_func [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
number_P [in Fairisle.Libraries.Lib_Lists.Tests_in_d_lists]
NXOR2 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
NXOR3 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
NXOR4 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
O
OBUF [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]Olatch [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
OLATCH [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
OR2 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
OR3 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
OR4 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
outdis [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
OUTDIS_Behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp_Behaviour]
Outdis_behaviour [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb_Behaviour]
OUTFFd [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates_Del]
OutPC_TimingPDecode_Id [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
OutPC_Timing_PDecode [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
OutPC_arbiter [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
OutPC_TimingPDecode_Id [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OutPC_Timing_PDecode [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OutPC_arbiter [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OutputDisable [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
OutputDisable' [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
outputDisable' [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
Output_requested [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
output_four_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
output_two_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
output_arbiter [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Output_rel [in Fairisle.Libraries.Lib_Automata.Mealy]
output_four_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
output_two_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
output_arbiter [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OutSC_Arbitration [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
OutSC_Arbitration [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OutSC_Arbitration_beh [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Out_latch [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
Out_Buf [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
Out_PC_part [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Out_Four_Arbiters_Mealy [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Out_Four_Arbiters [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Out_priority_decode [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_Struct_four_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_Struct_two_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_ArbiterXY [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_outdis [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_Struct_Timing [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Out_FC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Out_SC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Out_PC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Out_Timing_Mealy [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Out_Timing [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Out_priority_decode [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Out_Struct_four_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Out_Struct_two_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Out_ArbiterXY [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Out_outdis [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Out_Struct_Timing [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
OUT_LATCH [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
OUT_BUF [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
Out_PriorityDecode_Mealy [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Out_PriorityDecode [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Out_id [in Fairisle.Libraries.Lib_Automata.Identity]
Out_Arbitration_Mealy [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Out_Arbitration [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Out_Mealy [in Fairisle.Libraries.Lib_Automata.Moore_Mealy]
Out_TimingPDecode_Id [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Out_Timing_PDecode [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
P
Pause [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]PAUSE [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
PC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
PC_part [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Pdt_List4_List3 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
pdt_List2 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
PickSuccessfulInput [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Prifilunit [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Prifil4clb [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
PriorityRequests [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PickSuccessfulInput]
Priority_Decode_Less_Pause [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Priority_4 [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
priority_bits [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
pri_bits [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
proof_in [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
proof_out [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.PortsCompl]
put_end [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
P_a4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
P_Timing [in Fairisle.Fairisle.PROOFS.Timing_Arbiter]
P_A [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
R
Reg [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]Regf [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gen_Gates_Del]
Remove_i [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
remove_i [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
RequestsToArbitrate [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
Rev [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Rlatch [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
rlatch [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
RLATCH [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Base_Struct]
RLATCH2 [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
RoundRobin [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
RoundRobinArbiter [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.RoundRobin]
route_bits [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
rou_bits [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
R_a4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
R_Timing [in Fairisle.Fairisle.PROOFS.Timing_Proof]
R_Priority_Decode [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
R_A [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
S
SC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]Scd_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
Scd_of_l3 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
Scd_of_l2 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
seg [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Seg [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Segment [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
segment [in Fairisle.Libraries.Lib_Lists.dlist_Compl]
seg' [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Seg' [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
sig_true [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
sig_false [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
SM4 [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.Lemmas_on_fcts]
Square [in Fairisle.Libraries.Lib_Arithmetic.Lib_Square]
StatesSC_ARBITRATION [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
StatesSC_ARBITRATION [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
States_PC_part [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
States_FOUR_ARBITERS [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
States_TIMINGPDECODE_ID [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
States_TIMING_PDECODE [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
States_Mealy [in Fairisle.Libraries.Lib_Automata.Mealy]
States_FC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
States_SC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
States_PC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
States_Structure_TIMING [in Fairisle.Fairisle.PROOFS.Timing_Proof]
States_TIMING [in Fairisle.Fairisle.PROOFS.Timing_Proof]
States_TIMINGPDECODE_ID [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
States_TIMING_PDECODE [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
States_Structure_PRIORITY_DECODE [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
States_PRIORITY_DECODE [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
States_IDENTITY [in Fairisle.Libraries.Lib_Automata.Identity]
States_ARBITRATION [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
States_Beh_SC_ARBITRATION [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
States_Beh_TIMINGPDECODE_ID [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
States_Beh_TIMING_PDECODE [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
STATE_a4 [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
STATE_p [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
STATE_A [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Stream_to_dlist [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
strip_off_last [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
strip_off_first [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
Structure_ARBITRATION [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_TIMINGPDECODE_ID [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_TIMING_PDECODE [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_PRIORITY_DECODE [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_FOUR_ARBITERS [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_TWO_ARBITERS [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_ARBITER [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_ArbiterXY [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_Outdis [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_TIMING [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Structure_ARBITRATION [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_TIMINGPDECODE_ID [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_TIMING_PDECODE [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_PRIORITY_DECODE [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_FOUR_ARBITERS [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_TWO_ARBITERS [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_ARBITER [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_ArbiterXY [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_Outdis [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_TIMING [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Structure_States_FOUR_ARBITERS [in Fairisle.Fairisle.PROOFS.Arbiter4_Proof]
subst [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
SuccessfulInput [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]
SUC_MODN [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.NextPort]
S_Two_Fst [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Snd_pdt [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Fst_pdt [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Fth_of_4 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Thd_of_4 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Snd_of_4 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Thd_of_3 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Snd_of_3 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_list_of_seg [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_list_of_nth [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Fold_List [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Unfold_List [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Remove_i [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Seg [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Nth [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_tls [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_hds [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map4 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map3 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map2 [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_map [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_tail [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_head [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
S_Ackor [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
S_three_fst_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_List_of_scd_of_l2 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_List_of_tails_of_l2 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_List_of_fst_of_l2 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Fth_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Thd_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Scd_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Fst_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Scd_of_l2 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
S_Fst_of_l2 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
T
test_port [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.SuccessfulInput]Thd_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
Thd_of_l3 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
three_fst_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
Timing [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementComb]
Timing_Aux [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Timing_Aux [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
tls [in Fairisle.Libraries.Lib_Lists.Infinite_lists]
transf [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf_List4_List3 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf1 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf2 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf3 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
transf4 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
TransPC_TimingPDecode_Id [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
TransPC_Timing_PDecode [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
TransPC_arbiter [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
TransPC_TimingPDecode_Id [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
TransPC_Timing_PDecode [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
TransPC_arbiter [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
TransSC_Arbitration [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
TransSC_Arbitration [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
TransSC_Arbitration_beh [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Trans_PC_part [in Fairisle.Libraries.Lib_Automata.Derived_composition_rules]
Trans_Four_Arbiters [in Fairisle.Fairisle.PROOFS.Arbiter4_Specif]
Trans_priority_decode [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Trans_Struct_four_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Trans_Struct_two_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Trans_ArbiterXY [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Trans_outdis [in Fairisle.Fairisle.SPECIF.ELEMENT.Arbitration]
Trans_FC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Trans_SC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Trans_PC [in Fairisle.Libraries.Lib_Automata.Basic_composition_rules]
Trans_Timing [in Fairisle.Fairisle.PROOFS.Timing_Proof]
Trans_priority_decode [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Trans_Struct_four_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Trans_Struct_two_arbiters [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Trans_ArbiterXY [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Trans_outdis [in Fairisle.Fairisle.SPECIF.ELEMENT.ElementTemp]
Trans_PriorityDecode [in Fairisle.Fairisle.PROOFS.PriorityDecode_Proof]
Trans_id [in Fairisle.Libraries.Lib_Automata.Identity]
Trans_Arbitration [in Fairisle.Fairisle.PROOFS.Arbitration_Specif]
Trans_TimingPDecode_Id [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Trans_Timing_PDecode [in Fairisle.Fairisle.PROOFS.Arbitration_beh_sc]
Two_last_of_l3 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Two_fst_of_l3 [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Two_last_of_l4' [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Two_Fst_of_l4' [in Fairisle.Libraries.Lib_Lists.Fixed_dLists]
Two_last_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
Two_Fst_of_l4 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
two_fst_of_l3 [in Fairisle.Libraries.Lib_Lists.Proj_lists]
T_Outportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.TypePorts]
T_Inportno [in Fairisle.Fairisle.SPECIF.ROUND_ROBIN.TypePorts]
U
UnCompact [in Fairisle.Libraries.Lib_Lists.Infinite_lists]Unfold_List [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]
W
wcat [in Fairisle.Libraries.Lib_Lists.Dependent_lists_Compl]Wire [in Fairisle.Fairisle.SPECIF.ELEMENT.Base_Behaviour]
Wire_bool [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
X
xGrant' [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]Xnor [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
Xor [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
XOR2 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
XOR3 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
XOR4 [in Fairisle.Fairisle.SPECIF.GATES_AND_LATCHES.Gates]
x_Grant' [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
x_Grant [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
Y
yGrant' [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]y_Grant' [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
y_Grant [in Fairisle.Fairisle.SPECIF.ELEMENT.Tools_Inf]
Z
zeros [in Fairisle.Libraries.Lib_Lists.Infinite_lists]| 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 | (1518 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 | (358 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 | (71 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 | (460 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 | (39 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 | (1 entry) |
| 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 | (21 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 | (53 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 | (21 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 | (494 entries) |