Contribution: AxiomaticABP

Global Index

J

Q

U

V

W

Z

_

(333 entries)

Section Index

A

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(18 entries)

Lemma Index

A

B

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(27 entries)

Constructor Index

A

B

F

G

H

J

K

L

M

O

P

Q

U

V

W

X

Y

Z

_

(22 entries)

Inductive Index

B

C

D

F

G

H

I

J

K

M

N

P

Q

R

S

T

U

V

W

X

Y

Z

_

(4 entries)

Definition Index

B

C

E

F

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

Z

_

(14 entries)

Axiom Index

J

Q

U

V

W

Z

_

(160 entries)

Variable Index

A

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(81 entries)

Library Index

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

_

(7 entries)

Global Index

A

ABP [definition, in AxiomaticABP.abp_defs]
abp_base [library]
abp_defs [library]
abp_lem1 [library]
abp_lem2 [library]
abp_lem25 [library]
abp_lem3 [library]
abp_proc [library]
act [inductive, in AxiomaticABP.abp_base]
alt [axiom, in AxiomaticABP.abp_base]
andb [axiom, in AxiomaticABP.abp_defs]
andb1 [axiom, in AxiomaticABP.abp_defs]
andb2 [axiom, in AxiomaticABP.abp_defs]
A1 [axiom, in AxiomaticABP.abp_base]
A2 [axiom, in AxiomaticABP.abp_base]
A3 [axiom, in AxiomaticABP.abp_base]
A4 [axiom, in AxiomaticABP.abp_base]
A5 [axiom, in AxiomaticABP.abp_base]
A6 [axiom, in AxiomaticABP.abp_base]
A7 [axiom, in AxiomaticABP.abp_base]

B

B [axiom, in AxiomaticABP.abp_proc]
BIT [section, in AxiomaticABP.abp_defs]
bit [axiom, in AxiomaticABP.abp_defs]
BIT.b [variable, in AxiomaticABP.abp_defs]
bit1 [axiom, in AxiomaticABP.abp_defs]
bit2 [axiom, in AxiomaticABP.abp_defs]
bit3 [axiom, in AxiomaticABP.abp_defs]
BOOL [section, in AxiomaticABP.abp_defs]
BOOL.b [variable, in AxiomaticABP.abp_defs]
BPA [section, in AxiomaticABP.abp_base]
BPA.x [variable, in AxiomaticABP.abp_base]
BPA.y [variable, in AxiomaticABP.abp_base]
BPA.z [variable, in AxiomaticABP.abp_base]

C

CF1 [axiom, in AxiomaticABP.abp_base]
CF2 [axiom, in AxiomaticABP.abp_base]
CF2' [axiom, in AxiomaticABP.abp_base]
CF2'' [axiom, in AxiomaticABP.abp_base]
ChanK [axiom, in AxiomaticABP.abp_defs]
ChanL [axiom, in AxiomaticABP.abp_defs]
CM1 [axiom, in AxiomaticABP.abp_base]
CM2 [axiom, in AxiomaticABP.abp_base]
CM3 [axiom, in AxiomaticABP.abp_base]
CM4 [axiom, in AxiomaticABP.abp_base]
CM5 [axiom, in AxiomaticABP.abp_base]
CM6 [axiom, in AxiomaticABP.abp_base]
CM7 [axiom, in AxiomaticABP.abp_base]
CM8 [axiom, in AxiomaticABP.abp_base]
CM9 [axiom, in AxiomaticABP.abp_base]
comm [axiom, in AxiomaticABP.abp_base]
Comms3L [lemma, in AxiomaticABP.abp_lem1]
Comms3Rn_b [lemma, in AxiomaticABP.abp_lem1]
Comms3Rn_b' [lemma, in AxiomaticABP.abp_lem1]
Comms3Rn_lce [lemma, in AxiomaticABP.abp_lem1]
Comms3Tn_d [lemma, in AxiomaticABP.abp_lem1]
CommTn_dRn [lemma, in AxiomaticABP.abp_lem1]
COMMUNICATION_F [section, in AxiomaticABP.abp_base]
COMMUNICATION_F.a [variable, in AxiomaticABP.abp_base]
COMMUNICATION_F.b [variable, in AxiomaticABP.abp_base]
COMMUNICATION_F.E [variable, in AxiomaticABP.abp_base]
COMMUNICATION_F.e [variable, in AxiomaticABP.abp_base]
COMMUNICATION_F.e1 [variable, in AxiomaticABP.abp_base]
COMMUNICATION_F.e2 [variable, in AxiomaticABP.abp_base]
COMMUNICATION_F.F [variable, in AxiomaticABP.abp_base]
COMMUNICATION_F.f [variable, in AxiomaticABP.abp_base]
cond [axiom, in AxiomaticABP.abp_base]
CONDITION [section, in AxiomaticABP.abp_base]
CONDITION.x [variable, in AxiomaticABP.abp_base]
CONDITION.y [variable, in AxiomaticABP.abp_base]
COND1 [axiom, in AxiomaticABP.abp_base]
COND2 [axiom, in AxiomaticABP.abp_base]
cons [constructor, in AxiomaticABP.abp_base]
c2 [constructor, in AxiomaticABP.abp_base]
c3 [constructor, in AxiomaticABP.abp_base]
c5 [constructor, in AxiomaticABP.abp_base]
c6 [constructor, in AxiomaticABP.abp_base]

D

D [axiom, in AxiomaticABP.abp_defs]
DATA [section, in AxiomaticABP.abp_defs]
DATA.d [variable, in AxiomaticABP.abp_defs]
DATA.e [variable, in AxiomaticABP.abp_defs]
Delta [definition, in AxiomaticABP.abp_base]
delta [constructor, in AxiomaticABP.abp_base]
D1 [axiom, in AxiomaticABP.abp_base]
D2 [axiom, in AxiomaticABP.abp_base]
D3 [axiom, in AxiomaticABP.abp_base]
D4 [axiom, in AxiomaticABP.abp_base]
D5 [axiom, in AxiomaticABP.abp_base]

E

ehcons [constructor, in AxiomaticABP.abp_base]
ehlist [inductive, in AxiomaticABP.abp_base]
ehnil [constructor, in AxiomaticABP.abp_base]
enc [axiom, in AxiomaticABP.abp_base]
ENCAPSULATION [section, in AxiomaticABP.abp_base]
ENCAPSULATION.a [variable, in AxiomaticABP.abp_base]
ENCAPSULATION.e [variable, in AxiomaticABP.abp_base]
ENCAPSULATION.E [variable, in AxiomaticABP.abp_base]
ENCAPSULATION.L [variable, in AxiomaticABP.abp_base]
ENCAPSULATION.x [variable, in AxiomaticABP.abp_base]
ENCAPSULATION.y [variable, in AxiomaticABP.abp_base]
EQ [axiom, in AxiomaticABP.abp_base]
eqb [axiom, in AxiomaticABP.abp_defs]
eqD [axiom, in AxiomaticABP.abp_defs]
EQDi [axiom, in AxiomaticABP.abp_defs]
eqD5 [axiom, in AxiomaticABP.abp_defs]
eqD6 [axiom, in AxiomaticABP.abp_defs]
eqD7 [axiom, in AxiomaticABP.abp_defs]
eqD8 [axiom, in AxiomaticABP.abp_defs]
eqF [axiom, in AxiomaticABP.abp_defs]
eqf [axiom, in AxiomaticABP.abp_defs]
EQFD [axiom, in AxiomaticABP.abp_defs]
EQfD [axiom, in AxiomaticABP.abp_defs]
EQFf [axiom, in AxiomaticABP.abp_defs]
EQFi [axiom, in AxiomaticABP.abp_defs]
EQfi [axiom, in AxiomaticABP.abp_defs]
eqF1 [axiom, in AxiomaticABP.abp_defs]
eqf1 [axiom, in AxiomaticABP.abp_defs]
eqF2 [axiom, in AxiomaticABP.abp_defs]
eqf2 [axiom, in AxiomaticABP.abp_defs]
eqF3 [axiom, in AxiomaticABP.abp_defs]
eqf3 [axiom, in AxiomaticABP.abp_defs]
eqf4 [axiom, in AxiomaticABP.abp_defs]
eqF4 [axiom, in AxiomaticABP.abp_defs]
eqF5 [axiom, in AxiomaticABP.abp_defs]
eqf5 [axiom, in AxiomaticABP.abp_defs]
eqf6 [axiom, in AxiomaticABP.abp_defs]
eqF6 [axiom, in AxiomaticABP.abp_defs]
eqf7 [axiom, in AxiomaticABP.abp_defs]
eqF7 [axiom, in AxiomaticABP.abp_defs]
eqF8 [axiom, in AxiomaticABP.abp_defs]
eqf8 [axiom, in AxiomaticABP.abp_defs]
EQ_refl [axiom, in AxiomaticABP.abp_base]
EQ_sym [axiom, in AxiomaticABP.abp_base]
EXPH4_ [section, in AxiomaticABP.abp_base]
EXPH4_.H [variable, in AxiomaticABP.abp_base]
EXPH4_.u [variable, in AxiomaticABP.abp_base]
EXPH4_.x [variable, in AxiomaticABP.abp_base]
EXPH4_.y [variable, in AxiomaticABP.abp_base]
EXPH4_.z [variable, in AxiomaticABP.abp_base]
EXP2_ [section, in AxiomaticABP.abp_base]
EXP2_.x [variable, in AxiomaticABP.abp_base]
EXP2_.y [variable, in AxiomaticABP.abp_base]
EXP3_ [section, in AxiomaticABP.abp_base]
EXP3_.x [variable, in AxiomaticABP.abp_base]
EXP3_.y [variable, in AxiomaticABP.abp_base]
EXP3_.z [variable, in AxiomaticABP.abp_base]
EXTE [axiom, in AxiomaticABP.abp_base]
e0 [axiom, in AxiomaticABP.abp_defs]
e1 [axiom, in AxiomaticABP.abp_defs]

F

frame [axiom, in AxiomaticABP.abp_defs]
Frame [axiom, in AxiomaticABP.abp_defs]
FRAME1 [section, in AxiomaticABP.abp_defs]
FRAME1.b [variable, in AxiomaticABP.abp_defs]
FRAME1.b1 [variable, in AxiomaticABP.abp_defs]
FRAME1.b2 [variable, in AxiomaticABP.abp_defs]
FRAME1.d [variable, in AxiomaticABP.abp_defs]
FRAME1.e [variable, in AxiomaticABP.abp_defs]
FRAME2 [section, in AxiomaticABP.abp_defs]
FRAME2.b [variable, in AxiomaticABP.abp_defs]
FRAME2.b1 [variable, in AxiomaticABP.abp_defs]
FRAME2.b2 [variable, in AxiomaticABP.abp_defs]
FRAME2.d [variable, in AxiomaticABP.abp_defs]
FRAME2.d1 [variable, in AxiomaticABP.abp_defs]
FRAME2.d2 [variable, in AxiomaticABP.abp_defs]
FRAME2.e [variable, in AxiomaticABP.abp_defs]
FRAME2.e' [variable, in AxiomaticABP.abp_defs]

G

gamma [definition, in AxiomaticABP.abp_base]
GRD [axiom, in AxiomaticABP.abp_base]
GUARDED [section, in AxiomaticABP.abp_base]
GUARDED.a [variable, in AxiomaticABP.abp_base]
GUARDED.B [variable, in AxiomaticABP.abp_base]
GUARDED.d [variable, in AxiomaticABP.abp_base]
GUARDED.D [variable, in AxiomaticABP.abp_base]
GUARDED.L [variable, in AxiomaticABP.abp_base]
GUARDED.x [variable, in AxiomaticABP.abp_base]
GUARDED.y [variable, in AxiomaticABP.abp_base]
GUARDED.z [variable, in AxiomaticABP.abp_base]
G10 [axiom, in AxiomaticABP.abp_base]
G11 [axiom, in AxiomaticABP.abp_base]
G12 [axiom, in AxiomaticABP.abp_base]
G13 [axiom, in AxiomaticABP.abp_base]
G2 [axiom, in AxiomaticABP.abp_base]
G5 [axiom, in AxiomaticABP.abp_base]
G6 [axiom, in AxiomaticABP.abp_base]
G7 [axiom, in AxiomaticABP.abp_base]
G8 [axiom, in AxiomaticABP.abp_base]
G9 [axiom, in AxiomaticABP.abp_base]

H

H [definition, in AxiomaticABP.abp_defs]
Handshaking [axiom, in AxiomaticABP.abp_base]
HIDE [section, in AxiomaticABP.abp_base]
hide [axiom, in AxiomaticABP.abp_base]
HIDE.a [variable, in AxiomaticABP.abp_base]
HIDE.e [variable, in AxiomaticABP.abp_base]
HIDE.E [variable, in AxiomaticABP.abp_base]
HIDE.L [variable, in AxiomaticABP.abp_base]
HIDE.x [variable, in AxiomaticABP.abp_base]
HIDE.y [variable, in AxiomaticABP.abp_base]

I

i [constructor, in AxiomaticABP.abp_base]
ia [axiom, in AxiomaticABP.abp_base]
ifD [axiom, in AxiomaticABP.abp_defs]
iff [axiom, in AxiomaticABP.abp_defs]
ifF [axiom, in AxiomaticABP.abp_defs]
int [constructor, in AxiomaticABP.abp_base]
In_ehlist [definition, in AxiomaticABP.abp_base]
In_list [definition, in AxiomaticABP.abp_base]
I' [definition, in AxiomaticABP.abp_defs]
I'' [definition, in AxiomaticABP.abp_defs]

K

K [axiom, in AxiomaticABP.abp_defs]
KFAR2 [axiom, in AxiomaticABP.abp_base]

L

L [axiom, in AxiomaticABP.abp_defs]
lce [axiom, in AxiomaticABP.abp_defs]
Lem1 [lemma, in AxiomaticABP.abp_lem2]
Lem10 [lemma, in AxiomaticABP.abp_lem25]
Lem11 [lemma, in AxiomaticABP.abp_lem25]
Lem12 [lemma, in AxiomaticABP.abp_lem25]
Lem13 [lemma, in AxiomaticABP.abp_lem25]
Lem14 [lemma, in AxiomaticABP.abp_lem25]
Lem15 [lemma, in AxiomaticABP.abp_lem25]
Lem16 [lemma, in AxiomaticABP.abp_lem25]
Lem17 [lemma, in AxiomaticABP.abp_lem25]
Lem18 [lemma, in AxiomaticABP.abp_lem25]
Lem19 [lemma, in AxiomaticABP.abp_lem25]
Lem2 [lemma, in AxiomaticABP.abp_lem2]
Lem20 [lemma, in AxiomaticABP.abp_lem3]
Lem21 [lemma, in AxiomaticABP.abp_lem3]
Lem3 [lemma, in AxiomaticABP.abp_lem2]
Lem4 [lemma, in AxiomaticABP.abp_lem2]
Lem5 [lemma, in AxiomaticABP.abp_lem2]
Lem6 [lemma, in AxiomaticABP.abp_lem2]
Lem7 [lemma, in AxiomaticABP.abp_lem2]
Lem8 [lemma, in AxiomaticABP.abp_lem2]
Lem9 [lemma, in AxiomaticABP.abp_lem2]
Lin2' [axiom, in AxiomaticABP.abp_proc]
Lin3' [axiom, in AxiomaticABP.abp_proc]
Lin5' [axiom, in AxiomaticABP.abp_proc]
Lin6' [axiom, in AxiomaticABP.abp_proc]
list [inductive, in AxiomaticABP.abp_base]
Lmer [axiom, in AxiomaticABP.abp_base]

M

mer [axiom, in AxiomaticABP.abp_base]

N

nil [constructor, in AxiomaticABP.abp_base]
notb [axiom, in AxiomaticABP.abp_defs]
notb1 [axiom, in AxiomaticABP.abp_defs]
notb2 [axiom, in AxiomaticABP.abp_defs]

O

one [inductive, in AxiomaticABP.abp_base]
orb [axiom, in AxiomaticABP.abp_defs]
orb1 [axiom, in AxiomaticABP.abp_defs]
orb2 [axiom, in AxiomaticABP.abp_defs]

P

PARALLEL_OPERATORS [section, in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.a [variable, in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.b [variable, in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.E [variable, in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.e [variable, in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.f [variable, in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.F [variable, in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.x [variable, in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.y [variable, in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.z [variable, in AxiomaticABP.abp_base]
PROC [section, in AxiomaticABP.abp_defs]
proc [axiom, in AxiomaticABP.abp_base]
ProcR [axiom, in AxiomaticABP.abp_defs]
ProcRn [axiom, in AxiomaticABP.abp_defs]
ProcS [axiom, in AxiomaticABP.abp_defs]
ProcSn [axiom, in AxiomaticABP.abp_defs]
ProcSn_d [axiom, in AxiomaticABP.abp_defs]
ProcTn_d [axiom, in AxiomaticABP.abp_defs]
PROC.b [variable, in AxiomaticABP.abp_defs]
PROC.d [variable, in AxiomaticABP.abp_defs]
PROC.j [variable, in AxiomaticABP.abp_defs]

R

R [axiom, in AxiomaticABP.abp_defs]
Rn [axiom, in AxiomaticABP.abp_defs]
RSP [axiom, in AxiomaticABP.abp_base]
r1 [constructor, in AxiomaticABP.abp_base]
r2 [constructor, in AxiomaticABP.abp_base]
r3 [constructor, in AxiomaticABP.abp_base]
r5 [constructor, in AxiomaticABP.abp_base]
r6 [constructor, in AxiomaticABP.abp_base]

S

S [axiom, in AxiomaticABP.abp_defs]
sce [axiom, in AxiomaticABP.abp_defs]
SC1 [axiom, in AxiomaticABP.abp_base]
SC3 [axiom, in AxiomaticABP.abp_base]
SC4 [axiom, in AxiomaticABP.abp_base]
SC5 [axiom, in AxiomaticABP.abp_base]
seq [axiom, in AxiomaticABP.abp_base]
Sn [axiom, in AxiomaticABP.abp_defs]
Sn_d [axiom, in AxiomaticABP.abp_defs]
Specificat [axiom, in AxiomaticABP.abp_proc]
STANDARD_CONCURRENCY [section, in AxiomaticABP.abp_base]
STANDARD_CONCURRENCY.x [variable, in AxiomaticABP.abp_base]
STANDARD_CONCURRENCY.y [variable, in AxiomaticABP.abp_base]
STANDARD_CONCURRENCY.z [variable, in AxiomaticABP.abp_base]
sum [axiom, in AxiomaticABP.abp_base]
SUM [section, in AxiomaticABP.abp_base]
SUM.D [variable, in AxiomaticABP.abp_base]
SUM.d [variable, in AxiomaticABP.abp_base]
SUM.L [variable, in AxiomaticABP.abp_base]
SUM.p [variable, in AxiomaticABP.abp_base]
SUM.x [variable, in AxiomaticABP.abp_base]
SUM.y [variable, in AxiomaticABP.abp_base]
SUM1 [axiom, in AxiomaticABP.abp_base]
SUM3 [axiom, in AxiomaticABP.abp_base]
SUM4 [axiom, in AxiomaticABP.abp_base]
SUM5 [axiom, in AxiomaticABP.abp_base]
SUM6 [axiom, in AxiomaticABP.abp_base]
SUM7 [axiom, in AxiomaticABP.abp_base]
SUM8 [axiom, in AxiomaticABP.abp_base]
SUM9 [axiom, in AxiomaticABP.abp_base]
s2 [constructor, in AxiomaticABP.abp_base]
s3 [constructor, in AxiomaticABP.abp_base]
s4 [constructor, in AxiomaticABP.abp_base]
s5 [constructor, in AxiomaticABP.abp_base]
s6 [constructor, in AxiomaticABP.abp_base]

T

tau [constructor, in AxiomaticABP.abp_base]
TI1 [axiom, in AxiomaticABP.abp_base]
TI2 [axiom, in AxiomaticABP.abp_base]
TI3 [axiom, in AxiomaticABP.abp_base]
TI4 [axiom, in AxiomaticABP.abp_base]
TI5 [axiom, in AxiomaticABP.abp_base]
Tn_d [axiom, in AxiomaticABP.abp_defs]
toggle [axiom, in AxiomaticABP.abp_defs]
Toggle1 [axiom, in AxiomaticABP.abp_defs]
Toggle2 [axiom, in AxiomaticABP.abp_defs]
Tuple [axiom, in AxiomaticABP.abp_defs]
tuple [axiom, in AxiomaticABP.abp_defs]
T1 [axiom, in AxiomaticABP.abp_base]

X

X [definition, in AxiomaticABP.abp_defs]
X' [axiom, in AxiomaticABP.abp_proc]
X1 [definition, in AxiomaticABP.abp_defs]
X1' [axiom, in AxiomaticABP.abp_proc]
X2 [definition, in AxiomaticABP.abp_defs]
X2' [axiom, in AxiomaticABP.abp_proc]

Y

Y [definition, in AxiomaticABP.abp_defs]
Y' [axiom, in AxiomaticABP.abp_proc]
Y1 [definition, in AxiomaticABP.abp_defs]
Y1' [axiom, in AxiomaticABP.abp_proc]
Y2 [definition, in AxiomaticABP.abp_defs]
Y2' [axiom, in AxiomaticABP.abp_proc]

Section Index

B

BIT [in AxiomaticABP.abp_defs]
BOOL [in AxiomaticABP.abp_defs]
BPA [in AxiomaticABP.abp_base]

C

COMMUNICATION_F [in AxiomaticABP.abp_base]
CONDITION [in AxiomaticABP.abp_base]

D

DATA [in AxiomaticABP.abp_defs]

E

ENCAPSULATION [in AxiomaticABP.abp_base]
EXPH4_ [in AxiomaticABP.abp_base]
EXP2_ [in AxiomaticABP.abp_base]
EXP3_ [in AxiomaticABP.abp_base]

F

FRAME1 [in AxiomaticABP.abp_defs]
FRAME2 [in AxiomaticABP.abp_defs]

G

GUARDED [in AxiomaticABP.abp_base]

H

HIDE [in AxiomaticABP.abp_base]

P

PARALLEL_OPERATORS [in AxiomaticABP.abp_base]
PROC [in AxiomaticABP.abp_defs]

S

STANDARD_CONCURRENCY [in AxiomaticABP.abp_base]
SUM [in AxiomaticABP.abp_base]

Lemma Index

C

Comms3L [in AxiomaticABP.abp_lem1]
Comms3Rn_b [in AxiomaticABP.abp_lem1]
Comms3Rn_b' [in AxiomaticABP.abp_lem1]
Comms3Rn_lce [in AxiomaticABP.abp_lem1]
Comms3Tn_d [in AxiomaticABP.abp_lem1]
CommTn_dRn [in AxiomaticABP.abp_lem1]

L

Lem1 [in AxiomaticABP.abp_lem2]
Lem10 [in AxiomaticABP.abp_lem25]
Lem11 [in AxiomaticABP.abp_lem25]
Lem12 [in AxiomaticABP.abp_lem25]
Lem13 [in AxiomaticABP.abp_lem25]
Lem14 [in AxiomaticABP.abp_lem25]
Lem15 [in AxiomaticABP.abp_lem25]
Lem16 [in AxiomaticABP.abp_lem25]
Lem17 [in AxiomaticABP.abp_lem25]
Lem18 [in AxiomaticABP.abp_lem25]
Lem19 [in AxiomaticABP.abp_lem25]
Lem2 [in AxiomaticABP.abp_lem2]
Lem20 [in AxiomaticABP.abp_lem3]
Lem21 [in AxiomaticABP.abp_lem3]
Lem3 [in AxiomaticABP.abp_lem2]
Lem4 [in AxiomaticABP.abp_lem2]
Lem5 [in AxiomaticABP.abp_lem2]
Lem6 [in AxiomaticABP.abp_lem2]
Lem7 [in AxiomaticABP.abp_lem2]
Lem8 [in AxiomaticABP.abp_lem2]
Lem9 [in AxiomaticABP.abp_lem2]

Constructor Index

C

cons [in AxiomaticABP.abp_base]
c2 [in AxiomaticABP.abp_base]
c3 [in AxiomaticABP.abp_base]
c5 [in AxiomaticABP.abp_base]
c6 [in AxiomaticABP.abp_base]

D

delta [in AxiomaticABP.abp_base]

E

ehcons [in AxiomaticABP.abp_base]
ehnil [in AxiomaticABP.abp_base]

I

i [in AxiomaticABP.abp_base]
int [in AxiomaticABP.abp_base]

N

nil [in AxiomaticABP.abp_base]

R

r1 [in AxiomaticABP.abp_base]
r2 [in AxiomaticABP.abp_base]
r3 [in AxiomaticABP.abp_base]
r5 [in AxiomaticABP.abp_base]
r6 [in AxiomaticABP.abp_base]

S

s2 [in AxiomaticABP.abp_base]
s3 [in AxiomaticABP.abp_base]
s4 [in AxiomaticABP.abp_base]
s5 [in AxiomaticABP.abp_base]
s6 [in AxiomaticABP.abp_base]

T

tau [in AxiomaticABP.abp_base]

Inductive Index

A

act [in AxiomaticABP.abp_base]

E

ehlist [in AxiomaticABP.abp_base]

L

list [in AxiomaticABP.abp_base]

O

one [in AxiomaticABP.abp_base]

Definition Index

A

ABP [in AxiomaticABP.abp_defs]

D

Delta [in AxiomaticABP.abp_base]

G

gamma [in AxiomaticABP.abp_base]

H

H [in AxiomaticABP.abp_defs]

I

In_ehlist [in AxiomaticABP.abp_base]
In_list [in AxiomaticABP.abp_base]
I' [in AxiomaticABP.abp_defs]
I'' [in AxiomaticABP.abp_defs]

X

X [in AxiomaticABP.abp_defs]
X1 [in AxiomaticABP.abp_defs]
X2 [in AxiomaticABP.abp_defs]

Y

Y [in AxiomaticABP.abp_defs]
Y1 [in AxiomaticABP.abp_defs]
Y2 [in AxiomaticABP.abp_defs]

Axiom Index

A

alt [in AxiomaticABP.abp_base]
andb [in AxiomaticABP.abp_defs]
andb1 [in AxiomaticABP.abp_defs]
andb2 [in AxiomaticABP.abp_defs]
A1 [in AxiomaticABP.abp_base]
A2 [in AxiomaticABP.abp_base]
A3 [in AxiomaticABP.abp_base]
A4 [in AxiomaticABP.abp_base]
A5 [in AxiomaticABP.abp_base]
A6 [in AxiomaticABP.abp_base]
A7 [in AxiomaticABP.abp_base]

B

B [in AxiomaticABP.abp_proc]
bit [in AxiomaticABP.abp_defs]
bit1 [in AxiomaticABP.abp_defs]
bit2 [in AxiomaticABP.abp_defs]
bit3 [in AxiomaticABP.abp_defs]

C

CF1 [in AxiomaticABP.abp_base]
CF2 [in AxiomaticABP.abp_base]
CF2' [in AxiomaticABP.abp_base]
CF2'' [in AxiomaticABP.abp_base]
ChanK [in AxiomaticABP.abp_defs]
ChanL [in AxiomaticABP.abp_defs]
CM1 [in AxiomaticABP.abp_base]
CM2 [in AxiomaticABP.abp_base]
CM3 [in AxiomaticABP.abp_base]
CM4 [in AxiomaticABP.abp_base]
CM5 [in AxiomaticABP.abp_base]
CM6 [in AxiomaticABP.abp_base]
CM7 [in AxiomaticABP.abp_base]
CM8 [in AxiomaticABP.abp_base]
CM9 [in AxiomaticABP.abp_base]
comm [in AxiomaticABP.abp_base]
cond [in AxiomaticABP.abp_base]
COND1 [in AxiomaticABP.abp_base]
COND2 [in AxiomaticABP.abp_base]

D

D [in AxiomaticABP.abp_defs]
D1 [in AxiomaticABP.abp_base]
D2 [in AxiomaticABP.abp_base]
D3 [in AxiomaticABP.abp_base]
D4 [in AxiomaticABP.abp_base]
D5 [in AxiomaticABP.abp_base]

E

enc [in AxiomaticABP.abp_base]
EQ [in AxiomaticABP.abp_base]
eqb [in AxiomaticABP.abp_defs]
eqD [in AxiomaticABP.abp_defs]
EQDi [in AxiomaticABP.abp_defs]
eqD5 [in AxiomaticABP.abp_defs]
eqD6 [in AxiomaticABP.abp_defs]
eqD7 [in AxiomaticABP.abp_defs]
eqD8 [in AxiomaticABP.abp_defs]
eqF [in AxiomaticABP.abp_defs]
eqf [in AxiomaticABP.abp_defs]
EQFD [in AxiomaticABP.abp_defs]
EQfD [in AxiomaticABP.abp_defs]
EQFf [in AxiomaticABP.abp_defs]
EQFi [in AxiomaticABP.abp_defs]
EQfi [in AxiomaticABP.abp_defs]
eqF1 [in AxiomaticABP.abp_defs]
eqf1 [in AxiomaticABP.abp_defs]
eqF2 [in AxiomaticABP.abp_defs]
eqf2 [in AxiomaticABP.abp_defs]
eqF3 [in AxiomaticABP.abp_defs]
eqf3 [in AxiomaticABP.abp_defs]
eqf4 [in AxiomaticABP.abp_defs]
eqF4 [in AxiomaticABP.abp_defs]
eqF5 [in AxiomaticABP.abp_defs]
eqf5 [in AxiomaticABP.abp_defs]
eqf6 [in AxiomaticABP.abp_defs]
eqF6 [in AxiomaticABP.abp_defs]
eqf7 [in AxiomaticABP.abp_defs]
eqF7 [in AxiomaticABP.abp_defs]
eqF8 [in AxiomaticABP.abp_defs]
eqf8 [in AxiomaticABP.abp_defs]
EQ_refl [in AxiomaticABP.abp_base]
EQ_sym [in AxiomaticABP.abp_base]
EXTE [in AxiomaticABP.abp_base]
e0 [in AxiomaticABP.abp_defs]
e1 [in AxiomaticABP.abp_defs]

F

frame [in AxiomaticABP.abp_defs]
Frame [in AxiomaticABP.abp_defs]

G

GRD [in AxiomaticABP.abp_base]
G10 [in AxiomaticABP.abp_base]
G11 [in AxiomaticABP.abp_base]
G12 [in AxiomaticABP.abp_base]
G13 [in AxiomaticABP.abp_base]
G2 [in AxiomaticABP.abp_base]
G5 [in AxiomaticABP.abp_base]
G6 [in AxiomaticABP.abp_base]
G7 [in AxiomaticABP.abp_base]
G8 [in AxiomaticABP.abp_base]
G9 [in AxiomaticABP.abp_base]

H

Handshaking [in AxiomaticABP.abp_base]
hide [in AxiomaticABP.abp_base]

I

ia [in AxiomaticABP.abp_base]
ifD [in AxiomaticABP.abp_defs]
iff [in AxiomaticABP.abp_defs]
ifF [in AxiomaticABP.abp_defs]

K

K [in AxiomaticABP.abp_defs]
KFAR2 [in AxiomaticABP.abp_base]

L

L [in AxiomaticABP.abp_defs]
lce [in AxiomaticABP.abp_defs]
Lin2' [in AxiomaticABP.abp_proc]
Lin3' [in AxiomaticABP.abp_proc]
Lin5' [in AxiomaticABP.abp_proc]
Lin6' [in AxiomaticABP.abp_proc]
Lmer [in AxiomaticABP.abp_base]

M

mer [in AxiomaticABP.abp_base]

N

notb [in AxiomaticABP.abp_defs]
notb1 [in AxiomaticABP.abp_defs]
notb2 [in AxiomaticABP.abp_defs]

O

orb [in AxiomaticABP.abp_defs]
orb1 [in AxiomaticABP.abp_defs]
orb2 [in AxiomaticABP.abp_defs]

P

proc [in AxiomaticABP.abp_base]
ProcR [in AxiomaticABP.abp_defs]
ProcRn [in AxiomaticABP.abp_defs]
ProcS [in AxiomaticABP.abp_defs]
ProcSn [in AxiomaticABP.abp_defs]
ProcSn_d [in AxiomaticABP.abp_defs]
ProcTn_d [in AxiomaticABP.abp_defs]

R

R [in AxiomaticABP.abp_defs]
Rn [in AxiomaticABP.abp_defs]
RSP [in AxiomaticABP.abp_base]

S

S [in AxiomaticABP.abp_defs]
sce [in AxiomaticABP.abp_defs]
SC1 [in AxiomaticABP.abp_base]
SC3 [in AxiomaticABP.abp_base]
SC4 [in AxiomaticABP.abp_base]
SC5 [in AxiomaticABP.abp_base]
seq [in AxiomaticABP.abp_base]
Sn [in AxiomaticABP.abp_defs]
Sn_d [in AxiomaticABP.abp_defs]
Specificat [in AxiomaticABP.abp_proc]
sum [in AxiomaticABP.abp_base]
SUM1 [in AxiomaticABP.abp_base]
SUM3 [in AxiomaticABP.abp_base]
SUM4 [in AxiomaticABP.abp_base]
SUM5 [in AxiomaticABP.abp_base]
SUM6 [in AxiomaticABP.abp_base]
SUM7 [in AxiomaticABP.abp_base]
SUM8 [in AxiomaticABP.abp_base]
SUM9 [in AxiomaticABP.abp_base]

T

TI1 [in AxiomaticABP.abp_base]
TI2 [in AxiomaticABP.abp_base]
TI3 [in AxiomaticABP.abp_base]
TI4 [in AxiomaticABP.abp_base]
TI5 [in AxiomaticABP.abp_base]
Tn_d [in AxiomaticABP.abp_defs]
toggle [in AxiomaticABP.abp_defs]
Toggle1 [in AxiomaticABP.abp_defs]
Toggle2 [in AxiomaticABP.abp_defs]
Tuple [in AxiomaticABP.abp_defs]
tuple [in AxiomaticABP.abp_defs]
T1 [in AxiomaticABP.abp_base]

X

X' [in AxiomaticABP.abp_proc]
X1' [in AxiomaticABP.abp_proc]
X2' [in AxiomaticABP.abp_proc]

Y

Y' [in AxiomaticABP.abp_proc]
Y1' [in AxiomaticABP.abp_proc]
Y2' [in AxiomaticABP.abp_proc]

Variable Index

B

BIT.b [in AxiomaticABP.abp_defs]
BOOL.b [in AxiomaticABP.abp_defs]
BPA.x [in AxiomaticABP.abp_base]
BPA.y [in AxiomaticABP.abp_base]
BPA.z [in AxiomaticABP.abp_base]

C

COMMUNICATION_F.a [in AxiomaticABP.abp_base]
COMMUNICATION_F.b [in AxiomaticABP.abp_base]
COMMUNICATION_F.E [in AxiomaticABP.abp_base]
COMMUNICATION_F.e [in AxiomaticABP.abp_base]
COMMUNICATION_F.e1 [in AxiomaticABP.abp_base]
COMMUNICATION_F.e2 [in AxiomaticABP.abp_base]
COMMUNICATION_F.F [in AxiomaticABP.abp_base]
COMMUNICATION_F.f [in AxiomaticABP.abp_base]
CONDITION.x [in AxiomaticABP.abp_base]
CONDITION.y [in AxiomaticABP.abp_base]

D

DATA.d [in AxiomaticABP.abp_defs]
DATA.e [in AxiomaticABP.abp_defs]

E

ENCAPSULATION.a [in AxiomaticABP.abp_base]
ENCAPSULATION.e [in AxiomaticABP.abp_base]
ENCAPSULATION.E [in AxiomaticABP.abp_base]
ENCAPSULATION.L [in AxiomaticABP.abp_base]
ENCAPSULATION.x [in AxiomaticABP.abp_base]
ENCAPSULATION.y [in AxiomaticABP.abp_base]
EXPH4_.H [in AxiomaticABP.abp_base]
EXPH4_.u [in AxiomaticABP.abp_base]
EXPH4_.x [in AxiomaticABP.abp_base]
EXPH4_.y [in AxiomaticABP.abp_base]
EXPH4_.z [in AxiomaticABP.abp_base]
EXP2_.x [in AxiomaticABP.abp_base]
EXP2_.y [in AxiomaticABP.abp_base]
EXP3_.x [in AxiomaticABP.abp_base]
EXP3_.y [in AxiomaticABP.abp_base]
EXP3_.z [in AxiomaticABP.abp_base]

F

FRAME1.b [in AxiomaticABP.abp_defs]
FRAME1.b1 [in AxiomaticABP.abp_defs]
FRAME1.b2 [in AxiomaticABP.abp_defs]
FRAME1.d [in AxiomaticABP.abp_defs]
FRAME1.e [in AxiomaticABP.abp_defs]
FRAME2.b [in AxiomaticABP.abp_defs]
FRAME2.b1 [in AxiomaticABP.abp_defs]
FRAME2.b2 [in AxiomaticABP.abp_defs]
FRAME2.d [in AxiomaticABP.abp_defs]
FRAME2.d1 [in AxiomaticABP.abp_defs]
FRAME2.d2 [in AxiomaticABP.abp_defs]
FRAME2.e [in AxiomaticABP.abp_defs]
FRAME2.e' [in AxiomaticABP.abp_defs]

G

GUARDED.a [in AxiomaticABP.abp_base]
GUARDED.B [in AxiomaticABP.abp_base]
GUARDED.d [in AxiomaticABP.abp_base]
GUARDED.D [in AxiomaticABP.abp_base]
GUARDED.L [in AxiomaticABP.abp_base]
GUARDED.x [in AxiomaticABP.abp_base]
GUARDED.y [in AxiomaticABP.abp_base]
GUARDED.z [in AxiomaticABP.abp_base]

H

HIDE.a [in AxiomaticABP.abp_base]
HIDE.e [in AxiomaticABP.abp_base]
HIDE.E [in AxiomaticABP.abp_base]
HIDE.L [in AxiomaticABP.abp_base]
HIDE.x [in AxiomaticABP.abp_base]
HIDE.y [in AxiomaticABP.abp_base]

P

PARALLEL_OPERATORS.a [in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.b [in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.E [in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.e [in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.f [in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.F [in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.x [in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.y [in AxiomaticABP.abp_base]
PARALLEL_OPERATORS.z [in AxiomaticABP.abp_base]
PROC.b [in AxiomaticABP.abp_defs]
PROC.d [in AxiomaticABP.abp_defs]
PROC.j [in AxiomaticABP.abp_defs]

S

STANDARD_CONCURRENCY.x [in AxiomaticABP.abp_base]
STANDARD_CONCURRENCY.y [in AxiomaticABP.abp_base]
STANDARD_CONCURRENCY.z [in AxiomaticABP.abp_base]
SUM.D [in AxiomaticABP.abp_base]
SUM.d [in AxiomaticABP.abp_base]
SUM.L [in AxiomaticABP.abp_base]
SUM.p [in AxiomaticABP.abp_base]
SUM.x [in AxiomaticABP.abp_base]
SUM.y [in AxiomaticABP.abp_base]

Library Index

A

abp_base
abp_defs
abp_lem1
abp_lem2
abp_lem25
abp_lem3
abp_proc

Global Index

J

Q

U

V

W

Z

_

(333 entries)

Section Index

A

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(18 entries)

Lemma Index

A

B

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(27 entries)

Constructor Index

A

B

F

G

H

J

K

L

M

O

P

Q

U

V

W

X

Y

Z

_

(22 entries)

Inductive Index

B

C

D

F

G

H

I

J

K

M

N

P

Q

R

S

T

U

V

W

X

Y

Z

_

(4 entries)

Definition Index

B

C

E

F

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

Z

_

(14 entries)

Axiom Index

J

Q

U

V

W

Z

_

(160 entries)

Variable Index

A

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(81 entries)

Library Index

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

_

(7 entries)