| 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 | (641 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 | (368 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 | (10 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 | (127 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 | (7 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 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 | (54 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 | (62 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
Global Index
A
Acc_clos_trans [lemma, in WeakUpTo.Relations]antisymmetric [definition, in WeakUpTo.Relations]
Applications [library]
B
bicontrolled [definition, in WeakUpTo.Settings]bisim [definition, in WeakUpTo.Settings]
bisimulation [definition, in WeakUpTo.Settings]
bisimulation_comp [lemma, in WeakUpTo.Settings]
bisimulation_bisim [lemma, in WeakUpTo.Settings]
bisim_trans [lemma, in WeakUpTo.Settings]
bisim_refl [lemma, in WeakUpTo.Settings]
bisim_sym [lemma, in WeakUpTo.Settings]
C
Chain [definition, in WeakUpTo.Functions]chaing_l_wmon [lemma, in WeakUpTo.WeakMonotonic]
Chaining_wmon [lemma, in WeakUpTo.WeakMonotonic]
chaining_r [definition, in WeakUpTo.Functions]
chaining_l [definition, in WeakUpTo.Functions]
chaining_l_mon [lemma, in WeakUpTo.Monotonic]
chaining_r_mon [lemma, in WeakUpTo.Monotonic]
commute [definition, in WeakUpTo.Diagrams]
comp [definition, in WeakUpTo.Relations]
Comp [definition, in WeakUpTo.Functions]
Compose [section, in WeakUpTo.Diagrams]
Compose.H1 [variable, in WeakUpTo.Diagrams]
Compose.H2 [variable, in WeakUpTo.Diagrams]
Compose.RX [variable, in WeakUpTo.Diagrams]
Compose.RY [variable, in WeakUpTo.Diagrams]
Compose.RZ [variable, in WeakUpTo.Diagrams]
Compose.R1 [variable, in WeakUpTo.Diagrams]
Compose.R2 [variable, in WeakUpTo.Diagrams]
Compose.S1 [variable, in WeakUpTo.Diagrams]
Compose.S2 [variable, in WeakUpTo.Diagrams]
Compose.X [variable, in WeakUpTo.Diagrams]
Compose.X' [variable, in WeakUpTo.Diagrams]
Compose.Y [variable, in WeakUpTo.Diagrams]
Compose.Y' [variable, in WeakUpTo.Diagrams]
Compose.Z [variable, in WeakUpTo.Diagrams]
Compose.Z' [variable, in WeakUpTo.Diagrams]
Comp_wmon [lemma, in WeakUpTo.WeakMonotonic]
comp_star_plus [lemma, in WeakUpTo.Relations]
comp_plus_star [lemma, in WeakUpTo.Relations]
comp_star_star [lemma, in WeakUpTo.Relations]
comp_assoc [lemma, in WeakUpTo.Relations]
comp_eeq [lemma, in WeakUpTo.Relations]
comp_incl [lemma, in WeakUpTo.Relations]
Comp_mon [lemma, in WeakUpTo.Monotonic]
confluent [definition, in WeakUpTo.Diagrams]
constant [definition, in WeakUpTo.Functions]
constant_mon [lemma, in WeakUpTo.Monotonic]
contains [definition, in WeakUpTo.Functions]
Controlled [section, in WeakUpTo.Applications]
controlled [record, in WeakUpTo.Settings]
Controlled [library]
controlled_correct [lemma, in WeakUpTo.Theory]
Controlled.A [variable, in WeakUpTo.Applications]
Controlled.B [variable, in WeakUpTo.Applications]
Controlled.BG [variable, in WeakUpTo.Applications]
Controlled.B' [variable, in WeakUpTo.Applications]
Controlled.B'G [variable, in WeakUpTo.Applications]
Controlled.F [variable, in WeakUpTo.Applications]
Controlled.FG [variable, in WeakUpTo.Applications]
Controlled.F_mon [variable, in WeakUpTo.Applications]
Controlled.G [variable, in WeakUpTo.Applications]
Controlled.HB [variable, in WeakUpTo.Applications]
Controlled.HB' [variable, in WeakUpTo.Applications]
Controlled.HRa [variable, in WeakUpTo.Applications]
Controlled.HRa' [variable, in WeakUpTo.Applications]
Controlled.HRt [variable, in WeakUpTo.Applications]
Controlled.HRt' [variable, in WeakUpTo.Applications]
Controlled.R [variable, in WeakUpTo.Applications]
Controlled.TX [variable, in WeakUpTo.Applications]
Controlled.X [variable, in WeakUpTo.Applications]
ctrl_a [projection, in WeakUpTo.Settings]
ctrl_t [projection, in WeakUpTo.Settings]
D
Definitions [section, in WeakUpTo.Relations]Definitions.R [variable, in WeakUpTo.Relations]
Definitions.X [variable, in WeakUpTo.Relations]
Definitions.Y [variable, in WeakUpTo.Relations]
Definitions.Z [variable, in WeakUpTo.Relations]
Def1 [section, in WeakUpTo.Diagrams]
Def1.R [variable, in WeakUpTo.Diagrams]
Def1.RX [variable, in WeakUpTo.Diagrams]
Def1.RY [variable, in WeakUpTo.Diagrams]
Def1.R' [variable, in WeakUpTo.Diagrams]
Def1.X [variable, in WeakUpTo.Diagrams]
Def1.X' [variable, in WeakUpTo.Diagrams]
Def1.Y [variable, in WeakUpTo.Diagrams]
Def1.Y' [variable, in WeakUpTo.Diagrams]
Def2 [section, in WeakUpTo.Diagrams]
Def2.R [variable, in WeakUpTo.Diagrams]
Def2.S [variable, in WeakUpTo.Diagrams]
Def2.X [variable, in WeakUpTo.Diagrams]
diagram [definition, in WeakUpTo.Diagrams]
Diagrams [library]
diagram_star_wf [lemma, in WeakUpTo.Diagrams]
diagram_star_wf_2 [lemma, in WeakUpTo.Diagrams]
diagram_star_wf_1 [lemma, in WeakUpTo.Diagrams]
diagram_plus_wf_2 [lemma, in WeakUpTo.Diagrams]
diagram_plus_wf_1 [lemma, in WeakUpTo.Diagrams]
diagram_plus_wf [lemma, in WeakUpTo.Diagrams]
diagram_plus [lemma, in WeakUpTo.Diagrams]
diagram_star [lemma, in WeakUpTo.Diagrams]
diagram_union [lemma, in WeakUpTo.Diagrams]
diagram_comp [lemma, in WeakUpTo.Diagrams]
diagram_reverse [lemma, in WeakUpTo.Diagrams]
diagram_incl [lemma, in WeakUpTo.Diagrams]
diagram_r [definition, in WeakUpTo.Reductions]
E
eeq [definition, in WeakUpTo.Relations]eeq_sym [lemma, in WeakUpTo.Relations]
eeq_trans [lemma, in WeakUpTo.Relations]
eeq_refl [lemma, in WeakUpTo.Relations]
eeq_r [definition, in WeakUpTo.Reductions]
Eeq1 [section, in WeakUpTo.Relations]
Eeq1.F [variable, in WeakUpTo.Relations]
Eeq1.F' [variable, in WeakUpTo.Relations]
Eeq1.I [variable, in WeakUpTo.Relations]
Eeq1.R [variable, in WeakUpTo.Relations]
Eeq1.R' [variable, in WeakUpTo.Relations]
Eeq1.R1 [variable, in WeakUpTo.Relations]
Eeq1.R1' [variable, in WeakUpTo.Relations]
Eeq1.S [variable, in WeakUpTo.Relations]
Eeq1.S' [variable, in WeakUpTo.Relations]
Eeq1.T [variable, in WeakUpTo.Relations]
Eeq1.T' [variable, in WeakUpTo.Relations]
Eeq1.X [variable, in WeakUpTo.Relations]
Eeq1.Y [variable, in WeakUpTo.Relations]
Eeq1.Z [variable, in WeakUpTo.Relations]
Eeq2 [section, in WeakUpTo.Relations]
Eeq2.F [variable, in WeakUpTo.Relations]
Eeq2.I [variable, in WeakUpTo.Relations]
Eeq2.R [variable, in WeakUpTo.Relations]
Eeq2.R' [variable, in WeakUpTo.Relations]
Eeq2.S [variable, in WeakUpTo.Relations]
Eeq2.T [variable, in WeakUpTo.Relations]
Eeq2.X [variable, in WeakUpTo.Relations]
Eeq2.Y [variable, in WeakUpTo.Relations]
Eeq2.Z [variable, in WeakUpTo.Relations]
eta2 [definition, in WeakUpTo.Relations]
evolve [definition, in WeakUpTo.Settings]
evolve_incl [lemma, in WeakUpTo.Settings]
evolve_union [lemma, in WeakUpTo.Settings]
evolve_a [definition, in WeakUpTo.Settings]
evolve_t [definition, in WeakUpTo.Settings]
evolve_1 [definition, in WeakUpTo.Settings]
EWeak [definition, in WeakUpTo.Reductions]
Exp [definition, in WeakUpTo.Functions]
expand [definition, in WeakUpTo.Settings]
expand_trans [lemma, in WeakUpTo.Settings]
expand_refl [lemma, in WeakUpTo.Settings]
expand_wexpand [lemma, in WeakUpTo.Settings]
expansion [definition, in WeakUpTo.Settings]
expansion_comp [lemma, in WeakUpTo.Settings]
expansion_expand [lemma, in WeakUpTo.Settings]
expansion1 [definition, in WeakUpTo.Settings]
expansion1_comp [lemma, in WeakUpTo.Settings]
F
FG [lemma, in WeakUpTo.Applications]function [definition, in WeakUpTo.Functions]
Functions [library]
function2 [definition, in WeakUpTo.Functions]
F_mon [lemma, in WeakUpTo.Applications]
G
Global [section, in WeakUpTo.WeakMonotonic]Global [section, in WeakUpTo.Theory]
Global [section, in WeakUpTo.Functions]
Global [section, in WeakUpTo.Monotonic]
Global [section, in WeakUpTo.Settings]
Global.A [section, in WeakUpTo.WeakMonotonic]
Global.A [variable, in WeakUpTo.WeakMonotonic]
Global.A [variable, in WeakUpTo.Theory]
Global.A [section, in WeakUpTo.Monotonic]
Global.A [variable, in WeakUpTo.Monotonic]
Global.A [variable, in WeakUpTo.Settings]
Global.A.A' [section, in WeakUpTo.Monotonic]
Global.A.A'.E [variable, in WeakUpTo.Monotonic]
Global.A.A'.R [variable, in WeakUpTo.Monotonic]
Global.A.A'.T [variable, in WeakUpTo.Monotonic]
Global.A.F [variable, in WeakUpTo.WeakMonotonic]
Global.A.F [variable, in WeakUpTo.Monotonic]
Global.A.G [variable, in WeakUpTo.WeakMonotonic]
Global.A.G [variable, in WeakUpTo.Monotonic]
Global.A.HF [variable, in WeakUpTo.WeakMonotonic]
Global.A.HF [variable, in WeakUpTo.Monotonic]
Global.A.HG [variable, in WeakUpTo.WeakMonotonic]
Global.A.HG [variable, in WeakUpTo.Monotonic]
Global.A.TX [variable, in WeakUpTo.WeakMonotonic]
Global.A.TX [variable, in WeakUpTo.Monotonic]
Global.A.TY [variable, in WeakUpTo.WeakMonotonic]
Global.A.TY [variable, in WeakUpTo.Monotonic]
Global.A.Union [section, in WeakUpTo.WeakMonotonic]
Global.A.Union [section, in WeakUpTo.Monotonic]
Global.A.Union.H [variable, in WeakUpTo.WeakMonotonic]
Global.A.Union.H [variable, in WeakUpTo.Monotonic]
Global.A.Union.HH [variable, in WeakUpTo.WeakMonotonic]
Global.A.Union.HH [variable, in WeakUpTo.Monotonic]
Global.A.Union.I [variable, in WeakUpTo.WeakMonotonic]
Global.A.Union.I [variable, in WeakUpTo.Monotonic]
Global.A.X [variable, in WeakUpTo.WeakMonotonic]
Global.A.X [variable, in WeakUpTo.Monotonic]
Global.A.Y [variable, in WeakUpTo.WeakMonotonic]
Global.A.Y [variable, in WeakUpTo.Monotonic]
Global.B [section, in WeakUpTo.WeakMonotonic]
Global.B [section, in WeakUpTo.Monotonic]
Global.Bi [section, in WeakUpTo.Settings]
Global.BiComposition [section, in WeakUpTo.Settings]
Global.BiComposition.R [variable, in WeakUpTo.Settings]
Global.BiComposition.S [variable, in WeakUpTo.Settings]
Global.BiComposition.TX [variable, in WeakUpTo.Settings]
Global.BiComposition.TY [variable, in WeakUpTo.Settings]
Global.BiComposition.TZ [variable, in WeakUpTo.Settings]
Global.BiComposition.X [variable, in WeakUpTo.Settings]
Global.BiComposition.Y [variable, in WeakUpTo.Settings]
Global.BiComposition.Z [variable, in WeakUpTo.Settings]
Global.Bi.TX [variable, in WeakUpTo.Settings]
Global.Bi.TY [variable, in WeakUpTo.Settings]
Global.Bi.X [variable, in WeakUpTo.Settings]
Global.Bi.Y [variable, in WeakUpTo.Settings]
Global.B.F [variable, in WeakUpTo.WeakMonotonic]
Global.B.F [variable, in WeakUpTo.Monotonic]
Global.B.G [variable, in WeakUpTo.WeakMonotonic]
Global.B.G [variable, in WeakUpTo.Monotonic]
Global.B.HF [variable, in WeakUpTo.WeakMonotonic]
Global.B.HF [variable, in WeakUpTo.Monotonic]
Global.B.HG [variable, in WeakUpTo.WeakMonotonic]
Global.B.HG [variable, in WeakUpTo.Monotonic]
Global.B.TX [variable, in WeakUpTo.WeakMonotonic]
Global.B.TX [variable, in WeakUpTo.Monotonic]
Global.B.TY [variable, in WeakUpTo.WeakMonotonic]
Global.B.TY [variable, in WeakUpTo.Monotonic]
Global.B.X [variable, in WeakUpTo.WeakMonotonic]
Global.B.X [variable, in WeakUpTo.Monotonic]
Global.B.Y [variable, in WeakUpTo.WeakMonotonic]
Global.B.Y [variable, in WeakUpTo.Monotonic]
Global.C [section, in WeakUpTo.WeakMonotonic]
Global.Composition [section, in WeakUpTo.Settings]
Global.Composition.R [variable, in WeakUpTo.Settings]
Global.Composition.S [variable, in WeakUpTo.Settings]
Global.Composition.TX [variable, in WeakUpTo.Settings]
Global.Composition.TY [variable, in WeakUpTo.Settings]
Global.Composition.TZ [variable, in WeakUpTo.Settings]
Global.Composition.wexpansion1_t [variable, in WeakUpTo.Settings]
Global.Composition.X [variable, in WeakUpTo.Settings]
Global.Composition.Y [variable, in WeakUpTo.Settings]
Global.Composition.Z [variable, in WeakUpTo.Settings]
Global.ControlledCorrect [section, in WeakUpTo.Theory]
Global.ControlledCorrect.B [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.F [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.G [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HB [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HBF [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HBG [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HBGGn [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HF [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HFG [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HFGn [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HG [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HGGBF [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HRa [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.HRt [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.pre_visible [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.pre_silent [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.R [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.silent [variable, in WeakUpTo.Theory]
Global.ControlledCorrect.visible [variable, in WeakUpTo.Theory]
Global.C.F [variable, in WeakUpTo.WeakMonotonic]
Global.C.G [variable, in WeakUpTo.WeakMonotonic]
Global.C.HF [variable, in WeakUpTo.WeakMonotonic]
Global.C.HG [variable, in WeakUpTo.WeakMonotonic]
Global.C.HL [variable, in WeakUpTo.WeakMonotonic]
Global.C.L [variable, in WeakUpTo.WeakMonotonic]
Global.C.TX [variable, in WeakUpTo.WeakMonotonic]
Global.C.TY [variable, in WeakUpTo.WeakMonotonic]
Global.C.X [variable, in WeakUpTo.WeakMonotonic]
Global.C.Y [variable, in WeakUpTo.WeakMonotonic]
Global.Def [section, in WeakUpTo.Functions]
Global.Def' [section, in WeakUpTo.Functions]
Global.Def'.F [variable, in WeakUpTo.Functions]
Global.Def'.R [variable, in WeakUpTo.Functions]
Global.Def'.X [variable, in WeakUpTo.Functions]
Global.Def'.X' [variable, in WeakUpTo.Functions]
Global.Def'.X'' [variable, in WeakUpTo.Functions]
Global.Def'.Y [variable, in WeakUpTo.Functions]
Global.Def'.Y' [variable, in WeakUpTo.Functions]
Global.Def'.Y'' [variable, in WeakUpTo.Functions]
Global.Def'.Z [variable, in WeakUpTo.Functions]
Global.Def'.Z' [variable, in WeakUpTo.Functions]
Global.Def.X [variable, in WeakUpTo.Functions]
Global.Def.X' [variable, in WeakUpTo.Functions]
Global.Def.Y [variable, in WeakUpTo.Functions]
Global.Def.Y' [variable, in WeakUpTo.Functions]
Global.MonotonicCorrect [section, in WeakUpTo.Theory]
Global.MonotonicCorrect.F [variable, in WeakUpTo.Theory]
Global.MonotonicCorrect.HF [variable, in WeakUpTo.Theory]
Global.MonotonicCorrect.HR [variable, in WeakUpTo.Theory]
Global.MonotonicCorrect.phi [variable, in WeakUpTo.Theory]
Global.MonotonicCorrect.R [variable, in WeakUpTo.Theory]
Global.Properties [section, in WeakUpTo.Settings]
Global.Properties.TX [variable, in WeakUpTo.Settings]
Global.Properties.X [variable, in WeakUpTo.Settings]
Global.Sim [section, in WeakUpTo.Settings]
Global.Sim.B [variable, in WeakUpTo.Settings]
Global.Sim.F [variable, in WeakUpTo.Settings]
Global.Sim.TX [variable, in WeakUpTo.Settings]
Global.Sim.TY [variable, in WeakUpTo.Settings]
Global.Sim.X [variable, in WeakUpTo.Settings]
Global.Sim.Y [variable, in WeakUpTo.Settings]
Global.TX [variable, in WeakUpTo.Theory]
Global.TY [variable, in WeakUpTo.Theory]
Global.UIter [section, in WeakUpTo.Functions]
Global.UIter' [section, in WeakUpTo.Functions]
Global.UIter'.F [variable, in WeakUpTo.Functions]
Global.UIter'.HF [variable, in WeakUpTo.Functions]
Global.UIter'.HF' [variable, in WeakUpTo.Functions]
Global.UIter'.X [variable, in WeakUpTo.Functions]
Global.UIter.F [variable, in WeakUpTo.Functions]
Global.UIter.HF [variable, in WeakUpTo.Functions]
Global.UIter.HF0 [variable, in WeakUpTo.Functions]
Global.UIter.HF2 [variable, in WeakUpTo.Functions]
Global.UIter.X [variable, in WeakUpTo.Functions]
Global.UIter.Y [variable, in WeakUpTo.Functions]
Global.UnifiedCorrect [section, in WeakUpTo.Theory]
Global.UnifiedCorrect.F [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.G [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.HF [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.HFG [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.HFGn [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.HG [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.HGFG [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.HGFGn [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.HRa [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.HRt [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.pre_visible [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.pre_silent [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.R [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.silent [variable, in WeakUpTo.Theory]
Global.UnifiedCorrect.visible [variable, in WeakUpTo.Theory]
Global.WeakMonotonicCorrect [section, in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.F [variable, in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.HF [variable, in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.HRa [variable, in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.HRt [variable, in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.R [variable, in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.silent [variable, in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.visible [variable, in WeakUpTo.Theory]
Global.X [variable, in WeakUpTo.Theory]
Global.Y [variable, in WeakUpTo.Theory]
G_reverse [lemma, in WeakUpTo.Applications]
G_wmon [lemma, in WeakUpTo.Applications]
I
identity [definition, in WeakUpTo.Functions]identity_mon [lemma, in WeakUpTo.Monotonic]
incl [definition, in WeakUpTo.Relations]
Incl [section, in WeakUpTo.Diagrams]
InclEeq [section, in WeakUpTo.Relations]
InclEeq.R [variable, in WeakUpTo.Relations]
InclEeq.S [variable, in WeakUpTo.Relations]
InclEeq.T [variable, in WeakUpTo.Relations]
InclEeq.X [variable, in WeakUpTo.Relations]
InclEeq.Y [variable, in WeakUpTo.Relations]
incl_trans [lemma, in WeakUpTo.Relations]
incl_refl [lemma, in WeakUpTo.Relations]
incl_r [definition, in WeakUpTo.Reductions]
incl_evolve [lemma, in WeakUpTo.Settings]
Incl.H [variable, in WeakUpTo.Diagrams]
Incl.HR [variable, in WeakUpTo.Diagrams]
Incl.HS [variable, in WeakUpTo.Diagrams]
Incl.R [variable, in WeakUpTo.Diagrams]
Incl.RX [variable, in WeakUpTo.Diagrams]
Incl.RY [variable, in WeakUpTo.Diagrams]
Incl.R' [variable, in WeakUpTo.Diagrams]
Incl.S [variable, in WeakUpTo.Diagrams]
Incl.S' [variable, in WeakUpTo.Diagrams]
Incl.X [variable, in WeakUpTo.Diagrams]
Incl.X' [variable, in WeakUpTo.Diagrams]
Incl.Y [variable, in WeakUpTo.Diagrams]
Incl.Y' [variable, in WeakUpTo.Diagrams]
increasing [definition, in WeakUpTo.Functions]
inv_union2 [lemma, in WeakUpTo.Relations]
inv_plus [lemma, in WeakUpTo.Relations]
inv_star [lemma, in WeakUpTo.Relations]
inv_union [lemma, in WeakUpTo.Relations]
inv_comp [lemma, in WeakUpTo.Relations]
inv_inv [lemma, in WeakUpTo.Relations]
Iter [definition, in WeakUpTo.Functions]
L
L [constructor, in WeakUpTo.Reductions]Lbl [inductive, in WeakUpTo.Reductions]
local_commute [definition, in WeakUpTo.Diagrams]
M
mkctrl [constructor, in WeakUpTo.Settings]mkmon [constructor, in WeakUpTo.Settings]
mkwmon [constructor, in WeakUpTo.Settings]
Modular [section, in WeakUpTo.Applications]
Modular.A [variable, in WeakUpTo.Applications]
Modular.F [variable, in WeakUpTo.Applications]
Modular.G [variable, in WeakUpTo.Applications]
Modular.HRa [variable, in WeakUpTo.Applications]
Modular.HRa' [variable, in WeakUpTo.Applications]
Modular.HRt [variable, in WeakUpTo.Applications]
Modular.HRt' [variable, in WeakUpTo.Applications]
Modular.R [variable, in WeakUpTo.Applications]
Modular.TX [variable, in WeakUpTo.Applications]
Modular.X [variable, in WeakUpTo.Applications]
monotonic [record, in WeakUpTo.Settings]
Monotonic [library]
monotonic_wmonotonic [lemma, in WeakUpTo.WeakMonotonic]
monotonic_correct [lemma, in WeakUpTo.Theory]
mon_a [projection, in WeakUpTo.Settings]
mon_t [projection, in WeakUpTo.Settings]
mon_m [projection, in WeakUpTo.Settings]
O
Operators [section, in WeakUpTo.Relations]Operators.O [section, in WeakUpTo.Relations]
Operators.O.Rxy [variable, in WeakUpTo.Relations]
Operators.O.Rxy' [variable, in WeakUpTo.Relations]
Operators.O.Ryz [variable, in WeakUpTo.Relations]
Operators.O.X [variable, in WeakUpTo.Relations]
Operators.O.Y [variable, in WeakUpTo.Relations]
Operators.O.Z [variable, in WeakUpTo.Relations]
Operators.R [variable, in WeakUpTo.Relations]
Operators.X [variable, in WeakUpTo.Relations]
P
plus [definition, in WeakUpTo.Relations]Plus [section, in WeakUpTo.Diagrams]
PlusWf [section, in WeakUpTo.Diagrams]
PlusWf [section, in WeakUpTo.Controlled]
PlusWf.A [variable, in WeakUpTo.Controlled]
PlusWf.B [variable, in WeakUpTo.Controlled]
PlusWf.HB [variable, in WeakUpTo.Controlled]
PlusWf.HB' [variable, in WeakUpTo.Controlled]
PlusWf.Hpwf [variable, in WeakUpTo.Diagrams]
PlusWf.HR [variable, in WeakUpTo.Diagrams]
PlusWf.HR' [variable, in WeakUpTo.Diagrams]
PlusWf.HS [variable, in WeakUpTo.Diagrams]
PlusWf.HS' [variable, in WeakUpTo.Diagrams]
PlusWf.Hwf [variable, in WeakUpTo.Diagrams]
PlusWf.R [variable, in WeakUpTo.Diagrams]
PlusWf.R' [variable, in WeakUpTo.Diagrams]
PlusWf.S [variable, in WeakUpTo.Diagrams]
PlusWf.TX [variable, in WeakUpTo.Diagrams]
PlusWf.TX [variable, in WeakUpTo.Controlled]
PlusWf.TX' [variable, in WeakUpTo.Diagrams]
PlusWf.TY [variable, in WeakUpTo.Diagrams]
PlusWf.TY [variable, in WeakUpTo.Controlled]
PlusWf.TY' [variable, in WeakUpTo.Diagrams]
PlusWf.X [variable, in WeakUpTo.Diagrams]
PlusWf.X [variable, in WeakUpTo.Controlled]
PlusWf.Y [variable, in WeakUpTo.Diagrams]
PlusWf.Y [variable, in WeakUpTo.Controlled]
plus_wf [lemma, in WeakUpTo.Relations]
Plus_WF.Rwf [variable, in WeakUpTo.Relations]
Plus_WF.R [variable, in WeakUpTo.Relations]
Plus_WF.X [variable, in WeakUpTo.Relations]
Plus_WF [section, in WeakUpTo.Relations]
plus_S [lemma, in WeakUpTo.Relations]
plus_trans [lemma, in WeakUpTo.Relations]
plus_star_plus [lemma, in WeakUpTo.Relations]
plus_star [lemma, in WeakUpTo.Relations]
plus_eeq [lemma, in WeakUpTo.Relations]
plus_incl [lemma, in WeakUpTo.Relations]
plus_wf_controlled [lemma, in WeakUpTo.Controlled]
Plus.HR [variable, in WeakUpTo.Diagrams]
Plus.R [variable, in WeakUpTo.Diagrams]
Plus.RX [variable, in WeakUpTo.Diagrams]
Plus.S [variable, in WeakUpTo.Diagrams]
Plus.X [variable, in WeakUpTo.Diagrams]
Plus.X' [variable, in WeakUpTo.Diagrams]
plus1 [lemma, in WeakUpTo.Relations]
R
reduction [definition, in WeakUpTo.Reductions]Reductions [section, in WeakUpTo.Reductions]
Reductions [library]
Reductions.A [variable, in WeakUpTo.Reductions]
Reductions.Diagram [section, in WeakUpTo.Reductions]
Reductions.Diagram.X [variable, in WeakUpTo.Reductions]
Reductions.Diagram.Y [variable, in WeakUpTo.Reductions]
Reductions.R [section, in WeakUpTo.Reductions]
Reductions.R.A [variable, in WeakUpTo.Reductions]
Reductions.R.X [variable, in WeakUpTo.Reductions]
Reductions.Weak [section, in WeakUpTo.Reductions]
Reductions.Weak.Red [variable, in WeakUpTo.Reductions]
Reductions.Weak.X [variable, in WeakUpTo.Reductions]
reduction_t [definition, in WeakUpTo.Reductions]
red_weak [lemma, in WeakUpTo.Reductions]
reflexive [definition, in WeakUpTo.Relations]
relation [definition, in WeakUpTo.Relations]
Relations [library]
relation2 [definition, in WeakUpTo.Relations]
RelaxedExpansion [section, in WeakUpTo.Controlled]
RelaxedExpansion.A [variable, in WeakUpTo.Controlled]
RelaxedExpansion.B [variable, in WeakUpTo.Controlled]
RelaxedExpansion.HB [variable, in WeakUpTo.Controlled]
RelaxedExpansion.TX [variable, in WeakUpTo.Controlled]
RelaxedExpansion.TY [variable, in WeakUpTo.Controlled]
RelaxedExpansion.wexpansion1_ctrl_t [variable, in WeakUpTo.Controlled]
RelaxedExpansion.X [variable, in WeakUpTo.Controlled]
RelaxedExpansion.Y [variable, in WeakUpTo.Controlled]
Reverse [section, in WeakUpTo.Diagrams]
Reverse.H [variable, in WeakUpTo.Diagrams]
Reverse.R [variable, in WeakUpTo.Diagrams]
Reverse.RX [variable, in WeakUpTo.Diagrams]
Reverse.RY [variable, in WeakUpTo.Diagrams]
Reverse.R' [variable, in WeakUpTo.Diagrams]
Reverse.X [variable, in WeakUpTo.Diagrams]
Reverse.X' [variable, in WeakUpTo.Diagrams]
Reverse.Y [variable, in WeakUpTo.Diagrams]
Reverse.Y' [variable, in WeakUpTo.Diagrams]
REWeak [definition, in WeakUpTo.Reductions]
S
semi_commute [definition, in WeakUpTo.Diagrams]set [definition, in WeakUpTo.Relations]
Settings [library]
simulation [definition, in WeakUpTo.Settings]
simulation_comp [lemma, in WeakUpTo.Settings]
simulation_t_eeq [lemma, in WeakUpTo.Settings]
simulation_eeq [lemma, in WeakUpTo.Settings]
simulation_t [definition, in WeakUpTo.Settings]
star [section, in WeakUpTo.Relations]
star [inductive, in WeakUpTo.Relations]
Star [section, in WeakUpTo.Diagrams]
StarWf [section, in WeakUpTo.Diagrams]
StarWf [section, in WeakUpTo.Controlled]
StarWf.A [variable, in WeakUpTo.Controlled]
StarWf.B [variable, in WeakUpTo.Controlled]
StarWf.Gen [section, in WeakUpTo.Diagrams]
StarWf.Gen.HR [variable, in WeakUpTo.Diagrams]
StarWf.Gen.HRT [variable, in WeakUpTo.Diagrams]
StarWf.Gen.HT [variable, in WeakUpTo.Diagrams]
StarWf.Gen.R [variable, in WeakUpTo.Diagrams]
StarWf.Gen.R' [variable, in WeakUpTo.Diagrams]
StarWf.Gen.SR [variable, in WeakUpTo.Diagrams]
StarWf.Gen.SR' [variable, in WeakUpTo.Diagrams]
StarWf.Gen.S' [variable, in WeakUpTo.Diagrams]
StarWf.Gen.TAX [variable, in WeakUpTo.Diagrams]
StarWf.Gen.TaX [variable, in WeakUpTo.Diagrams]
StarWf.Gen.TAY [variable, in WeakUpTo.Diagrams]
StarWf.Gen.TaY [variable, in WeakUpTo.Diagrams]
StarWf.Gen.TY [variable, in WeakUpTo.Diagrams]
StarWf.Gen.X' [variable, in WeakUpTo.Diagrams]
StarWf.Gen.Y [variable, in WeakUpTo.Diagrams]
StarWf.Gen.Y' [variable, in WeakUpTo.Diagrams]
StarWf.HB [variable, in WeakUpTo.Controlled]
StarWf.HB' [variable, in WeakUpTo.Controlled]
StarWf.HS [variable, in WeakUpTo.Diagrams]
StarWf.Hwf [variable, in WeakUpTo.Diagrams]
StarWf.S [variable, in WeakUpTo.Diagrams]
StarWf.TX [variable, in WeakUpTo.Diagrams]
StarWf.TX [variable, in WeakUpTo.Controlled]
StarWf.TY [variable, in WeakUpTo.Controlled]
StarWf.X [variable, in WeakUpTo.Diagrams]
StarWf.X [variable, in WeakUpTo.Controlled]
StarWf.Y [variable, in WeakUpTo.Controlled]
star_wmon [lemma, in WeakUpTo.WeakMonotonic]
star_plus_plus [lemma, in WeakUpTo.Relations]
star_trans [lemma, in WeakUpTo.Relations]
star_S [lemma, in WeakUpTo.Relations]
star_eeq [lemma, in WeakUpTo.Relations]
star_incl [lemma, in WeakUpTo.Relations]
star_refl [constructor, in WeakUpTo.Relations]
star_wf_controlled [lemma, in WeakUpTo.Controlled]
Star.H [variable, in WeakUpTo.Diagrams]
star.R [variable, in WeakUpTo.Relations]
Star.R [variable, in WeakUpTo.Diagrams]
Star.RX [variable, in WeakUpTo.Diagrams]
Star.S [variable, in WeakUpTo.Diagrams]
star.X [variable, in WeakUpTo.Relations]
Star.X [variable, in WeakUpTo.Diagrams]
Star.X' [variable, in WeakUpTo.Diagrams]
star1 [lemma, in WeakUpTo.Relations]
strong_commute [definition, in WeakUpTo.Diagrams]
symmetric [definition, in WeakUpTo.Relations]
S_plus [lemma, in WeakUpTo.Relations]
S_star [constructor, in WeakUpTo.Relations]
T
T [constructor, in WeakUpTo.Reductions]taus_weak [lemma, in WeakUpTo.Reductions]
tau_weak [lemma, in WeakUpTo.Reductions]
Theory [library]
trans [definition, in WeakUpTo.Relations]
transitive [definition, in WeakUpTo.Relations]
transparent [definition, in WeakUpTo.Functions]
trans_eeq [lemma, in WeakUpTo.Relations]
trans_incl [lemma, in WeakUpTo.Relations]
U
UExp [definition, in WeakUpTo.Functions]UExp_wmon [lemma, in WeakUpTo.WeakMonotonic]
UExp_trans [lemma, in WeakUpTo.Functions]
UExp_UExp [lemma, in WeakUpTo.Functions]
UExp_inc [lemma, in WeakUpTo.Functions]
UExp_incl [lemma, in WeakUpTo.Functions]
UExp_mon [lemma, in WeakUpTo.Monotonic]
UIter [definition, in WeakUpTo.Functions]
UIter_wmon [lemma, in WeakUpTo.WeakMonotonic]
UIter_trans [lemma, in WeakUpTo.Functions]
UIter_02 [lemma, in WeakUpTo.Functions]
UIter_inc [lemma, in WeakUpTo.Functions]
UIter_incl [lemma, in WeakUpTo.Functions]
UIter_mon [lemma, in WeakUpTo.Monotonic]
unified_correct [lemma, in WeakUpTo.Theory]
union [definition, in WeakUpTo.Relations]
Union [section, in WeakUpTo.Diagrams]
Union [definition, in WeakUpTo.Functions]
Union_wmon [lemma, in WeakUpTo.WeakMonotonic]
union_eeq [lemma, in WeakUpTo.Relations]
union_incl [lemma, in WeakUpTo.Relations]
union_st [definition, in WeakUpTo.Relations]
Union_mon [lemma, in WeakUpTo.Monotonic]
union_evolve [lemma, in WeakUpTo.Settings]
Union.H [variable, in WeakUpTo.Diagrams]
Union.I [variable, in WeakUpTo.Diagrams]
Union.R [variable, in WeakUpTo.Diagrams]
Union.RX [variable, in WeakUpTo.Diagrams]
Union.RY [variable, in WeakUpTo.Diagrams]
Union.S [variable, in WeakUpTo.Diagrams]
Union.X [variable, in WeakUpTo.Diagrams]
Union.X' [variable, in WeakUpTo.Diagrams]
Union.Y [variable, in WeakUpTo.Diagrams]
Union.Y' [variable, in WeakUpTo.Diagrams]
union2 [definition, in WeakUpTo.Relations]
Union2 [definition, in WeakUpTo.Functions]
Union2_wmon [lemma, in WeakUpTo.WeakMonotonic]
union2_eeq [lemma, in WeakUpTo.Relations]
union2_incl [lemma, in WeakUpTo.Relations]
Union2_mon [lemma, in WeakUpTo.Monotonic]
union2_evolve_right [lemma, in WeakUpTo.Settings]
union2_evolve_left [lemma, in WeakUpTo.Settings]
union2_evolve [lemma, in WeakUpTo.Settings]
upto [lemma, in WeakUpTo.Applications]
upto_ctrl [lemma, in WeakUpTo.Applications]
W
Weak [definition, in WeakUpTo.Reductions]WeakMonotonic [library]
Weak_ind [lemma, in WeakUpTo.Reductions]
weak_taus [lemma, in WeakUpTo.Reductions]
weak_tau [lemma, in WeakUpTo.Reductions]
weak_refl [lemma, in WeakUpTo.Reductions]
weak_strong [lemma, in WeakUpTo.Settings]
weak_strong_t [lemma, in WeakUpTo.Settings]
wexpand [definition, in WeakUpTo.Settings]
wexpand_trans [lemma, in WeakUpTo.Settings]
wexpand_refl [lemma, in WeakUpTo.Settings]
wexpand_bisim [lemma, in WeakUpTo.Settings]
wexpansion [definition, in WeakUpTo.Settings]
wexpansion_comp [lemma, in WeakUpTo.Settings]
wexpansion_wexpand [lemma, in WeakUpTo.Settings]
wexpansion1 [definition, in WeakUpTo.Settings]
wexpansion1_ctrl [lemma, in WeakUpTo.Controlled]
wexpansion1_comp [lemma, in WeakUpTo.Settings]
wmonotonic [record, in WeakUpTo.Settings]
wmonotonic_correct [lemma, in WeakUpTo.Theory]
wmonotonic_correct_t [lemma, in WeakUpTo.Theory]
wmon_a [projection, in WeakUpTo.Settings]
wmon_t [projection, in WeakUpTo.Settings]
wmon_m [projection, in WeakUpTo.Settings]
Variable Index
C
Compose.H1 [in WeakUpTo.Diagrams]Compose.H2 [in WeakUpTo.Diagrams]
Compose.RX [in WeakUpTo.Diagrams]
Compose.RY [in WeakUpTo.Diagrams]
Compose.RZ [in WeakUpTo.Diagrams]
Compose.R1 [in WeakUpTo.Diagrams]
Compose.R2 [in WeakUpTo.Diagrams]
Compose.S1 [in WeakUpTo.Diagrams]
Compose.S2 [in WeakUpTo.Diagrams]
Compose.X [in WeakUpTo.Diagrams]
Compose.X' [in WeakUpTo.Diagrams]
Compose.Y [in WeakUpTo.Diagrams]
Compose.Y' [in WeakUpTo.Diagrams]
Compose.Z [in WeakUpTo.Diagrams]
Compose.Z' [in WeakUpTo.Diagrams]
Controlled.A [in WeakUpTo.Applications]
Controlled.B [in WeakUpTo.Applications]
Controlled.BG [in WeakUpTo.Applications]
Controlled.B' [in WeakUpTo.Applications]
Controlled.B'G [in WeakUpTo.Applications]
Controlled.F [in WeakUpTo.Applications]
Controlled.FG [in WeakUpTo.Applications]
Controlled.F_mon [in WeakUpTo.Applications]
Controlled.G [in WeakUpTo.Applications]
Controlled.HB [in WeakUpTo.Applications]
Controlled.HB' [in WeakUpTo.Applications]
Controlled.HRa [in WeakUpTo.Applications]
Controlled.HRa' [in WeakUpTo.Applications]
Controlled.HRt [in WeakUpTo.Applications]
Controlled.HRt' [in WeakUpTo.Applications]
Controlled.R [in WeakUpTo.Applications]
Controlled.TX [in WeakUpTo.Applications]
Controlled.X [in WeakUpTo.Applications]
D
Definitions.R [in WeakUpTo.Relations]Definitions.X [in WeakUpTo.Relations]
Definitions.Y [in WeakUpTo.Relations]
Definitions.Z [in WeakUpTo.Relations]
Def1.R [in WeakUpTo.Diagrams]
Def1.RX [in WeakUpTo.Diagrams]
Def1.RY [in WeakUpTo.Diagrams]
Def1.R' [in WeakUpTo.Diagrams]
Def1.X [in WeakUpTo.Diagrams]
Def1.X' [in WeakUpTo.Diagrams]
Def1.Y [in WeakUpTo.Diagrams]
Def1.Y' [in WeakUpTo.Diagrams]
Def2.R [in WeakUpTo.Diagrams]
Def2.S [in WeakUpTo.Diagrams]
Def2.X [in WeakUpTo.Diagrams]
E
Eeq1.F [in WeakUpTo.Relations]Eeq1.F' [in WeakUpTo.Relations]
Eeq1.I [in WeakUpTo.Relations]
Eeq1.R [in WeakUpTo.Relations]
Eeq1.R' [in WeakUpTo.Relations]
Eeq1.R1 [in WeakUpTo.Relations]
Eeq1.R1' [in WeakUpTo.Relations]
Eeq1.S [in WeakUpTo.Relations]
Eeq1.S' [in WeakUpTo.Relations]
Eeq1.T [in WeakUpTo.Relations]
Eeq1.T' [in WeakUpTo.Relations]
Eeq1.X [in WeakUpTo.Relations]
Eeq1.Y [in WeakUpTo.Relations]
Eeq1.Z [in WeakUpTo.Relations]
Eeq2.F [in WeakUpTo.Relations]
Eeq2.I [in WeakUpTo.Relations]
Eeq2.R [in WeakUpTo.Relations]
Eeq2.R' [in WeakUpTo.Relations]
Eeq2.S [in WeakUpTo.Relations]
Eeq2.T [in WeakUpTo.Relations]
Eeq2.X [in WeakUpTo.Relations]
Eeq2.Y [in WeakUpTo.Relations]
Eeq2.Z [in WeakUpTo.Relations]
G
Global.A [in WeakUpTo.WeakMonotonic]Global.A [in WeakUpTo.Theory]
Global.A [in WeakUpTo.Monotonic]
Global.A [in WeakUpTo.Settings]
Global.A.A'.E [in WeakUpTo.Monotonic]
Global.A.A'.R [in WeakUpTo.Monotonic]
Global.A.A'.T [in WeakUpTo.Monotonic]
Global.A.F [in WeakUpTo.WeakMonotonic]
Global.A.F [in WeakUpTo.Monotonic]
Global.A.G [in WeakUpTo.WeakMonotonic]
Global.A.G [in WeakUpTo.Monotonic]
Global.A.HF [in WeakUpTo.WeakMonotonic]
Global.A.HF [in WeakUpTo.Monotonic]
Global.A.HG [in WeakUpTo.WeakMonotonic]
Global.A.HG [in WeakUpTo.Monotonic]
Global.A.TX [in WeakUpTo.WeakMonotonic]
Global.A.TX [in WeakUpTo.Monotonic]
Global.A.TY [in WeakUpTo.WeakMonotonic]
Global.A.TY [in WeakUpTo.Monotonic]
Global.A.Union.H [in WeakUpTo.WeakMonotonic]
Global.A.Union.H [in WeakUpTo.Monotonic]
Global.A.Union.HH [in WeakUpTo.WeakMonotonic]
Global.A.Union.HH [in WeakUpTo.Monotonic]
Global.A.Union.I [in WeakUpTo.WeakMonotonic]
Global.A.Union.I [in WeakUpTo.Monotonic]
Global.A.X [in WeakUpTo.WeakMonotonic]
Global.A.X [in WeakUpTo.Monotonic]
Global.A.Y [in WeakUpTo.WeakMonotonic]
Global.A.Y [in WeakUpTo.Monotonic]
Global.BiComposition.R [in WeakUpTo.Settings]
Global.BiComposition.S [in WeakUpTo.Settings]
Global.BiComposition.TX [in WeakUpTo.Settings]
Global.BiComposition.TY [in WeakUpTo.Settings]
Global.BiComposition.TZ [in WeakUpTo.Settings]
Global.BiComposition.X [in WeakUpTo.Settings]
Global.BiComposition.Y [in WeakUpTo.Settings]
Global.BiComposition.Z [in WeakUpTo.Settings]
Global.Bi.TX [in WeakUpTo.Settings]
Global.Bi.TY [in WeakUpTo.Settings]
Global.Bi.X [in WeakUpTo.Settings]
Global.Bi.Y [in WeakUpTo.Settings]
Global.B.F [in WeakUpTo.WeakMonotonic]
Global.B.F [in WeakUpTo.Monotonic]
Global.B.G [in WeakUpTo.WeakMonotonic]
Global.B.G [in WeakUpTo.Monotonic]
Global.B.HF [in WeakUpTo.WeakMonotonic]
Global.B.HF [in WeakUpTo.Monotonic]
Global.B.HG [in WeakUpTo.WeakMonotonic]
Global.B.HG [in WeakUpTo.Monotonic]
Global.B.TX [in WeakUpTo.WeakMonotonic]
Global.B.TX [in WeakUpTo.Monotonic]
Global.B.TY [in WeakUpTo.WeakMonotonic]
Global.B.TY [in WeakUpTo.Monotonic]
Global.B.X [in WeakUpTo.WeakMonotonic]
Global.B.X [in WeakUpTo.Monotonic]
Global.B.Y [in WeakUpTo.WeakMonotonic]
Global.B.Y [in WeakUpTo.Monotonic]
Global.Composition.R [in WeakUpTo.Settings]
Global.Composition.S [in WeakUpTo.Settings]
Global.Composition.TX [in WeakUpTo.Settings]
Global.Composition.TY [in WeakUpTo.Settings]
Global.Composition.TZ [in WeakUpTo.Settings]
Global.Composition.wexpansion1_t [in WeakUpTo.Settings]
Global.Composition.X [in WeakUpTo.Settings]
Global.Composition.Y [in WeakUpTo.Settings]
Global.Composition.Z [in WeakUpTo.Settings]
Global.ControlledCorrect.B [in WeakUpTo.Theory]
Global.ControlledCorrect.F [in WeakUpTo.Theory]
Global.ControlledCorrect.G [in WeakUpTo.Theory]
Global.ControlledCorrect.HB [in WeakUpTo.Theory]
Global.ControlledCorrect.HBF [in WeakUpTo.Theory]
Global.ControlledCorrect.HBG [in WeakUpTo.Theory]
Global.ControlledCorrect.HBGGn [in WeakUpTo.Theory]
Global.ControlledCorrect.HF [in WeakUpTo.Theory]
Global.ControlledCorrect.HFG [in WeakUpTo.Theory]
Global.ControlledCorrect.HFGn [in WeakUpTo.Theory]
Global.ControlledCorrect.HG [in WeakUpTo.Theory]
Global.ControlledCorrect.HGGBF [in WeakUpTo.Theory]
Global.ControlledCorrect.HRa [in WeakUpTo.Theory]
Global.ControlledCorrect.HRt [in WeakUpTo.Theory]
Global.ControlledCorrect.pre_visible [in WeakUpTo.Theory]
Global.ControlledCorrect.pre_silent [in WeakUpTo.Theory]
Global.ControlledCorrect.R [in WeakUpTo.Theory]
Global.ControlledCorrect.silent [in WeakUpTo.Theory]
Global.ControlledCorrect.visible [in WeakUpTo.Theory]
Global.C.F [in WeakUpTo.WeakMonotonic]
Global.C.G [in WeakUpTo.WeakMonotonic]
Global.C.HF [in WeakUpTo.WeakMonotonic]
Global.C.HG [in WeakUpTo.WeakMonotonic]
Global.C.HL [in WeakUpTo.WeakMonotonic]
Global.C.L [in WeakUpTo.WeakMonotonic]
Global.C.TX [in WeakUpTo.WeakMonotonic]
Global.C.TY [in WeakUpTo.WeakMonotonic]
Global.C.X [in WeakUpTo.WeakMonotonic]
Global.C.Y [in WeakUpTo.WeakMonotonic]
Global.Def'.F [in WeakUpTo.Functions]
Global.Def'.R [in WeakUpTo.Functions]
Global.Def'.X [in WeakUpTo.Functions]
Global.Def'.X' [in WeakUpTo.Functions]
Global.Def'.X'' [in WeakUpTo.Functions]
Global.Def'.Y [in WeakUpTo.Functions]
Global.Def'.Y' [in WeakUpTo.Functions]
Global.Def'.Y'' [in WeakUpTo.Functions]
Global.Def'.Z [in WeakUpTo.Functions]
Global.Def'.Z' [in WeakUpTo.Functions]
Global.Def.X [in WeakUpTo.Functions]
Global.Def.X' [in WeakUpTo.Functions]
Global.Def.Y [in WeakUpTo.Functions]
Global.Def.Y' [in WeakUpTo.Functions]
Global.MonotonicCorrect.F [in WeakUpTo.Theory]
Global.MonotonicCorrect.HF [in WeakUpTo.Theory]
Global.MonotonicCorrect.HR [in WeakUpTo.Theory]
Global.MonotonicCorrect.phi [in WeakUpTo.Theory]
Global.MonotonicCorrect.R [in WeakUpTo.Theory]
Global.Properties.TX [in WeakUpTo.Settings]
Global.Properties.X [in WeakUpTo.Settings]
Global.Sim.B [in WeakUpTo.Settings]
Global.Sim.F [in WeakUpTo.Settings]
Global.Sim.TX [in WeakUpTo.Settings]
Global.Sim.TY [in WeakUpTo.Settings]
Global.Sim.X [in WeakUpTo.Settings]
Global.Sim.Y [in WeakUpTo.Settings]
Global.TX [in WeakUpTo.Theory]
Global.TY [in WeakUpTo.Theory]
Global.UIter'.F [in WeakUpTo.Functions]
Global.UIter'.HF [in WeakUpTo.Functions]
Global.UIter'.HF' [in WeakUpTo.Functions]
Global.UIter'.X [in WeakUpTo.Functions]
Global.UIter.F [in WeakUpTo.Functions]
Global.UIter.HF [in WeakUpTo.Functions]
Global.UIter.HF0 [in WeakUpTo.Functions]
Global.UIter.HF2 [in WeakUpTo.Functions]
Global.UIter.X [in WeakUpTo.Functions]
Global.UIter.Y [in WeakUpTo.Functions]
Global.UnifiedCorrect.F [in WeakUpTo.Theory]
Global.UnifiedCorrect.G [in WeakUpTo.Theory]
Global.UnifiedCorrect.HF [in WeakUpTo.Theory]
Global.UnifiedCorrect.HFG [in WeakUpTo.Theory]
Global.UnifiedCorrect.HFGn [in WeakUpTo.Theory]
Global.UnifiedCorrect.HG [in WeakUpTo.Theory]
Global.UnifiedCorrect.HGFG [in WeakUpTo.Theory]
Global.UnifiedCorrect.HGFGn [in WeakUpTo.Theory]
Global.UnifiedCorrect.HRa [in WeakUpTo.Theory]
Global.UnifiedCorrect.HRt [in WeakUpTo.Theory]
Global.UnifiedCorrect.pre_visible [in WeakUpTo.Theory]
Global.UnifiedCorrect.pre_silent [in WeakUpTo.Theory]
Global.UnifiedCorrect.R [in WeakUpTo.Theory]
Global.UnifiedCorrect.silent [in WeakUpTo.Theory]
Global.UnifiedCorrect.visible [in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.F [in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.HF [in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.HRa [in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.HRt [in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.R [in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.silent [in WeakUpTo.Theory]
Global.WeakMonotonicCorrect.visible [in WeakUpTo.Theory]
Global.X [in WeakUpTo.Theory]
Global.Y [in WeakUpTo.Theory]
I
InclEeq.R [in WeakUpTo.Relations]InclEeq.S [in WeakUpTo.Relations]
InclEeq.T [in WeakUpTo.Relations]
InclEeq.X [in WeakUpTo.Relations]
InclEeq.Y [in WeakUpTo.Relations]
Incl.H [in WeakUpTo.Diagrams]
Incl.HR [in WeakUpTo.Diagrams]
Incl.HS [in WeakUpTo.Diagrams]
Incl.R [in WeakUpTo.Diagrams]
Incl.RX [in WeakUpTo.Diagrams]
Incl.RY [in WeakUpTo.Diagrams]
Incl.R' [in WeakUpTo.Diagrams]
Incl.S [in WeakUpTo.Diagrams]
Incl.S' [in WeakUpTo.Diagrams]
Incl.X [in WeakUpTo.Diagrams]
Incl.X' [in WeakUpTo.Diagrams]
Incl.Y [in WeakUpTo.Diagrams]
Incl.Y' [in WeakUpTo.Diagrams]
M
Modular.A [in WeakUpTo.Applications]Modular.F [in WeakUpTo.Applications]
Modular.G [in WeakUpTo.Applications]
Modular.HRa [in WeakUpTo.Applications]
Modular.HRa' [in WeakUpTo.Applications]
Modular.HRt [in WeakUpTo.Applications]
Modular.HRt' [in WeakUpTo.Applications]
Modular.R [in WeakUpTo.Applications]
Modular.TX [in WeakUpTo.Applications]
Modular.X [in WeakUpTo.Applications]
O
Operators.O.Rxy [in WeakUpTo.Relations]Operators.O.Rxy' [in WeakUpTo.Relations]
Operators.O.Ryz [in WeakUpTo.Relations]
Operators.O.X [in WeakUpTo.Relations]
Operators.O.Y [in WeakUpTo.Relations]
Operators.O.Z [in WeakUpTo.Relations]
Operators.R [in WeakUpTo.Relations]
Operators.X [in WeakUpTo.Relations]
P
PlusWf.A [in WeakUpTo.Controlled]PlusWf.B [in WeakUpTo.Controlled]
PlusWf.HB [in WeakUpTo.Controlled]
PlusWf.HB' [in WeakUpTo.Controlled]
PlusWf.Hpwf [in WeakUpTo.Diagrams]
PlusWf.HR [in WeakUpTo.Diagrams]
PlusWf.HR' [in WeakUpTo.Diagrams]
PlusWf.HS [in WeakUpTo.Diagrams]
PlusWf.HS' [in WeakUpTo.Diagrams]
PlusWf.Hwf [in WeakUpTo.Diagrams]
PlusWf.R [in WeakUpTo.Diagrams]
PlusWf.R' [in WeakUpTo.Diagrams]
PlusWf.S [in WeakUpTo.Diagrams]
PlusWf.TX [in WeakUpTo.Diagrams]
PlusWf.TX [in WeakUpTo.Controlled]
PlusWf.TX' [in WeakUpTo.Diagrams]
PlusWf.TY [in WeakUpTo.Diagrams]
PlusWf.TY [in WeakUpTo.Controlled]
PlusWf.TY' [in WeakUpTo.Diagrams]
PlusWf.X [in WeakUpTo.Diagrams]
PlusWf.X [in WeakUpTo.Controlled]
PlusWf.Y [in WeakUpTo.Diagrams]
PlusWf.Y [in WeakUpTo.Controlled]
Plus_WF.Rwf [in WeakUpTo.Relations]
Plus_WF.R [in WeakUpTo.Relations]
Plus_WF.X [in WeakUpTo.Relations]
Plus.HR [in WeakUpTo.Diagrams]
Plus.R [in WeakUpTo.Diagrams]
Plus.RX [in WeakUpTo.Diagrams]
Plus.S [in WeakUpTo.Diagrams]
Plus.X [in WeakUpTo.Diagrams]
Plus.X' [in WeakUpTo.Diagrams]
R
Reductions.A [in WeakUpTo.Reductions]Reductions.Diagram.X [in WeakUpTo.Reductions]
Reductions.Diagram.Y [in WeakUpTo.Reductions]
Reductions.R.A [in WeakUpTo.Reductions]
Reductions.R.X [in WeakUpTo.Reductions]
Reductions.Weak.Red [in WeakUpTo.Reductions]
Reductions.Weak.X [in WeakUpTo.Reductions]
RelaxedExpansion.A [in WeakUpTo.Controlled]
RelaxedExpansion.B [in WeakUpTo.Controlled]
RelaxedExpansion.HB [in WeakUpTo.Controlled]
RelaxedExpansion.TX [in WeakUpTo.Controlled]
RelaxedExpansion.TY [in WeakUpTo.Controlled]
RelaxedExpansion.wexpansion1_ctrl_t [in WeakUpTo.Controlled]
RelaxedExpansion.X [in WeakUpTo.Controlled]
RelaxedExpansion.Y [in WeakUpTo.Controlled]
Reverse.H [in WeakUpTo.Diagrams]
Reverse.R [in WeakUpTo.Diagrams]
Reverse.RX [in WeakUpTo.Diagrams]
Reverse.RY [in WeakUpTo.Diagrams]
Reverse.R' [in WeakUpTo.Diagrams]
Reverse.X [in WeakUpTo.Diagrams]
Reverse.X' [in WeakUpTo.Diagrams]
Reverse.Y [in WeakUpTo.Diagrams]
Reverse.Y' [in WeakUpTo.Diagrams]
S
StarWf.A [in WeakUpTo.Controlled]StarWf.B [in WeakUpTo.Controlled]
StarWf.Gen.HR [in WeakUpTo.Diagrams]
StarWf.Gen.HRT [in WeakUpTo.Diagrams]
StarWf.Gen.HT [in WeakUpTo.Diagrams]
StarWf.Gen.R [in WeakUpTo.Diagrams]
StarWf.Gen.R' [in WeakUpTo.Diagrams]
StarWf.Gen.SR [in WeakUpTo.Diagrams]
StarWf.Gen.SR' [in WeakUpTo.Diagrams]
StarWf.Gen.S' [in WeakUpTo.Diagrams]
StarWf.Gen.TAX [in WeakUpTo.Diagrams]
StarWf.Gen.TaX [in WeakUpTo.Diagrams]
StarWf.Gen.TAY [in WeakUpTo.Diagrams]
StarWf.Gen.TaY [in WeakUpTo.Diagrams]
StarWf.Gen.TY [in WeakUpTo.Diagrams]
StarWf.Gen.X' [in WeakUpTo.Diagrams]
StarWf.Gen.Y [in WeakUpTo.Diagrams]
StarWf.Gen.Y' [in WeakUpTo.Diagrams]
StarWf.HB [in WeakUpTo.Controlled]
StarWf.HB' [in WeakUpTo.Controlled]
StarWf.HS [in WeakUpTo.Diagrams]
StarWf.Hwf [in WeakUpTo.Diagrams]
StarWf.S [in WeakUpTo.Diagrams]
StarWf.TX [in WeakUpTo.Diagrams]
StarWf.TX [in WeakUpTo.Controlled]
StarWf.TY [in WeakUpTo.Controlled]
StarWf.X [in WeakUpTo.Diagrams]
StarWf.X [in WeakUpTo.Controlled]
StarWf.Y [in WeakUpTo.Controlled]
Star.H [in WeakUpTo.Diagrams]
star.R [in WeakUpTo.Relations]
Star.R [in WeakUpTo.Diagrams]
Star.RX [in WeakUpTo.Diagrams]
Star.S [in WeakUpTo.Diagrams]
star.X [in WeakUpTo.Relations]
Star.X [in WeakUpTo.Diagrams]
Star.X' [in WeakUpTo.Diagrams]
U
Union.H [in WeakUpTo.Diagrams]Union.I [in WeakUpTo.Diagrams]
Union.R [in WeakUpTo.Diagrams]
Union.RX [in WeakUpTo.Diagrams]
Union.RY [in WeakUpTo.Diagrams]
Union.S [in WeakUpTo.Diagrams]
Union.X [in WeakUpTo.Diagrams]
Union.X' [in WeakUpTo.Diagrams]
Union.Y [in WeakUpTo.Diagrams]
Union.Y' [in WeakUpTo.Diagrams]
Library Index
A
ApplicationsC
ControlledD
DiagramsF
FunctionsM
MonotonicR
ReductionsRelations
S
SettingsT
TheoryW
WeakMonotonicLemma Index
A
Acc_clos_trans [in WeakUpTo.Relations]B
bisimulation_comp [in WeakUpTo.Settings]bisimulation_bisim [in WeakUpTo.Settings]
bisim_trans [in WeakUpTo.Settings]
bisim_refl [in WeakUpTo.Settings]
bisim_sym [in WeakUpTo.Settings]
C
chaing_l_wmon [in WeakUpTo.WeakMonotonic]Chaining_wmon [in WeakUpTo.WeakMonotonic]
chaining_l_mon [in WeakUpTo.Monotonic]
chaining_r_mon [in WeakUpTo.Monotonic]
Comp_wmon [in WeakUpTo.WeakMonotonic]
comp_star_plus [in WeakUpTo.Relations]
comp_plus_star [in WeakUpTo.Relations]
comp_star_star [in WeakUpTo.Relations]
comp_assoc [in WeakUpTo.Relations]
comp_eeq [in WeakUpTo.Relations]
comp_incl [in WeakUpTo.Relations]
Comp_mon [in WeakUpTo.Monotonic]
constant_mon [in WeakUpTo.Monotonic]
controlled_correct [in WeakUpTo.Theory]
D
diagram_star_wf [in WeakUpTo.Diagrams]diagram_star_wf_2 [in WeakUpTo.Diagrams]
diagram_star_wf_1 [in WeakUpTo.Diagrams]
diagram_plus_wf_2 [in WeakUpTo.Diagrams]
diagram_plus_wf_1 [in WeakUpTo.Diagrams]
diagram_plus_wf [in WeakUpTo.Diagrams]
diagram_plus [in WeakUpTo.Diagrams]
diagram_star [in WeakUpTo.Diagrams]
diagram_union [in WeakUpTo.Diagrams]
diagram_comp [in WeakUpTo.Diagrams]
diagram_reverse [in WeakUpTo.Diagrams]
diagram_incl [in WeakUpTo.Diagrams]
E
eeq_sym [in WeakUpTo.Relations]eeq_trans [in WeakUpTo.Relations]
eeq_refl [in WeakUpTo.Relations]
evolve_incl [in WeakUpTo.Settings]
evolve_union [in WeakUpTo.Settings]
expand_trans [in WeakUpTo.Settings]
expand_refl [in WeakUpTo.Settings]
expand_wexpand [in WeakUpTo.Settings]
expansion_comp [in WeakUpTo.Settings]
expansion_expand [in WeakUpTo.Settings]
expansion1_comp [in WeakUpTo.Settings]
F
FG [in WeakUpTo.Applications]F_mon [in WeakUpTo.Applications]
G
G_reverse [in WeakUpTo.Applications]G_wmon [in WeakUpTo.Applications]
I
identity_mon [in WeakUpTo.Monotonic]incl_trans [in WeakUpTo.Relations]
incl_refl [in WeakUpTo.Relations]
incl_evolve [in WeakUpTo.Settings]
inv_union2 [in WeakUpTo.Relations]
inv_plus [in WeakUpTo.Relations]
inv_star [in WeakUpTo.Relations]
inv_union [in WeakUpTo.Relations]
inv_comp [in WeakUpTo.Relations]
inv_inv [in WeakUpTo.Relations]
M
monotonic_wmonotonic [in WeakUpTo.WeakMonotonic]monotonic_correct [in WeakUpTo.Theory]
P
plus_wf [in WeakUpTo.Relations]plus_S [in WeakUpTo.Relations]
plus_trans [in WeakUpTo.Relations]
plus_star_plus [in WeakUpTo.Relations]
plus_star [in WeakUpTo.Relations]
plus_eeq [in WeakUpTo.Relations]
plus_incl [in WeakUpTo.Relations]
plus_wf_controlled [in WeakUpTo.Controlled]
plus1 [in WeakUpTo.Relations]
R
red_weak [in WeakUpTo.Reductions]S
simulation_comp [in WeakUpTo.Settings]simulation_t_eeq [in WeakUpTo.Settings]
simulation_eeq [in WeakUpTo.Settings]
star_wmon [in WeakUpTo.WeakMonotonic]
star_plus_plus [in WeakUpTo.Relations]
star_trans [in WeakUpTo.Relations]
star_S [in WeakUpTo.Relations]
star_eeq [in WeakUpTo.Relations]
star_incl [in WeakUpTo.Relations]
star_wf_controlled [in WeakUpTo.Controlled]
star1 [in WeakUpTo.Relations]
S_plus [in WeakUpTo.Relations]
T
taus_weak [in WeakUpTo.Reductions]tau_weak [in WeakUpTo.Reductions]
trans_eeq [in WeakUpTo.Relations]
trans_incl [in WeakUpTo.Relations]
U
UExp_wmon [in WeakUpTo.WeakMonotonic]UExp_trans [in WeakUpTo.Functions]
UExp_UExp [in WeakUpTo.Functions]
UExp_inc [in WeakUpTo.Functions]
UExp_incl [in WeakUpTo.Functions]
UExp_mon [in WeakUpTo.Monotonic]
UIter_wmon [in WeakUpTo.WeakMonotonic]
UIter_trans [in WeakUpTo.Functions]
UIter_02 [in WeakUpTo.Functions]
UIter_inc [in WeakUpTo.Functions]
UIter_incl [in WeakUpTo.Functions]
UIter_mon [in WeakUpTo.Monotonic]
unified_correct [in WeakUpTo.Theory]
Union_wmon [in WeakUpTo.WeakMonotonic]
union_eeq [in WeakUpTo.Relations]
union_incl [in WeakUpTo.Relations]
Union_mon [in WeakUpTo.Monotonic]
union_evolve [in WeakUpTo.Settings]
Union2_wmon [in WeakUpTo.WeakMonotonic]
union2_eeq [in WeakUpTo.Relations]
union2_incl [in WeakUpTo.Relations]
Union2_mon [in WeakUpTo.Monotonic]
union2_evolve_right [in WeakUpTo.Settings]
union2_evolve_left [in WeakUpTo.Settings]
union2_evolve [in WeakUpTo.Settings]
upto [in WeakUpTo.Applications]
upto_ctrl [in WeakUpTo.Applications]
W
Weak_ind [in WeakUpTo.Reductions]weak_taus [in WeakUpTo.Reductions]
weak_tau [in WeakUpTo.Reductions]
weak_refl [in WeakUpTo.Reductions]
weak_strong [in WeakUpTo.Settings]
weak_strong_t [in WeakUpTo.Settings]
wexpand_trans [in WeakUpTo.Settings]
wexpand_refl [in WeakUpTo.Settings]
wexpand_bisim [in WeakUpTo.Settings]
wexpansion_comp [in WeakUpTo.Settings]
wexpansion_wexpand [in WeakUpTo.Settings]
wexpansion1_ctrl [in WeakUpTo.Controlled]
wexpansion1_comp [in WeakUpTo.Settings]
wmonotonic_correct [in WeakUpTo.Theory]
wmonotonic_correct_t [in WeakUpTo.Theory]
Constructor Index
L
L [in WeakUpTo.Reductions]M
mkctrl [in WeakUpTo.Settings]mkmon [in WeakUpTo.Settings]
mkwmon [in WeakUpTo.Settings]
S
star_refl [in WeakUpTo.Relations]S_star [in WeakUpTo.Relations]
T
T [in WeakUpTo.Reductions]Inductive Index
L
Lbl [in WeakUpTo.Reductions]S
star [in WeakUpTo.Relations]Projection Index
C
ctrl_a [in WeakUpTo.Settings]ctrl_t [in WeakUpTo.Settings]
M
mon_a [in WeakUpTo.Settings]mon_t [in WeakUpTo.Settings]
mon_m [in WeakUpTo.Settings]
W
wmon_a [in WeakUpTo.Settings]wmon_t [in WeakUpTo.Settings]
wmon_m [in WeakUpTo.Settings]
Section Index
C
Compose [in WeakUpTo.Diagrams]Controlled [in WeakUpTo.Applications]
D
Definitions [in WeakUpTo.Relations]Def1 [in WeakUpTo.Diagrams]
Def2 [in WeakUpTo.Diagrams]
E
Eeq1 [in WeakUpTo.Relations]Eeq2 [in WeakUpTo.Relations]
G
Global [in WeakUpTo.WeakMonotonic]Global [in WeakUpTo.Theory]
Global [in WeakUpTo.Functions]
Global [in WeakUpTo.Monotonic]
Global [in WeakUpTo.Settings]
Global.A [in WeakUpTo.WeakMonotonic]
Global.A [in WeakUpTo.Monotonic]
Global.A.A' [in WeakUpTo.Monotonic]
Global.A.Union [in WeakUpTo.WeakMonotonic]
Global.A.Union [in WeakUpTo.Monotonic]
Global.B [in WeakUpTo.WeakMonotonic]
Global.B [in WeakUpTo.Monotonic]
Global.Bi [in WeakUpTo.Settings]
Global.BiComposition [in WeakUpTo.Settings]
Global.C [in WeakUpTo.WeakMonotonic]
Global.Composition [in WeakUpTo.Settings]
Global.ControlledCorrect [in WeakUpTo.Theory]
Global.Def [in WeakUpTo.Functions]
Global.Def' [in WeakUpTo.Functions]
Global.MonotonicCorrect [in WeakUpTo.Theory]
Global.Properties [in WeakUpTo.Settings]
Global.Sim [in WeakUpTo.Settings]
Global.UIter [in WeakUpTo.Functions]
Global.UIter' [in WeakUpTo.Functions]
Global.UnifiedCorrect [in WeakUpTo.Theory]
Global.WeakMonotonicCorrect [in WeakUpTo.Theory]
I
Incl [in WeakUpTo.Diagrams]InclEeq [in WeakUpTo.Relations]
M
Modular [in WeakUpTo.Applications]O
Operators [in WeakUpTo.Relations]Operators.O [in WeakUpTo.Relations]
P
Plus [in WeakUpTo.Diagrams]PlusWf [in WeakUpTo.Diagrams]
PlusWf [in WeakUpTo.Controlled]
Plus_WF [in WeakUpTo.Relations]
R
Reductions [in WeakUpTo.Reductions]Reductions.Diagram [in WeakUpTo.Reductions]
Reductions.R [in WeakUpTo.Reductions]
Reductions.Weak [in WeakUpTo.Reductions]
RelaxedExpansion [in WeakUpTo.Controlled]
Reverse [in WeakUpTo.Diagrams]
S
star [in WeakUpTo.Relations]Star [in WeakUpTo.Diagrams]
StarWf [in WeakUpTo.Diagrams]
StarWf [in WeakUpTo.Controlled]
StarWf.Gen [in WeakUpTo.Diagrams]
U
Union [in WeakUpTo.Diagrams]Definition Index
A
antisymmetric [in WeakUpTo.Relations]B
bicontrolled [in WeakUpTo.Settings]bisim [in WeakUpTo.Settings]
bisimulation [in WeakUpTo.Settings]
C
Chain [in WeakUpTo.Functions]chaining_r [in WeakUpTo.Functions]
chaining_l [in WeakUpTo.Functions]
commute [in WeakUpTo.Diagrams]
comp [in WeakUpTo.Relations]
Comp [in WeakUpTo.Functions]
confluent [in WeakUpTo.Diagrams]
constant [in WeakUpTo.Functions]
contains [in WeakUpTo.Functions]
D
diagram [in WeakUpTo.Diagrams]diagram_r [in WeakUpTo.Reductions]
E
eeq [in WeakUpTo.Relations]eeq_r [in WeakUpTo.Reductions]
eta2 [in WeakUpTo.Relations]
evolve [in WeakUpTo.Settings]
evolve_a [in WeakUpTo.Settings]
evolve_t [in WeakUpTo.Settings]
evolve_1 [in WeakUpTo.Settings]
EWeak [in WeakUpTo.Reductions]
Exp [in WeakUpTo.Functions]
expand [in WeakUpTo.Settings]
expansion [in WeakUpTo.Settings]
expansion1 [in WeakUpTo.Settings]
F
function [in WeakUpTo.Functions]function2 [in WeakUpTo.Functions]
I
identity [in WeakUpTo.Functions]incl [in WeakUpTo.Relations]
incl_r [in WeakUpTo.Reductions]
increasing [in WeakUpTo.Functions]
Iter [in WeakUpTo.Functions]
L
local_commute [in WeakUpTo.Diagrams]P
plus [in WeakUpTo.Relations]R
reduction [in WeakUpTo.Reductions]reduction_t [in WeakUpTo.Reductions]
reflexive [in WeakUpTo.Relations]
relation [in WeakUpTo.Relations]
relation2 [in WeakUpTo.Relations]
REWeak [in WeakUpTo.Reductions]
S
semi_commute [in WeakUpTo.Diagrams]set [in WeakUpTo.Relations]
simulation [in WeakUpTo.Settings]
simulation_t [in WeakUpTo.Settings]
strong_commute [in WeakUpTo.Diagrams]
symmetric [in WeakUpTo.Relations]
T
trans [in WeakUpTo.Relations]transitive [in WeakUpTo.Relations]
transparent [in WeakUpTo.Functions]
U
UExp [in WeakUpTo.Functions]UIter [in WeakUpTo.Functions]
union [in WeakUpTo.Relations]
Union [in WeakUpTo.Functions]
union_st [in WeakUpTo.Relations]
union2 [in WeakUpTo.Relations]
Union2 [in WeakUpTo.Functions]
W
Weak [in WeakUpTo.Reductions]wexpand [in WeakUpTo.Settings]
wexpansion [in WeakUpTo.Settings]
wexpansion1 [in WeakUpTo.Settings]
Record Index
C
controlled [in WeakUpTo.Settings]M
monotonic [in WeakUpTo.Settings]W
wmonotonic [in WeakUpTo.Settings]| 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 | (641 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 | (368 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 | (10 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 | (127 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 | (7 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 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 | (54 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 | (62 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |