Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
From Coq Require Import Program.Equality.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits.

Utility: Properties of Possibly-Infinite Traces

The property encodings and many specific properties are adapted from the paper A Hoare logic for the coinductive trace-based big-step semantics of While .
Section sec_trace_properties.

Context {A B : Type}.

#[local] Notation trace := (@trace A B).
We want to reason about trace properties that do not distinguish bisimilar traces; these are called setoid properties.
Definition setoidT (p : trace -> Prop) :=
forall tr0, p tr0 -> forall tr1, bisim tr0 tr1 -> p tr1.

Definition propT := { p : trace -> Prop | setoidT p }.

Infiniteness property

CoInductive infiniteT : trace -> Prop :=
| infiniteT_delay : forall a b tr,
   infiniteT tr ->
   infiniteT (Tcons a b tr).

A, B: Type

setoidT infiniteT
A, B: Type

setoidT infiniteT
A, B: Type
CIH: setoidT infiniteT

setoidT infiniteT
A, B: Type
CIH: setoidT infiniteT
a: A
b: B
tr, tr': trace
H: infiniteT tr
H4: bisim tr tr'

infiniteT (Tcons a b tr')
exact: (infiniteT_delay a b (CIH _ H _ H4)). Qed. Definition InfiniteT : propT := exist _ (fun tr => infiniteT tr) infiniteT_setoidT.
A, B: Type

forall (a : A) (b : B) (tr : trace), infiniteT (Tcons a b tr) -> infiniteT tr
A, B: Type

forall (a : A) (b : B) (tr : trace), infiniteT (Tcons a b tr) -> infiniteT tr
by move => a b tr Hinf; inversion Hinf. Qed.
A, B: Type

forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr' +++ tr)
A, B: Type

forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr' +++ tr)
A, B: Type
CIH: forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr' +++ tr)

forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr' +++ tr)
A, B: Type
CIH: forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr' +++ tr)
tr: trace
Htr: infiniteT tr

forall tr' : trace, infiniteT (tr' +++ tr)
A, B: Type
CIH: forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr' +++ tr)
tr: trace
Htr: infiniteT tr
a: A
b: B
tr': trace

infiniteT (Tcons a b tr' +++ tr)
A, B: Type
CIH: forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr' +++ tr)
tr: trace
Htr: infiniteT tr
a: A
b: B
tr': trace

infiniteT (Tcons a b (tr' +++ tr))
exact/infiniteT_delay/CIH. Qed.
A, B: Type

forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr +++ tr')
A, B: Type

forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr +++ tr')
A, B: Type
CIH: forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr +++ tr')

forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr +++ tr')
A, B: Type
CIH: forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr +++ tr')
a: A
b: B
tr0: trace
Hinf: infiniteT (Tcons a b tr0)
H0: infiniteT tr0
tr': trace

infiniteT (Tcons a b tr0 +++ tr')
A, B: Type
CIH: forall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr +++ tr')
a: A
b: B
tr0: trace
Hinf: infiniteT (Tcons a b tr0)
H0: infiniteT tr0
tr': trace

infiniteT (Tcons a b (tr0 +++ tr'))
exact/infiniteT_delay/CIH. Qed.

Finiteness property

Inductive finiteT : trace -> Prop :=
| finiteT_nil : forall a,
   finiteT (Tnil a)
| finiteT_delay : forall (a : A) (b : B) tr,
   finiteT tr ->
   finiteT (Tcons a b tr).

A, B: Type

setoidT finiteT
A, B: Type

setoidT finiteT
A, B: Type
tr1: trace
a: A

finiteT (Tnil a)
A, B: Type
tr1: trace
a: A
b: B
tr1': trace
Hfin: finiteT tr1'
IH: forall tr1 : trace, bisim tr1' tr1 -> finiteT tr1
tr': trace
H3: bisim tr1' tr'
finiteT (Tcons a b tr')
A, B: Type
tr1: trace
a: A

finiteT (Tnil a)
A, B: Type
tr1: trace
a: A
b: B
tr1': trace
Hfin: finiteT tr1'
IH: forall tr1 : trace, bisim tr1' tr1 -> finiteT tr1
tr': trace
H3: bisim tr1' tr'
finiteT (Tcons a b tr')
A, B: Type
tr1: trace
a: A
b: B
tr1': trace
Hfin: finiteT tr1'
IH: forall tr1 : trace, bisim tr1' tr1 -> finiteT tr1
tr': trace
H3: bisim tr1' tr'

finiteT (Tcons a b tr')
A, B: Type
tr1: trace
a: A
b: B
tr1': trace
Hfin: finiteT tr1'
IH: forall tr1 : trace, bisim tr1' tr1 -> finiteT tr1
tr': trace
H3: bisim tr1' tr'

finiteT (Tcons a b tr')
exact/finiteT_delay/IH. Qed. Definition FiniteT : propT := exist _ (fun tr => finiteT tr) finiteT_setoidT.
A, B: Type
a: A
b: B
tr: trace
h: finiteT (Tcons a b tr)

finiteT tr
A, B: Type
a: A
b: B
tr: trace
h: finiteT (Tcons a b tr)

finiteT tr
by inversion h. Defined.
Equality coincides with bisimilarity for finite traces.
A, B: Type

forall tr : trace, finiteT tr -> forall tr' : trace, bisim tr tr' -> tr = tr'
A, B: Type

forall tr : trace, finiteT tr -> forall tr' : trace, bisim tr tr' -> tr = tr'
A, B: Type
tr: trace
a: A
b: B
tr0: trace
Hfin: finiteT tr0
IH: forall tr' : trace, bisim tr0 tr' -> tr0 = tr'
tr'0: trace
H3: bisim tr0 tr'0

Tcons a b tr0 = Tcons a b tr'0
by rewrite (IH _ H3). Qed.
Basic connections between finiteness and infiniteness.
A, B: Type

forall tr : trace, finiteT tr -> infiniteT tr -> False
A, B: Type

forall tr : trace, finiteT tr -> infiniteT tr -> False
by move => tr; elim => [a | a b tr' Hfin IH] Hinf; inversion Hinf. Qed.
A, B: Type

forall tr : trace, ~ finiteT tr -> infiniteT tr
A, B: Type

forall tr : trace, ~ finiteT tr -> infiniteT tr
A, B: Type
CIH: forall tr : trace, ~ finiteT tr -> infiniteT tr

forall tr : trace, ~ finiteT tr -> infiniteT tr
A, B: Type
CIH: forall tr : trace, ~ finiteT tr -> infiniteT tr
a: A
b: B
tr: trace
Hfin: ~ finiteT (Tcons a b tr)

infiniteT (Tcons a b tr)
A, B: Type
CIH: forall tr : trace, ~ finiteT tr -> infiniteT tr
a: A
b: B
tr: trace
Hfin: ~ finiteT (Tcons a b tr)

infiniteT tr
A, B: Type
a: A
b: B
tr: trace
Hfin: ~ finiteT (Tcons a b tr)
Hinf: finiteT tr

False
A, B: Type
a: A
b: B
tr: trace
Hinf: finiteT tr

finiteT (Tcons a b tr)
exact: finiteT_delay. Qed.

Final element properties

Inductive finalTA : trace -> A -> Prop :=
| finalTA_nil : forall a,
   finalTA (Tnil a) a
| finalTA_delay : forall a b a' tr,
   finalTA tr a' ->
   finalTA (Tcons a b tr) a'.

Inductive finalTB : trace -> B -> Prop :=
| finalTB_nil : forall a b a',
   finalTB (Tcons a b (Tnil a')) b
| finalTB_delay : forall a b b' tr,
   finalTB tr b' ->
   finalTB (Tcons a b tr) b'.

A, B: Type

forall (tr : trace) (a : A), finalTA tr a -> finiteT tr
A, B: Type

forall (tr : trace) (a : A), finalTA tr a -> finiteT tr
A, B: Type
tr: trace
a, a1: A

finiteT (Tnil a1)
A, B: Type
tr: trace
a, a1: A
b: B
a2: A
tr': trace
Hfinal: finalTA tr' a2
IH: finiteT tr'
finiteT (Tcons a1 b tr')
A, B: Type
tr: trace
a, a1: A

finiteT (Tnil a1)
A, B: Type
tr: trace
a, a1: A
b: B
a2: A
tr': trace
Hfinal: finalTA tr' a2
IH: finiteT tr'
finiteT (Tcons a1 b tr')
A, B: Type
tr: trace
a, a1: A
b: B
a2: A
tr': trace
Hfinal: finalTA tr' a2
IH: finiteT tr'

finiteT (Tcons a1 b tr')
A, B: Type
tr: trace
a, a1: A
b: B
a2: A
tr': trace
Hfinal: finalTA tr' a2
IH: finiteT tr'

finiteT (Tcons a1 b tr')
exact/finiteT_delay/IH. Qed.
A, B: Type

forall (tr : trace) (b : B), finalTB tr b -> finiteT tr
A, B: Type

forall (tr : trace) (b : B), finalTB tr b -> finiteT tr
A, B: Type
tr: trace
b: B
a1: A
b1: B
a2: A

finiteT (Tcons a1 b1 (Tnil a2))
A, B: Type
tr: trace
b: B
a1: A
b1, b2: B
a2: trace
Hfin: finalTB a2 b2
IH: finiteT a2
finiteT (Tcons a1 b1 a2)
A, B: Type
tr: trace
b: B
a1: A
b1: B
a2: A

finiteT (Tcons a1 b1 (Tnil a2))
A, B: Type
tr: trace
b: B
a1: A
b1, b2: B
a2: trace
Hfin: finalTB a2 b2
IH: finiteT a2
finiteT (Tcons a1 b1 a2)
A, B: Type
tr: trace
b: B
a1: A
b1, b2: B
a2: trace
Hfin: finalTB a2 b2
IH: finiteT a2

finiteT (Tcons a1 b1 a2)
A, B: Type
tr: trace
b: B
a1: A
b1, b2: B
a2: trace
Hfin: finalTB a2 b2
IH: finiteT a2

finiteT (Tcons a1 b1 a2)
exact: finiteT_delay. Qed. Fixpoint finalA (tr : trace) (h : finiteT tr) {struct h} : A := match tr as tr' return (finiteT tr' -> A) with | Tnil a => fun _ => a | Tcons a b tr => fun h => finalA (invert_finiteT_delay h) end h.
A, B: Type

forall (tr : trace) (h : finiteT tr), finalTA tr (finalA h)
A, B: Type

forall (tr : trace) (h : finiteT tr), finalTA tr (finalA h)
A, B: Type
IH: forall (tr : trace) (h : finiteT tr), finalTA tr (finalA h)
tr: trace
h: finiteT tr

finalTA tr (finalA h)
A, B: Type
IH: forall (tr : trace) (h : finiteT tr), finalTA tr (finalA h)
a: A
h: finiteT (Tnil a)
a0: A
H0: a0 = a

finalTA (Tnil a) a
A, B: Type
IH: forall (tr : trace) (h : finiteT tr), finalTA tr (finalA h)
a: A
b: B
tr: trace
h: finiteT (Tcons a b tr)
a0: A
b0: B
tr0: trace
f: finiteT tr
H0: a0 = a
H1: b0 = b
H2: tr0 = tr
finalTA (Tcons a b tr) (finalA (eq_ind_r (fun _ : A => b = b -> tr = tr -> finiteT tr -> finiteT tr) (fun H1 : b = b => eq_ind_r (fun _ : B => tr = tr -> finiteT tr -> finiteT tr) (fun H2 : tr = tr => eq_ind_r (fun t : trace => finiteT t -> finiteT tr) (fun H0 : finiteT tr => H0) H2) H1) eq_refl eq_refl eq_refl f))
A, B: Type
IH: forall (tr : trace) (h : finiteT tr), finalTA tr (finalA h)
a: A
h: finiteT (Tnil a)
a0: A
H0: a0 = a

finalTA (Tnil a) a
A, B: Type
IH: forall (tr : trace) (h : finiteT tr), finalTA tr (finalA h)
a: A
b: B
tr: trace
h: finiteT (Tcons a b tr)
a0: A
b0: B
tr0: trace
f: finiteT tr
H0: a0 = a
H1: b0 = b
H2: tr0 = tr
finalTA (Tcons a b tr) (finalA (eq_ind_r (fun _ : A => b = b -> tr = tr -> finiteT tr -> finiteT tr) (fun H1 : b = b => eq_ind_r (fun _ : B => tr = tr -> finiteT tr -> finiteT tr) (fun H2 : tr = tr => eq_ind_r (fun t : trace => finiteT t -> finiteT tr) (fun H0 : finiteT tr => H0) H2) H1) eq_refl eq_refl eq_refl f))
A, B: Type
IH: forall (tr : trace) (h : finiteT tr), finalTA tr (finalA h)
a: A
b: B
tr: trace
h: finiteT (Tcons a b tr)
a0: A
b0: B
tr0: trace
f: finiteT tr
H0: a0 = a
H1: b0 = b
H2: tr0 = tr

finalTA (Tcons a b tr) (finalA (eq_ind_r (fun _ : A => b = b -> tr = tr -> finiteT tr -> finiteT tr) (fun H1 : b = b => eq_ind_r (fun _ : B => tr = tr -> finiteT tr -> finiteT tr) (fun H2 : tr = tr => eq_ind_r (fun t : trace => finiteT t -> finiteT tr) (fun H0 : finiteT tr => H0) H2) H1) eq_refl eq_refl eq_refl f))
A, B: Type
IH: forall (tr : trace) (h : finiteT tr), finalTA tr (finalA h)
a: A
b: B
tr: trace
h: finiteT (Tcons a b tr)
a0: A
b0: B
tr0: trace
f: finiteT tr
H0: a0 = a
H1: b0 = b
H2: tr0 = tr

finalTA (Tcons a b tr) (finalA (eq_ind_r (fun _ : A => b = b -> tr = tr -> finiteT tr -> finiteT tr) (fun H1 : b = b => eq_ind_r (fun _ : B => tr = tr -> finiteT tr -> finiteT tr) (fun H2 : tr = tr => eq_ind_r (fun t : trace => finiteT t -> finiteT tr) (fun H0 : finiteT tr => H0) H2) H1) eq_refl eq_refl eq_refl f))
exact: finalTA_delay. Qed.
A, B: Type

forall (tr0 : trace) (a : A), finalTA tr0 a -> forall tr1 : trace, hd tr1 = a -> hd (tr0 +++ tr1) = hd tr0
A, B: Type

forall (tr0 : trace) (a : A), finalTA tr0 a -> forall tr1 : trace, hd tr1 = a -> hd (tr0 +++ tr1) = hd tr0
by move => tr a; elim => {tr a} [a tr <- | a b a' tr Hfinal IH tr'] //=. Qed.

Basic trace properties and connectives

Definition ttT : trace -> Prop := fun tr => True.

A, B: Type

setoidT ttT
A, B: Type

setoidT ttT
by []. Qed. Definition TtT : propT := exist _ ttT ttT_setoidT. Definition ffT : trace -> Prop := fun tr => False.
A, B: Type

setoidT ffT
A, B: Type

setoidT ffT
by []. Qed. Definition FfT : propT := exist _ ffT ffT_setoidT. Definition notT (p : trace -> Prop) : trace -> Prop := fun tr => ~ p tr.
A, B: Type

forall p : trace -> Prop, setoidT p -> setoidT (notT p)
A, B: Type

forall p : trace -> Prop, setoidT p -> setoidT (notT p)
A, B: Type
p: trace -> Prop
hp: setoidT p
tr: trace
h1: notT p tr
tr': trace
h2: bisim tr tr'
h3: p tr'

False
A, B: Type
p: trace -> Prop
hp: setoidT p
tr, tr': trace
h2: bisim tr tr'
h3: p tr'

p tr
apply: hp _ h3 _ (bisim_sym h2). Qed. Definition NotT (p : propT) : propT := let: exist f hf := p in exist _ (notT f) (notT_setoidT hf). Definition satisfyT (p : propT) : trace -> Prop := fun tr => let: exist f0 h0 := p in f0 tr. Program Definition ExT {T : Type} (p : T -> propT) : propT := exist _ (fun tr => exists x, satisfyT (p x) tr) _.
A, B, T: Type
p: T -> propT

setoidT (fun tr : trace => exists x : T, satisfyT (p x) tr)
A, B, T: Type
p: T -> propT

setoidT (fun tr : trace => exists x : T, satisfyT (p x) tr)
A, B, T: Type
p: T -> propT
tr0: trace
x: T
h0: satisfyT (p x) tr0
tr1: trace
h1: bisim tr0 tr1

exists x : T, satisfyT (p x) tr1
A, B, T: Type
p: T -> propT
tr0: trace
x: T
h0: satisfyT (p x) tr0
tr1: trace
h1: bisim tr0 tr1

satisfyT (p x) tr1
A, B, T: Type
p: T -> propT
tr0: trace
x: T
tr1: trace
h1: bisim tr0 tr1
f0: trace -> Prop
h2: setoidT f0
h0: f0 tr0

f0 tr1
exact: h2 _ h0 _ h1. Defined.
A, B: Type

forall f0 f1 : trace -> Prop, setoidT f0 -> setoidT f1 -> setoidT (fun tr : trace => f0 tr /\ f1 tr)
A, B: Type

forall f0 f1 : trace -> Prop, setoidT f0 -> setoidT f1 -> setoidT (fun tr : trace => f0 tr /\ f1 tr)
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f0 tr0
h3: f1 tr0
tr1: trace
h4: bisim tr0 tr1

f0 tr1
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f0 tr0
h3: f1 tr0
tr1: trace
h4: bisim tr0 tr1
f1 tr1
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f0 tr0
h3: f1 tr0
tr1: trace
h4: bisim tr0 tr1

f0 tr1
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f0 tr0
h3: f1 tr0
tr1: trace
h4: bisim tr0 tr1
f1 tr1
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f0 tr0
h3: f1 tr0
tr1: trace
h4: bisim tr0 tr1

f1 tr1
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f0 tr0
h3: f1 tr0
tr1: trace
h4: bisim tr0 tr1

f1 tr1
exact: h1 _ h3 _ h4. Qed. Definition AndT (p1 p2 : propT) : propT := let: exist f0 h0 := p1 in let: exist f1 h1 := p2 in exist _ (fun tr => f0 tr /\ f1 tr) (andT_setoidT h0 h1).
Identifier 'andT' now a keyword
A, B: Type

forall f0 f1 : trace -> Prop, setoidT f0 -> setoidT f1 -> setoidT (fun tr : trace => f0 tr \/ f1 tr)
A, B: Type

forall f0 f1 : trace -> Prop, setoidT f0 -> setoidT f1 -> setoidT (fun tr : trace => f0 tr \/ f1 tr)
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f0 tr0
tr1: trace
h3: bisim tr0 tr1

f0 tr1 \/ f1 tr1
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f1 tr0
tr1: trace
h3: bisim tr0 tr1
f0 tr1 \/ f1 tr1
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f0 tr0
tr1: trace
h3: bisim tr0 tr1

f0 tr1 \/ f1 tr1
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f1 tr0
tr1: trace
h3: bisim tr0 tr1
f0 tr1 \/ f1 tr1
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f1 tr0
tr1: trace
h3: bisim tr0 tr1

f0 tr1 \/ f1 tr1
A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f1 tr0
tr1: trace
h3: bisim tr0 tr1

f0 tr1 \/ f1 tr1
by right; apply: h1 _ h2 _ h3. Qed. Definition OrT (p1 p2 : propT) : propT := let: exist f0 h0 := p1 in let: exist f1 h1 := p2 in exist _ (fun tr => f0 tr \/ f1 tr) (orT_setoidT h0 h1).
Identifier 'orT' now a keyword
Definition propT_imp (p1 p2 : propT) : Prop := forall tr, satisfyT p1 tr -> satisfyT p2 tr. #[local] Infix "=>>" := propT_imp (at level 60, right associativity).
A, B: Type

forall p0 p1 q : propT, p0 =>> p1 -> p1 =>> q -> p0 =>> q
A, B: Type

forall p0 p1 q : propT, p0 =>> p1 -> p1 =>> q -> p0 =>> q
A, B: Type
p0: trace -> Prop
hp0: setoidT p0
p1: trace -> Prop
hp1: setoidT p1
q: trace -> Prop
hq: setoidT q
h0: exist (fun p : trace -> Prop => setoidT p) p0 hp0 =>> exist (fun p : trace -> Prop => setoidT p) p1 hp1
h1: exist (fun p : trace -> Prop => setoidT p) p1 hp1 =>> exist (fun p : trace -> Prop => setoidT p) q hq
tr0: trace
h2: p0 tr0

q tr0
exact/h1/h0. Qed.
A, B: Type

forall p q0 q1 : propT, q0 =>> q1 -> p =>> q0 -> p =>> q1
A, B: Type

forall p q0 q1 : propT, q0 =>> q1 -> p =>> q0 -> p =>> q1
A, B: Type
p: trace -> Prop
hp: setoidT p
q0: trace -> Prop
hq0: setoidT q0
q1: trace -> Prop
hq1: setoidT q1
h0: exist (fun p : trace -> Prop => setoidT p) q0 hq0 =>> exist (fun p : trace -> Prop => setoidT p) q1 hq1
h1: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q0 hq0
tr0: trace
h2: p tr0

q1 tr0
exact/h0/h1. Qed.
A, B: Type

forall p q0 q1 : propT, p =>> q0 -> p =>> q1 -> p =>> q0 andT q1
A, B: Type

forall p q0 q1 : propT, p =>> q0 -> p =>> q1 -> p =>> q0 andT q1
A, B: Type
p: trace -> Prop
hp: setoidT p
q0: trace -> Prop
hq0: setoidT q0
q1: trace -> Prop
hq1: setoidT q1
h0: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q0 hq0
h1: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q1 hq1
tr0: trace
h2: p tr0

q0 tr0 /\ q1 tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
q0: trace -> Prop
hq0: setoidT q0
q1: trace -> Prop
hq1: setoidT q1
h0: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q0 hq0
h1: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q1 hq1
tr0: trace
h2: p tr0

q0 tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
q0: trace -> Prop
hq0: setoidT q0
q1: trace -> Prop
hq1: setoidT q1
h0: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q0 hq0
h1: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q1 hq1
tr0: trace
h2: p tr0
q1 tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
q0: trace -> Prop
hq0: setoidT q0
q1: trace -> Prop
hq1: setoidT q1
h0: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q0 hq0
h1: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q1 hq1
tr0: trace
h2: p tr0

q0 tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
q0: trace -> Prop
hq0: setoidT q0
q1: trace -> Prop
hq1: setoidT q1
h0: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q0 hq0
h1: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q1 hq1
tr0: trace
h2: p tr0
q1 tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
q0: trace -> Prop
hq0: setoidT q0
q1: trace -> Prop
hq1: setoidT q1
h0: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q0 hq0
h1: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q1 hq1
tr0: trace
h2: p tr0

q1 tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
q0: trace -> Prop
hq0: setoidT q0
q1: trace -> Prop
hq1: setoidT q1
h0: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q0 hq0
h1: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q1 hq1
tr0: trace
h2: p tr0

q1 tr0
exact: h1. Qed.
A, B: Type

forall p : propT, p =>> p
A, B: Type

forall p : propT, p =>> p
by move => p. Qed.
A, B: Type

forall p0 p1 : propT, p0 =>> p1 -> forall tr : trace, satisfyT p0 tr -> satisfyT p1 tr
A, B: Type

forall p0 p1 : propT, p0 =>> p1 -> forall tr : trace, satisfyT p0 tr -> satisfyT p1 tr
A, B: Type
f0: trace -> Prop
h0: setoidT f0
f1: trace -> Prop
h1: setoidT f1
h2: exist (fun p : trace -> Prop => setoidT p) f0 h0 =>> exist (fun p : trace -> Prop => setoidT p) f1 h1
tr: trace
h3: f0 tr

f1 tr
exact: h2. Qed.
A, B: Type

forall p q r : propT, p =>> q -> q =>> r -> p =>> r
A, B: Type

forall p q r : propT, p =>> q -> q =>> r -> p =>> r
A, B: Type
p, q, r: propT
h0: p =>> q
h1: q =>> r
tr0: trace
h2: satisfyT p tr0

satisfyT r tr0
exact/(satisfyT_cont h1)/(satisfyT_cont h0 h2). Qed.
A, B: Type

forall p1 p2 : propT, p1 =>> p1 orT p2
A, B: Type

forall p1 p2 : propT, p1 =>> p1 orT p2
by move => [f1 hf1] [f2 hf2] tr /= h1; left. Qed.
A, B: Type

forall p1 p2 : propT, p2 =>> p1 orT p2
A, B: Type

forall p1 p2 : propT, p2 =>> p1 orT p2
by move => [f1 hf1] [f2 hf2] tr /= h1; right. Qed.

Basic trace element properties and connectives

Definition propA := A -> Prop.

Definition ttA : propA := fun a => True.

Definition ffA : propA := fun a => False.

Definition propA_imp (u1 u2 : propA) : Prop := forall a, u1 a -> u2 a.

#[local] Infix "->>" := propA_imp (at level 60, right associativity).

Definition andA (u1 u2 : propA) : propA := fun a => u1 a /\ u2 a.

Identifier 'andA' now a keyword
Definition exA {T : Type} (u : T -> propA) : propA := fun st => exists x, u x st.

Singleton property

Definition singletonT (u : propA) : trace -> Prop :=
fun tr => exists a, u a /\ bisim tr (Tnil a).

A, B: Type

forall (u : propA) (a : A), u a -> singletonT u (Tnil a)
A, B: Type

forall (u : propA) (a : A), u a -> singletonT u (Tnil a)
by move => u st h0; exists st; split; last by apply: bisim_refl. Qed.
A, B: Type

forall u : propA, setoidT (singletonT u)
A, B: Type

forall u : propA, setoidT (singletonT u)
A, B: Type
u: propA
a: A
h0: u a

singletonT u (Tnil a)
exact: nil_singletonT. Qed.
A, B: Type

forall u v : propA, u ->> v -> forall tr : trace, singletonT u tr -> singletonT v tr
A, B: Type

forall u v : propA, u ->> v -> forall tr : trace, singletonT u tr -> singletonT v tr
A, B: Type
u, v: propA
huv: u ->> v
a: A
h0: u a

singletonT v (Tnil a)
exact/nil_singletonT/huv. Qed.
A, B: Type

forall (u : propA) (a : A), singletonT u (Tnil a) -> u a
A, B: Type

forall (u : propA) (a : A), singletonT u (Tnil a) -> u a
by move => u st [a [h0 h1]]; invs h1. Qed. Definition SingletonT (u : propA) : propT := exist _ (singletonT u) (@singletonT_setoidT u). #[local] Notation "[| p |]" := (SingletonT p) (at level 80).
A, B: Type

forall u v : propA, u ->> v -> ([|u|]) =>> ([|v|])
A, B: Type

forall u v : propA, u ->> v -> ([|u|]) =>> ([|v|])
A, B: Type
u, v: propA
h0: u ->> v
a: A
h1: u a

satisfyT ([|v|]) (Tnil a)
exact/nil_singletonT/h0. Qed.

Duplicate element property

Definition dupT (u : propA) (b : B) : trace -> Prop :=
fun tr => exists a, u a /\ bisim tr (Tcons a b (Tnil a)).

A, B: Type

forall (u : propA) (a : A) (b : B), u a -> dupT u b (Tcons a b (Tnil a))
A, B: Type

forall (u : propA) (a : A) (b : B), u a -> dupT u b (Tcons a b (Tnil a))
A, B: Type
u: propA
a: A
b: B
h: u a

dupT u b (Tcons a b (Tnil a))
by exists a; split; [apply: h | apply: bisim_refl]. Qed.
A, B: Type

forall (u0 u1 : propA) (b : B), u0 ->> u1 -> forall tr : trace, dupT u0 b tr -> dupT u1 b tr
A, B: Type

forall (u0 u1 : propA) (b : B), u0 ->> u1 -> forall tr : trace, dupT u0 b tr -> dupT u1 b tr
A, B: Type
u0, u1: propA
b: B
hu: u0 ->> u1
a: A
h0: u0 a

dupT u1 b (Tcons a b (Tnil a))
exact/dupT_Tcons/hu. Qed.
A, B: Type

forall (u : propA) (b : B), setoidT (dupT u b)
A, B: Type

forall (u : propA) (b : B), setoidT (dupT u b)
A, B: Type
u: propA
b: B
tr0: trace
a: A
h0: u a
h1: bisim tr0 (Tcons a b (Tnil a))
tr1: trace
h2: bisim tr0 tr1

dupT u b tr1
A, B: Type
u: propA
b: B
a: A
h0: u a

dupT u b (Tcons a b (Tnil a))
exact/dupT_Tcons. Qed. Definition DupT (u : propA) (b : B) : propT := exist _ (dupT u b) (@dupT_setoidT u b). #[local] Notation "<< p ; b >>" := (DupT p b) (at level 80).
A, B: Type

forall (u v : propA) (b : B), u ->> v -> (<< u; b >>) =>> (<< v; b >>)
A, B: Type

forall (u v : propA) (b : B), u ->> v -> (<< u; b >>) =>> (<< v; b >>)
A, B: Type
u, v: propA
b: B
h0: u ->> v
tr0: trace

dupT u b tr0 -> dupT v b tr0
exact: dupT_cont. Qed.

Follows property

The follows property holds for two traces when the first is a prefix of the second, and p holds for the suffix.
CoInductive followsT (p : trace -> Prop) : trace -> trace -> Prop :=
| followsT_nil : forall a tr,
   hd tr = a ->
   p tr ->
   followsT p (Tnil a) tr
| followsT_delay : forall a b tr tr',
   followsT p tr tr' ->
   followsT p (Tcons a b tr) (Tcons a b tr').

A, B: Type

forall (p : trace -> Prop) (tr0 tr1 : trace), followsT p tr0 tr1 -> hd tr0 = hd tr1
A, B: Type

forall (p : trace -> Prop) (tr0 tr1 : trace), followsT p tr0 tr1 -> hd tr0 = hd tr1
by move => p tr0 tr1 h0; invs h0. Qed.
A, B: Type

forall (p : trace -> Prop) (tr0 tr1 : trace), followsT p tr0 tr1 -> {tr : trace & {a : A | tr0 = Tnil a /\ hd tr = a /\ p tr}} + {tr : trace & {tr' : trace & {a : A & {b : B | tr0 = Tcons a b tr /\ tr1 = Tcons a b tr' /\ followsT p tr tr'}}}}
A, B: Type

forall (p : trace -> Prop) (tr0 tr1 : trace), followsT p tr0 tr1 -> {tr : trace & {a : A | tr0 = Tnil a /\ hd tr = a /\ p tr}} + {tr : trace & {tr' : trace & {a : A & {b : B | tr0 = Tcons a b tr /\ tr1 = Tcons a b tr' /\ followsT p tr tr'}}}}
A, B: Type
p: trace -> Prop
a: A
tr1: trace
h: followsT p (Tnil a) tr1

({tr : trace & {a0 : A | Tnil a = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a0 : A & {b : B | Tnil a = Tcons a0 b tr /\ tr1 = Tcons a0 b tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
b: B
tr0, tr1: trace
h: followsT p (Tcons a b tr0) tr1
({tr : trace & {a0 : A | Tcons a b tr0 = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a0 : A & {b0 : B | Tcons a b tr0 = Tcons a0 b0 tr /\ tr1 = Tcons a0 b0 tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
tr1: trace
h: followsT p (Tnil a) tr1

({tr : trace & {a0 : A | Tnil a = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a0 : A & {b : B | Tnil a = Tcons a0 b tr /\ tr1 = Tcons a0 b tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
b: B
tr0, tr1: trace
h: followsT p (Tcons a b tr0) tr1
({tr : trace & {a0 : A | Tcons a b tr0 = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a0 : A & {b0 : B | Tcons a b tr0 = Tcons a0 b0 tr /\ tr1 = Tcons a0 b0 tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
b: B
tr0, tr1: trace
h: followsT p (Tcons a b tr0) tr1

({tr : trace & {a0 : A | Tcons a b tr0 = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a0 : A & {b0 : B | Tcons a b tr0 = Tcons a0 b0 tr /\ tr1 = Tcons a0 b0 tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
b: B
tr0, tr1: trace
h: followsT p (Tcons a b tr0) tr1

({tr : trace & {a0 : A | Tcons a b tr0 = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a0 : A & {b0 : B | Tcons a b tr0 = Tcons a0 b0 tr /\ tr1 = Tcons a0 b0 tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
b: B
tr0: trace
a0: A
h: followsT p (Tcons a b tr0) (Tnil a0)

({tr : trace & {a0 : A | Tcons a b tr0 = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a1 : A & {b0 : B | Tcons a b tr0 = Tcons a1 b0 tr /\ Tnil a0 = Tcons a1 b0 tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
b: B
tr0: trace
a0: A
b0: B
tr1: trace
h: followsT p (Tcons a b tr0) (Tcons a0 b0 tr1)
({tr : trace & {a0 : A | Tcons a b tr0 = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a1 : A & {b1 : B | Tcons a b tr0 = Tcons a1 b1 tr /\ Tcons a0 b0 tr1 = Tcons a1 b1 tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
b: B
tr0: trace
a0: A
h: followsT p (Tcons a b tr0) (Tnil a0)

({tr : trace & {a0 : A | Tcons a b tr0 = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a1 : A & {b0 : B | Tcons a b tr0 = Tcons a1 b0 tr /\ Tnil a0 = Tcons a1 b0 tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
b: B
tr0: trace
a0: A
b0: B
tr1: trace
h: followsT p (Tcons a b tr0) (Tcons a0 b0 tr1)
({tr : trace & {a0 : A | Tcons a b tr0 = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a1 : A & {b1 : B | Tcons a b tr0 = Tcons a1 b1 tr /\ Tcons a0 b0 tr1 = Tcons a1 b1 tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
b: B
tr0: trace
a0: A
b0: B
tr1: trace
h: followsT p (Tcons a b tr0) (Tcons a0 b0 tr1)

({tr : trace & {a0 : A | Tcons a b tr0 = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a1 : A & {b1 : B | Tcons a b tr0 = Tcons a1 b1 tr /\ Tcons a0 b0 tr1 = Tcons a1 b1 tr' /\ followsT p tr tr'}}}})%type
A, B: Type
p: trace -> Prop
a: A
b: B
tr0: trace
a0: A
b0: B
tr1: trace
h: followsT p (Tcons a b tr0) (Tcons a0 b0 tr1)

({tr : trace & {a0 : A | Tcons a b tr0 = Tnil a0 /\ hd tr = a0 /\ p tr}} + {tr : trace & {tr' : trace & {a1 : A & {b1 : B | Tcons a b tr0 = Tcons a1 b1 tr /\ Tcons a0 b0 tr1 = Tcons a1 b1 tr' /\ followsT p tr tr'}}}})%type
by right; exists tr0, tr1, a, b; inversion h. Defined.
A, B: Type

forall p : trace -> Prop, (forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1) -> forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
A, B: Type

forall p : trace -> Prop, (forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1) -> forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1

forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3

forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
tr1, tr2: trace
h1: bisim (Tnil (hd tr1)) tr2
tr3: trace
h2: bisim tr1 tr3
H0: p tr1

followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
a: A
b: B
tr, tr', tr2: trace
h1: bisim (Tcons a b tr) tr2
tr3: trace
h2: bisim (Tcons a b tr') tr3
H: followsT p tr tr'
followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
tr1, tr2: trace
h1: bisim (Tnil (hd tr1)) tr2
tr3: trace
h2: bisim tr1 tr3
H0: p tr1

followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
a: A
b: B
tr, tr', tr2: trace
h1: bisim (Tcons a b tr) tr2
tr3: trace
h2: bisim (Tcons a b tr') tr3
H: followsT p tr tr'
followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
tr1, tr3: trace
h2: bisim tr1 tr3
H0: p tr1

followsT p (Tnil (hd tr1)) tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
a: A
b: B
tr, tr', tr2: trace
h1: bisim (Tcons a b tr) tr2
tr3: trace
h2: bisim (Tcons a b tr') tr3
H: followsT p tr tr'
followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
tr1, tr3: trace
h2: bisim tr1 tr3
H0: p tr1
h0: hd tr1 = hd tr3

followsT p (Tnil (hd tr1)) tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
a: A
b: B
tr, tr', tr2: trace
h1: bisim (Tcons a b tr) tr2
tr3: trace
h2: bisim (Tcons a b tr') tr3
H: followsT p tr tr'
followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
tr1, tr3: trace
h2: bisim tr1 tr3
H0: p tr1
h0: hd tr3 = hd tr1

followsT p (Tnil (hd tr1)) tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
a: A
b: B
tr, tr', tr2: trace
h1: bisim (Tcons a b tr) tr2
tr3: trace
h2: bisim (Tcons a b tr') tr3
H: followsT p tr tr'
followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
a: A
b: B
tr, tr', tr2: trace
h1: bisim (Tcons a b tr) tr2
tr3: trace
h2: bisim (Tcons a b tr') tr3
H: followsT p tr tr'

followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
a: A
b: B
tr, tr', tr2: trace
h1: bisim (Tcons a b tr) tr2
tr3: trace
h2: bisim (Tcons a b tr') tr3
H: followsT p tr tr'

followsT p tr2 tr3
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3
a: A
b: B
tr, tr', tr'1, tr'0: trace
H: followsT p tr tr'
H4: bisim tr' tr'0
H5: bisim tr tr'1

followsT p (Tcons a b tr'1) (Tcons a b tr'0)
exact: (followsT_delay a b (CIH _ _ H _ H5 _ H4)). Qed.
A, B: Type

forall (p : trace -> Prop) (tr0 tr1 : trace), followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1
A, B: Type

forall (p : trace -> Prop) (tr0 tr1 : trace), followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1
A, B: Type
p: trace -> Prop

forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1

forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1
tr0: trace
H0: p tr0

followsT p (Tnil (hd tr0)) tr0
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1
a: A
b: B
tr2, tr', tr'0: trace
H: followsT p tr2 tr'
H4: bisim tr2 tr'0
followsT p (Tcons a b tr'0) (Tcons a b tr')
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1
tr0: trace
H0: p tr0

followsT p (Tnil (hd tr0)) tr0
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1
a: A
b: B
tr2, tr', tr'0: trace
H: followsT p tr2 tr'
H4: bisim tr2 tr'0
followsT p (Tcons a b tr'0) (Tcons a b tr')
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1
a: A
b: B
tr2, tr', tr'0: trace
H: followsT p tr2 tr'
H4: bisim tr2 tr'0

followsT p (Tcons a b tr'0) (Tcons a b tr')
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1
a: A
b: B
tr2, tr', tr'0: trace
H: followsT p tr2 tr'
H4: bisim tr2 tr'0

followsT p (Tcons a b tr'0) (Tcons a b tr')
exact: (followsT_delay a b (CIH _ _ H _ H4)). Qed.
A, B: Type

forall p : trace -> Prop, (forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1) -> forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
A, B: Type

forall p : trace -> Prop, (forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1) -> forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1

forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1

forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
tr0, tr1: trace
h1: bisim tr0 tr1
H0: p tr0

followsT p (Tnil (hd tr0)) tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
a: A
b: B
tr2, tr', tr1: trace
h1: bisim (Tcons a b tr') tr1
H: followsT p tr2 tr'
followsT p (Tcons a b tr2) tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
tr0, tr1: trace
h1: bisim tr0 tr1
H0: p tr0

followsT p (Tnil (hd tr0)) tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
a: A
b: B
tr2, tr', tr1: trace
h1: bisim (Tcons a b tr') tr1
H: followsT p tr2 tr'
followsT p (Tcons a b tr2) tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
tr0, tr1: trace
h1: bisim tr0 tr1
H0: p tr0

p tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
a: A
b: B
tr2, tr', tr1: trace
h1: bisim (Tcons a b tr') tr1
H: followsT p tr2 tr'
followsT p (Tcons a b tr2) tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
a: A
b: B
tr2, tr', tr1: trace
h1: bisim (Tcons a b tr') tr1
H: followsT p tr2 tr'

followsT p (Tcons a b tr2) tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
a: A
b: B
tr2, tr', tr1: trace
h1: bisim (Tcons a b tr') tr1
H: followsT p tr2 tr'

followsT p (Tcons a b tr2) tr1
A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1
CIH: forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1
a: A
b: B
tr2, tr', tr'0: trace
H: followsT p tr2 tr'
H4: bisim tr' tr'0

followsT p (Tcons a b tr2) (Tcons a b tr'0)
exact: (followsT_delay a b (CIH _ _ H _ H4)). Qed.
A, B: Type

forall p q : trace -> Prop, (forall tr : trace, p tr -> q tr) -> forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
A, B: Type

forall p q : trace -> Prop, (forall tr : trace, p tr -> q tr) -> forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q tr

forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q tr
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1

forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q tr
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
tr1: trace
H0: p tr1

followsT q (Tnil (hd tr1)) tr1
A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q tr
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
a: A
b: B
tr, tr': trace
H: followsT p tr tr'
followsT q (Tcons a b tr) (Tcons a b tr')
A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q tr
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
tr1: trace
H0: p tr1

followsT q (Tnil (hd tr1)) tr1
A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q tr
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
a: A
b: B
tr, tr': trace
H: followsT p tr tr'
followsT q (Tcons a b tr) (Tcons a b tr')
A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q tr
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
tr1: trace
H0: p tr1

q tr1
A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q tr
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
a: A
b: B
tr, tr': trace
H: followsT p tr tr'
followsT q (Tcons a b tr) (Tcons a b tr')
A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q tr
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
a: A
b: B
tr, tr': trace
H: followsT p tr tr'

followsT q (Tcons a b tr) (Tcons a b tr')
A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q tr
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1
a: A
b: B
tr, tr': trace
H: followsT p tr tr'

followsT q (Tcons a b tr) (Tcons a b tr')
exact/followsT_delay/CIH. Qed.
A, B: Type

forall (u : propA) (tr0 tr1 : trace), followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
A, B: Type

forall (u : propA) (tr0 tr1 : trace), followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
A, B: Type
u: propA

forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1

forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
tr1: trace
H0: singletonT u tr1

bisim (Tnil (hd tr1)) tr1
A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
a: A
b: B
tr, tr': trace
H: followsT (singletonT u) tr tr'
bisim (Tcons a b tr) (Tcons a b tr')
A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
tr1: trace
H0: singletonT u tr1

bisim (Tnil (hd tr1)) tr1
A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
a: A
b: B
tr, tr': trace
H: followsT (singletonT u) tr tr'
bisim (Tcons a b tr) (Tcons a b tr')
A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
a: A
h0: u a

bisim (Tnil a) (Tnil a)
A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
a: A
b: B
tr, tr': trace
H: followsT (singletonT u) tr tr'
bisim (Tcons a b tr) (Tcons a b tr')
A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
a: A
b: B
tr, tr': trace
H: followsT (singletonT u) tr tr'

bisim (Tcons a b tr) (Tcons a b tr')
A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
a: A
b: B
tr, tr': trace
H: followsT (singletonT u) tr tr'

bisim (Tcons a b tr) (Tcons a b tr')
exact/bisim_cons/CIH. Qed.
A, B: Type

forall (u0 u1 : propA) (tr0 : trace), followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
A, B: Type

forall (u0 u1 : propA) (tr0 : trace), followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
A, B: Type
u0, u1: propA

forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0

forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0

forall a : A, followsT (singletonT (u0 andA u1)) (Tnil a) (Tnil a) -> followsT (singletonT u0) (Tnil a) (Tnil a)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u0) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0

forall a : A, followsT (singletonT (u0 andA u1)) (Tnil a) (Tnil a) -> followsT (singletonT u0) (Tnil a) (Tnil a)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u0) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
a: A
h0: followsT (singletonT (u0 andA u1)) (Tnil a) (Tnil a)
a0: A
tr: trace
H0: hd (Tnil a) = a
H2: tr = Tnil a

followsT (singletonT u0) (Tnil a) (Tnil a)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u0) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
a, a0: A
H0: a = a
H1: hd (Tnil a) = a
H3: singletonT (u0 andA u1) (Tnil a)

followsT (singletonT u0) (Tnil a) (Tnil a)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u0) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
a, a0: A
H0: a = a
H1: hd (Tnil a) = a
a': A
h1: (u0 andA u1) a'
h2: bisim (Tnil a) (Tnil a')

followsT (singletonT u0) (Tnil a) (Tnil a)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u0) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
a0, a': A
H1: hd (Tnil a') = a'
H0: a' = a'
h1: (u0 andA u1) a'

followsT (singletonT u0) (Tnil a') (Tnil a')
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u0) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
a0, a': A
H1: hd (Tnil a') = a'
H0: a' = a'
h1: u0 a'
h2: u1 a'

followsT (singletonT u0) (Tnil a') (Tnil a')
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u0) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
a0, a': A
H1: hd (Tnil a') = a'
H0: a' = a'
h1: u0 a'
h2: u1 a'

singletonT u0 (Tnil a')
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u0) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0

forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u0) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0

forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u0) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0
a: A
b: B
tr0: trace
H0: followsT (singletonT (u0 andA u1)) tr0 tr0

followsT (singletonT u0) (Tcons a b tr0) (Tcons a b tr0)
exact/followsT_delay/CIH. Qed.
A, B: Type

forall (u0 u1 : propA) (tr0 : trace), followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
A, B: Type

forall (u0 u1 : propA) (tr0 : trace), followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
A, B: Type
u0, u1: propA

forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0

forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0

forall a : A, followsT (singletonT (u0 andA u1)) (Tnil a) (Tnil a) -> followsT (singletonT u1) (Tnil a) (Tnil a)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u1) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0

forall a : A, followsT (singletonT (u0 andA u1)) (Tnil a) (Tnil a) -> followsT (singletonT u1) (Tnil a) (Tnil a)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u1) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
a: A
h0: followsT (singletonT (u0 andA u1)) (Tnil a) (Tnil a)
a0: A
tr: trace
H0: hd (Tnil a) = a
H2: tr = Tnil a

followsT (singletonT u1) (Tnil a) (Tnil a)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u1) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
a, a0: A
H0: a = a
H1: hd (Tnil a) = a
H3: singletonT (u0 andA u1) (Tnil a)

followsT (singletonT u1) (Tnil a) (Tnil a)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u1) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
a, a0: A
H0: a = a
H1: hd (Tnil a) = a
a': A
h1: (u0 andA u1) a'
h2: bisim (Tnil a) (Tnil a')

followsT (singletonT u1) (Tnil a) (Tnil a)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u1) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
a0, a': A
H1: hd (Tnil a') = a'
H0: a' = a'
h1: (u0 andA u1) a'

followsT (singletonT u1) (Tnil a') (Tnil a')
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u1) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
a0, a': A
H1: hd (Tnil a') = a'
H0: a' = a'
h1: u0 a'
h2: u1 a'

followsT (singletonT u1) (Tnil a') (Tnil a')
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u1) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
a0, a': A
H1: hd (Tnil a') = a'
H0: a' = a'
h1: u0 a'
h2: u1 a'

singletonT u1 (Tnil a')
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u1) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0

forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u1) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0

forall (a : A) (b : B) (t : trace), followsT (singletonT (u0 andA u1)) (Tcons a b t) (Tcons a b t) -> followsT (singletonT u1) (Tcons a b t) (Tcons a b t)
A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0
a: A
b: B
tr0: trace
H0: followsT (singletonT (u0 andA u1)) tr0 tr0

followsT (singletonT u1) (Tcons a b tr0) (Tcons a b tr0)
exact/followsT_delay/CIH. Qed.
A, B: Type

forall (u v : propA) (tr : trace), followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
A, B: Type

forall (u v : propA) (tr : trace), followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
A, B: Type
u, v: propA

forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr

forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
a: A
H: hd (Tnil a) = a
H0: singletonT u (Tnil a)
H2: hd (Tnil a) = a
H3: singletonT v (Tnil a)

followsT (singletonT (u andA v)) (Tnil a) (Tnil a)
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
a: A
b: B
tr0: trace
H1: followsT (singletonT u) tr0 tr0
H0: followsT (singletonT v) tr0 tr0
followsT (singletonT (u andA v)) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
a: A
H: hd (Tnil a) = a
H0: singletonT u (Tnil a)
H2: hd (Tnil a) = a
H3: singletonT v (Tnil a)

followsT (singletonT (u andA v)) (Tnil a) (Tnil a)
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
a: A
b: B
tr0: trace
H1: followsT (singletonT u) tr0 tr0
H0: followsT (singletonT v) tr0 tr0
followsT (singletonT (u andA v)) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
a: A
H: hd (Tnil a) = a
H0: singletonT u (Tnil a)
H2: hd (Tnil a) = a
H3: singletonT v (Tnil a)

singletonT (u andA v) (Tnil a)
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
a: A
b: B
tr0: trace
H1: followsT (singletonT u) tr0 tr0
H0: followsT (singletonT v) tr0 tr0
followsT (singletonT (u andA v)) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
a: A
H: hd (Tnil a) = a
H0: singletonT u (Tnil a)
H2: hd (Tnil a) = a
H3: singletonT v (Tnil a)

(u andA v) a
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
a: A
b: B
tr0: trace
H1: followsT (singletonT u) tr0 tr0
H0: followsT (singletonT v) tr0 tr0
followsT (singletonT (u andA v)) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
a: A
b: B
tr0: trace
H1: followsT (singletonT u) tr0 tr0
H0: followsT (singletonT v) tr0 tr0

followsT (singletonT (u andA v)) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
u, v: propA
CIH: forall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr tr
a: A
b: B
tr0: trace
H1: followsT (singletonT u) tr0 tr0
H0: followsT (singletonT v) tr0 tr0

followsT (singletonT (u andA v)) (Tcons a b tr0) (Tcons a b tr0)
exact/followsT_delay/CIH. Qed.
A, B: Type

forall tr : trace, followsT (singletonT ttA) tr tr
A, B: Type

forall tr : trace, followsT (singletonT ttA) tr tr
A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr

forall tr : trace, followsT (singletonT ttA) tr tr
A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A

followsT (singletonT ttA) (Tnil a) (Tnil a)
A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A
b: B
tr0: trace
followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A

followsT (singletonT ttA) (Tnil a) (Tnil a)
A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A
b: B
tr0: trace
followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A

singletonT ttA (Tnil a)
A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A
b: B
tr0: trace
followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A
b: B
tr0: trace

followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A
b: B
tr0: trace

followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
exact/followsT_delay/CIH. Qed.

Append property

The append property holds for a trace whenever it has a prefix for which p1 holds, and p2 holds for the suffix.
Definition appendT (p1 p2 : trace -> Prop) : trace -> Prop :=
fun tr => exists tr', p1 tr' /\ followsT p2 tr' tr.

#[local] Infix "*+*" := appendT (at level 60, right associativity).

A, B: Type

forall p0 p1 q0 q1 : trace -> Prop, (forall tr : trace, p0 tr -> p1 tr) -> (forall tr : trace, q0 tr -> q1 tr) -> forall tr : trace, (p0 *+* q0) tr -> (p1 *+* q1) tr
A, B: Type

forall p0 p1 q0 q1 : trace -> Prop, (forall tr : trace, p0 tr -> p1 tr) -> (forall tr : trace, q0 tr -> q1 tr) -> forall tr : trace, (p0 *+* q0) tr -> (p1 *+* q1) tr
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
tr, tr0: trace
h0: p0 tr0
h1: followsT q0 tr0 tr

(p1 *+* q1) tr
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
tr, tr0: trace
h0: p0 tr0
h1: followsT q0 tr0 tr

followsT q1 tr0 tr
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr

forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
CIH: forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr

forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
CIH: forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr
tr1: trace
H0: q0 tr1

followsT q1 (Tnil (hd tr1)) tr1
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
CIH: forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr
a: A
b: B
tr, tr': trace
H: followsT q0 tr tr'
followsT q1 (Tcons a b tr) (Tcons a b tr')
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
CIH: forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr
tr1: trace
H0: q0 tr1

followsT q1 (Tnil (hd tr1)) tr1
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
CIH: forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr
a: A
b: B
tr, tr': trace
H: followsT q0 tr tr'
followsT q1 (Tcons a b tr) (Tcons a b tr')
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
CIH: forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr
tr1: trace
H0: q0 tr1

q1 tr1
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
CIH: forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr
a: A
b: B
tr, tr': trace
H: followsT q0 tr tr'
followsT q1 (Tcons a b tr) (Tcons a b tr')
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
CIH: forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr
a: A
b: B
tr, tr': trace
H: followsT q0 tr tr'

followsT q1 (Tcons a b tr) (Tcons a b tr')
A, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 tr
CIH: forall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 tr
a: A
b: B
tr, tr': trace
H: followsT q0 tr tr'

followsT q1 (Tcons a b tr) (Tcons a b tr')
exact/followsT_delay/CIH. Qed.
A, B: Type

forall p0 p1 q : trace -> Prop, (forall tr : trace, p0 tr -> p1 tr) -> forall tr : trace, (p0 *+* q) tr -> (p1 *+* q) tr
A, B: Type

forall p0 p1 q : trace -> Prop, (forall tr : trace, p0 tr -> p1 tr) -> forall tr : trace, (p0 *+* q) tr -> (p1 *+* q) tr
A, B: Type
p0, p1, q: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
tr: trace

(p0 *+* q) tr -> (p1 *+* q) tr
exact: (@appendT_cont _ _ q q hp _). Qed.
A, B: Type

forall p q0 q1 : trace -> Prop, (forall tr : trace, q0 tr -> q1 tr) -> forall tr : trace, (p *+* q0) tr -> (p *+* q1) tr
A, B: Type

forall p q0 q1 : trace -> Prop, (forall tr : trace, q0 tr -> q1 tr) -> forall tr : trace, (p *+* q0) tr -> (p *+* q1) tr
A, B: Type
p, q0, q1: trace -> Prop
hq: forall tr : trace, q0 tr -> q1 tr
tr: trace

(p *+* q0) tr -> (p *+* q1) tr
exact: (@appendT_cont p p _ _ _ hq). Qed.
A, B: Type

forall p0 p1 : trace -> Prop, setoidT p1 -> setoidT (p0 *+* p1)
A, B: Type

forall p0 p1 : trace -> Prop, setoidT p1 -> setoidT (p0 *+* p1)
A, B: Type
p0, p1: trace -> Prop
hp1: setoidT p1
tr0: trace
h0: (p0 *+* p1) tr0
tr1: trace
h1: bisim tr0 tr1

(p0 *+* p1) tr1
A, B: Type
p0, p1: trace -> Prop
hp1: setoidT p1
tr0, tr1: trace
h1: bisim tr0 tr1
tr2: trace
h0: p0 tr2
h2: followsT p1 tr2 tr0

(p0 *+* p1) tr1
A, B: Type
p0, p1: trace -> Prop
hp1: setoidT p1
tr0, tr1: trace
h1: bisim tr0 tr1
tr2: trace
h0: p0 tr2
h2: followsT p1 tr2 tr0

followsT p1 tr2 tr1
exact: (followsT_setoidT_R hp1 h2 h1). Qed.
A, B: Type

forall (p q : trace -> Prop) (tr0 tr1 tr2 : trace), followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
A, B: Type

forall (p q : trace -> Prop) (tr0 tr1 tr2 : trace), followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
A, B: Type
p, q: trace -> Prop

forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2

forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2

forall (a : A) (tr1 tr2 : trace), followsT p (Tnil a) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tnil a) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
forall (a : A) (b : B) (t tr1 tr2 : trace), followsT p (Tcons a b t) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tcons a b t) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2

forall (a : A) (tr1 tr2 : trace), followsT p (Tnil a) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tnil a) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
forall (a : A) (b : B) (t tr1 tr2 : trace), followsT p (Tcons a b t) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tcons a b t) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
tr1, tr2: trace
h1: followsT q tr1 tr2
H1: p tr1

followsT (p *+* q) (Tnil (hd tr1)) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
forall (a : A) (b : B) (t tr1 tr2 : trace), followsT p (Tcons a b t) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tcons a b t) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
tr1, tr2: trace
h1: followsT q tr1 tr2
H1: p tr1
h2: hd tr1 = hd tr2

followsT (p *+* q) (Tnil (hd tr1)) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
forall (a : A) (b : B) (t tr1 tr2 : trace), followsT p (Tcons a b t) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tcons a b t) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
tr1, tr2: trace
h1: followsT q tr1 tr2
H1: p tr1
h2: hd tr1 = hd tr2

(p *+* q) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
forall (a : A) (b : B) (t tr1 tr2 : trace), followsT p (Tcons a b t) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tcons a b t) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2

forall (a : A) (b : B) (t tr1 tr2 : trace), followsT p (Tcons a b t) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tcons a b t) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2

forall (a : A) (b : B) (t tr1 tr2 : trace), followsT p (Tcons a b t) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tcons a b t) tr2
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2
a: A
b: B
tr0, tr', tr'0: trace
H3: followsT p tr0 tr'
H4: followsT q tr' tr'0

followsT (p *+* q) (Tcons a b tr0) (Tcons a b tr'0)
exact: followsT_delay _ _ (CIH _ _ _ H3 H4). Qed.
A, B: Type

forall (p1 p2 p3 : trace -> Prop) (tr : trace), ((p1 *+* p2) *+* p3) tr -> (p1 *+* p2 *+* p3) tr
A, B: Type

forall (p1 p2 p3 : trace -> Prop) (tr : trace), ((p1 *+* p2) *+* p3) tr -> (p1 *+* p2 *+* p3) tr
A, B: Type
p1, p2, p3: trace -> Prop
tr0: trace
h1: ((p1 *+* p2) *+* p3) tr0

(p1 *+* p2 *+* p3) tr0
A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h1: (p1 *+* p2) tr1
h2: followsT p3 tr1 tr0

(p1 *+* p2 *+* p3) tr0
A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h2: followsT p3 tr1 tr0
tr2: trace
h1: p1 tr2 /\ followsT p2 tr2 tr1

(p1 *+* p2 *+* p3) tr0
A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h2: followsT p3 tr1 tr0
tr2: trace
h1: p1 tr2
h3: followsT p2 tr2 tr1

(p1 *+* p2 *+* p3) tr0
A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h2: followsT p3 tr1 tr0
tr2: trace
h3: followsT p2 tr2 tr1

followsT (p2 *+* p3) tr2 tr0
A, B: Type
p1, p2, p3: trace -> Prop

forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0

forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
tr1, tr2: trace
h1: followsT p3 tr2 tr1
H0: p2 tr2

followsT (p2 *+* p3) (Tnil (hd tr2)) tr1
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
tr1: trace
a: A
b: B
tr': trace
h1: followsT p3 (Tcons a b tr') tr1
tr: trace
H: followsT p2 tr tr'
followsT (p2 *+* p3) (Tcons a b tr) tr1
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
tr1, tr2: trace
h1: followsT p3 tr2 tr1
H0: p2 tr2

followsT (p2 *+* p3) (Tnil (hd tr2)) tr1
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
tr1: trace
a: A
b: B
tr': trace
h1: followsT p3 (Tcons a b tr') tr1
tr: trace
H: followsT p2 tr tr'
followsT (p2 *+* p3) (Tcons a b tr) tr1
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
tr1, tr2: trace
h1: followsT p3 tr2 tr1
H0: p2 tr2

hd tr1 = hd tr2
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
tr1: trace
a: A
b: B
tr': trace
h1: followsT p3 (Tcons a b tr') tr1
tr: trace
H: followsT p2 tr tr'
followsT (p2 *+* p3) (Tcons a b tr) tr1
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
tr1, tr2: trace
h1: followsT p3 tr2 tr1
H0: p2 tr2

hd tr2 = hd tr1
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
tr1: trace
a: A
b: B
tr': trace
h1: followsT p3 (Tcons a b tr') tr1
tr: trace
H: followsT p2 tr tr'
followsT (p2 *+* p3) (Tcons a b tr) tr1
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
tr1: trace
a: A
b: B
tr': trace
h1: followsT p3 (Tcons a b tr') tr1
tr: trace
H: followsT p2 tr tr'

followsT (p2 *+* p3) (Tcons a b tr) tr1
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
tr1: trace
a: A
b: B
tr': trace
h1: followsT p3 (Tcons a b tr') tr1
tr: trace
H: followsT p2 tr tr'

followsT (p2 *+* p3) (Tcons a b tr) tr1
A, B: Type
p1, p2, p3: trace -> Prop
CIH: forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0
a: A
b: B
tr', tr'0, tr: trace
H: followsT p2 tr tr'
H4: followsT p3 tr' tr'0

followsT (p2 *+* p3) (Tcons a b tr) (Tcons a b tr'0)
exact: followsT_delay _ _ (CIH _ _ _ H4 H). Qed.
A, B: Type

forall (p q : trace -> Prop) (tr0 tr1 : trace), p tr0 -> q tr1 -> finalTA tr0 (hd tr1) -> (p *+* q) (tr0 +++ tr1)
A, B: Type

forall (p q : trace -> Prop) (tr0 tr1 : trace), p tr0 -> q tr1 -> finalTA tr0 (hd tr1) -> (p *+* q) (tr0 +++ tr1)
A, B: Type
p, q: trace -> Prop
tr0, tr1: trace
hp: p tr0
hq: q tr1
hfin: finalTA tr0 (hd tr1)

(p *+* q) (tr0 +++ tr1)
A, B: Type
p, q: trace -> Prop
tr0, tr1: trace
hp: p tr0
hq: q tr1
hfin: finalTA tr0 (hd tr1)

p tr0 /\ followsT q tr0 (tr0 +++ tr1)
A, B: Type
p, q: trace -> Prop
tr0, tr1: trace
hp: p tr0
hq: q tr1
hfin: finalTA tr0 (hd tr1)

followsT q tr0 (tr0 +++ tr1)
A, B: Type
p, q: trace -> Prop

forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)

forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)

forall (a : A) (tr1 : trace), q tr1 -> finalTA (Tnil a) (hd tr1) -> followsT q (Tnil a) (Tnil a +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
forall (a : A) (b : B) (t tr1 : trace), q tr1 -> finalTA (Tcons a b t) (hd tr1) -> followsT q (Tcons a b t) (Tcons a b t +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)

forall (a : A) (tr1 : trace), q tr1 -> finalTA (Tnil a) (hd tr1) -> followsT q (Tnil a) (Tnil a +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
forall (a : A) (b : B) (t tr1 : trace), q tr1 -> finalTA (Tcons a b t) (hd tr1) -> followsT q (Tcons a b t) (Tcons a b t +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
a: A
tr0: trace
hq: q tr0
h1: finalTA (Tnil a) (hd tr0)

followsT q (Tnil a) (Tnil a +++ tr0)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
forall (a : A) (b : B) (t tr1 : trace), q tr1 -> finalTA (Tcons a b t) (hd tr1) -> followsT q (Tcons a b t) (Tcons a b t +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
a: A
tr0: trace
hq: q tr0
h1: finalTA (Tnil a) (hd tr0)

followsT q (Tnil a) tr0
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
forall (a : A) (b : B) (t tr1 : trace), q tr1 -> finalTA (Tcons a b t) (hd tr1) -> followsT q (Tcons a b t) (Tcons a b t +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
tr0: trace
hq: q tr0

followsT q (Tnil (hd tr0)) tr0
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
forall (a : A) (b : B) (t tr1 : trace), q tr1 -> finalTA (Tcons a b t) (hd tr1) -> followsT q (Tcons a b t) (Tcons a b t +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)

forall (a : A) (b : B) (t tr1 : trace), q tr1 -> finalTA (Tcons a b t) (hd tr1) -> followsT q (Tcons a b t) (Tcons a b t +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)

forall (a : A) (b : B) (t tr1 : trace), q tr1 -> finalTA (Tcons a b t) (hd tr1) -> followsT q (Tcons a b t) (Tcons a b t +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
a: A
b: B
tr0, tr1: trace
h0: q tr1
H3: finalTA tr0 (hd tr1)

followsT q (Tcons a b tr0) (Tcons a b tr0 +++ tr1)
A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 : trace, q tr1 -> finalTA tr0 (hd tr1) -> followsT q tr0 (tr0 +++ tr1)
a: A
b: B
tr0, tr1: trace
h0: q tr1
H3: finalTA tr0 (hd tr1)

followsT q (Tcons a b tr0) (Tcons a b ((cofix trace_append (tr tr' : trace) : trace := match tr with | Tnil _ => tr' | Tcons a b tr0 => Tcons a b (trace_append tr0 tr') end) tr0 tr1))
exact/followsT_delay/CIH. Qed. Definition AppendT (p1 p2 : propT) : propT := let: exist f0 h0 := p1 in let: exist f1 h1 := p2 in exist _ (appendT f0 f1) (appendT_setoidT h1). #[local] Infix "***" := AppendT (at level 60, right associativity).
A, B: Type

forall p1 p2 p3 : propT, ((p1 *** p2) *** p3) =>> p1 *** p2 *** p3
A, B: Type

forall p1 p2 p3 : propT, ((p1 *** p2) *** p3) =>> p1 *** p2 *** p3
A, B: Type
f1: trace -> Prop
hf1: setoidT f1
f2: trace -> Prop
hf2: setoidT f2
f3: trace -> Prop
hf3: setoidT f3
tr0: trace
h1: ((f1 *+* f2) *+* f3) tr0

(f1 *+* f2 *+* f3) tr0
exact: appendT_assoc_L. Qed.
A, B: Type

forall p1 p2 q1 q2 : propT, p1 =>> p2 -> q1 =>> q2 -> (p1 *** q1) =>> p2 *** q2
A, B: Type

forall p1 p2 q1 q2 : propT, p1 =>> p2 -> q1 =>> q2 -> (p1 *** q1) =>> p2 *** q2
A, B: Type
p1: trace -> Prop
hp1: setoidT p1
p2: trace -> Prop
hp2: setoidT p2
q1: trace -> Prop
hq1: setoidT q1
q2: trace -> Prop
hq2: setoidT q2
h0: exist (fun p : trace -> Prop => setoidT p) p1 hp1 =>> exist (fun p : trace -> Prop => setoidT p) p2 hp2
h1: exist (fun p : trace -> Prop => setoidT p) q1 hq1 =>> exist (fun p : trace -> Prop => setoidT p) q2 hq2
tr0: trace
h2: (p1 *+* q1) tr0

(p2 *+* q2) tr0
A, B: Type
p1: trace -> Prop
hp1: setoidT p1
p2: trace -> Prop
hp2: setoidT p2
q1: trace -> Prop
hq1: setoidT q1
q2: trace -> Prop
hq2: setoidT q2
h0: exist (fun p : trace -> Prop => setoidT p) p1 hp1 =>> exist (fun p : trace -> Prop => setoidT p) p2 hp2
h1: exist (fun p : trace -> Prop => setoidT p) q1 hq1 =>> exist (fun p : trace -> Prop => setoidT p) q2 hq2
tr0: trace
h2: (p1 *+* q1) tr0

forall tr : trace, p1 tr -> p2 tr
A, B: Type
p1: trace -> Prop
hp1: setoidT p1
p2: trace -> Prop
hp2: setoidT p2
q1: trace -> Prop
hq1: setoidT q1
q2: trace -> Prop
hq2: setoidT q2
h0: exist (fun p : trace -> Prop => setoidT p) p1 hp1 =>> exist (fun p : trace -> Prop => setoidT p) p2 hp2
h1: exist (fun p : trace -> Prop => setoidT p) q1 hq1 =>> exist (fun p : trace -> Prop => setoidT p) q2 hq2
tr0: trace
h2: (p1 *+* q1) tr0
forall tr : trace, q1 tr -> q2 tr
A, B: Type
p1: trace -> Prop
hp1: setoidT p1
p2: trace -> Prop
hp2: setoidT p2
q1: trace -> Prop
hq1: setoidT q1
q2: trace -> Prop
hq2: setoidT q2
h0: exist (fun p : trace -> Prop => setoidT p) p1 hp1 =>> exist (fun p : trace -> Prop => setoidT p) p2 hp2
h1: exist (fun p : trace -> Prop => setoidT p) q1 hq1 =>> exist (fun p : trace -> Prop => setoidT p) q2 hq2
tr0: trace
h2: (p1 *+* q1) tr0

forall tr : trace, p1 tr -> p2 tr
A, B: Type
p1: trace -> Prop
hp1: setoidT p1
p2: trace -> Prop
hp2: setoidT p2
q1: trace -> Prop
hq1: setoidT q1
q2: trace -> Prop
hq2: setoidT q2
h0: exist (fun p : trace -> Prop => setoidT p) p1 hp1 =>> exist (fun p : trace -> Prop => setoidT p) p2 hp2
h1: exist (fun p : trace -> Prop => setoidT p) q1 hq1 =>> exist (fun p : trace -> Prop => setoidT p) q2 hq2
tr0: trace
h2: (p1 *+* q1) tr0
forall tr : trace, q1 tr -> q2 tr
A, B: Type
p1: trace -> Prop
hp1: setoidT p1
p2: trace -> Prop
hp2: setoidT p2
q1: trace -> Prop
hq1: setoidT q1
q2: trace -> Prop
hq2: setoidT q2
h0: exist (fun p : trace -> Prop => setoidT p) p1 hp1 =>> exist (fun p : trace -> Prop => setoidT p) p2 hp2
h1: exist (fun p : trace -> Prop => setoidT p) q1 hq1 =>> exist (fun p : trace -> Prop => setoidT p) q2 hq2
tr0: trace
h2: (p1 *+* q1) tr0

forall tr : trace, q1 tr -> q2 tr
A, B: Type
p1: trace -> Prop
hp1: setoidT p1
p2: trace -> Prop
hp2: setoidT p2
q1: trace -> Prop
hq1: setoidT q1
q2: trace -> Prop
hq2: setoidT q2
h0: exist (fun p : trace -> Prop => setoidT p) p1 hp1 =>> exist (fun p : trace -> Prop => setoidT p) p2 hp2
h1: exist (fun p : trace -> Prop => setoidT p) q1 hq1 =>> exist (fun p : trace -> Prop => setoidT p) q2 hq2
tr0: trace
h2: (p1 *+* q1) tr0

forall tr : trace, q1 tr -> q2 tr
exact: h1. Qed.
A, B: Type

forall p1 p2 q : propT, p1 =>> p2 -> (p1 *** q) =>> p2 *** q
A, B: Type

forall p1 p2 q : propT, p1 =>> p2 -> (p1 *** q) =>> p2 *** q
A, B: Type
p1: trace -> Prop
hp1: setoidT p1
p2: trace -> Prop
hp2: setoidT p2
q: trace -> Prop
hq: setoidT q
h0: exist (fun p : trace -> Prop => setoidT p) p1 hp1 =>> exist (fun p : trace -> Prop => setoidT p) p2 hp2
tr0: trace

(p1 *+* q) tr0 -> (p2 *+* q) tr0
exact: appendT_cont_L. Qed.
A, B: Type

forall q p1 p2 : propT, p1 =>> p2 -> (q *** p1) =>> q *** p2
A, B: Type

forall q p1 p2 : propT, p1 =>> p2 -> (q *** p1) =>> q *** p2
A, B: Type
q: trace -> Prop
hq: setoidT q
p1: trace -> Prop
hp1: setoidT p1
p2: trace -> Prop
hp2: setoidT p2
h0: exist (fun p : trace -> Prop => setoidT p) p1 hp1 =>> exist (fun p : trace -> Prop => setoidT p) p2 hp2
tr0: trace
h1: (q *+* p1) tr0

(q *+* p2) tr0
exact: (@appendT_cont q q p1 p2). Qed.
A, B: Type

forall p : propT, p =>> p *** ([|ttA|])
A, B: Type

forall p : propT, p =>> p *** ([|ttA|])
A, B: Type
f: trace -> Prop
hp: setoidT f
tr0: trace
h0: f tr0

(f *+* singletonT ttA) tr0
A, B: Type
f: trace -> Prop
hp: setoidT f
tr0: trace
h0: f tr0

followsT (singletonT ttA) tr0 tr0
A, B: Type
f: trace -> Prop

forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
A, B: Type
f: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0

forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
A, B: Type
f: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A

followsT (singletonT ttA) (Tnil a) (Tnil a)
A, B: Type
f: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: trace
followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
f: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A

followsT (singletonT ttA) (Tnil a) (Tnil a)
A, B: Type
f: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: trace
followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
f: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: trace

followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
f: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: trace

followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
exact/followsT_delay/CIH. Qed.
A, B: Type

forall (u v : propA) (b : B), (([|u|]) *** (<< v; b >>)) =>> (<< u andA v; b >>)
A, B: Type

forall (u v : propA) (b : B), (([|u|]) *** (<< v; b >>)) =>> (<< u andA v; b >>)
A, B: Type
u, v: propA
b: B
tr0: trace
h0: u (hd tr0)
H1: dupT v b tr0

dupT (u andA v) b tr0
A, B: Type
u, v: propA
b: B
a: A
h0: u (hd (Tcons a b (Tnil a)))
h1: v a

dupT (u andA v) b (Tcons a b (Tnil a))
exact: dupT_Tcons. Qed.
A, B: Type

forall (u v : propA) (b : B), (<< u andA v; b >>) =>> ([|u|]) *** (<< v; b >>)
A, B: Type

forall (u v : propA) (b : B), (<< u andA v; b >>) =>> ([|u|]) *** (<< v; b >>)
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a

satisfyT (([|u|]) *** (<< v; b >>)) (Tcons a b (Tnil a))
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a

followsT (dupT v b) (Tnil a) (Tcons a b (Tnil a))
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a

dupT v b (Tcons a b (Tnil a))
exact: dupT_Tcons. Qed.
A, B: Type

forall (u v : propA) (b : B), (<< u andA v; b >>) =>> (<< u; b >>) *** ([|v|])
A, B: Type

forall (u v : propA) (b : B), (<< u andA v; b >>) =>> (<< u; b >>) *** ([|v|])
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a

satisfyT ((<< u; b >>) *** ([|v|])) (Tcons a b (Tnil a))
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a

dupT u b (Tcons a b (Tnil a))
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a
followsT (singletonT v) (Tcons a b (Tnil a)) (Tcons a b (Tnil a))
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a

dupT u b (Tcons a b (Tnil a))
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a
followsT (singletonT v) (Tcons a b (Tnil a)) (Tcons a b (Tnil a))
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a

followsT (singletonT v) (Tcons a b (Tnil a)) (Tcons a b (Tnil a))
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a

followsT (singletonT v) (Tcons a b (Tnil a)) (Tcons a b (Tnil a))
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a

followsT (singletonT v) (Tnil a) (Tnil a)
A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v a

singletonT v (Tnil a)
exact: nil_singletonT. Qed.
A, B: Type

forall (u v : propA) (b : B), ((<< u; b >>) *** ([|v|])) =>> (<< u andA v; b >>)
A, B: Type

forall (u v : propA) (b : B), ((<< u; b >>) *** ([|v|])) =>> (<< u andA v; b >>)
A, B: Type
u, v: propA
b: B
tr0, tr1: trace
a: A
hu: u a
h0: bisim tr1 (Tcons a b (Tnil a))
h1: followsT (singletonT v) tr1 tr0

satisfyT (<< u andA v; b >>) tr0
A, B: Type
u, v: propA
b: B
a: A
hu: u (hd (Tnil a))
hv: v a

dupT (u andA v) b (Tcons a b (Tnil a))
exact: dupT_Tcons. Qed.
A, B: Type

forall u v : propA, (([|u|]) *** ([|v|])) =>> ([|u andA v|])
A, B: Type

forall u v : propA, (([|u|]) *** ([|v|])) =>> ([|u andA v|])
A, B: Type
u, v: propA
tr0, tr1: trace
a: A
hu: u a
h0: bisim tr1 (Tnil a)
h1: followsT (singletonT v) tr1 tr0

satisfyT ([|u andA v|]) tr0
A, B: Type
u, v: propA
a: A
hu: u (hd (Tnil a))
hv: v a

singletonT (u andA v) (Tnil a)
exact: nil_singletonT. Qed.
A, B: Type

forall u v : propA, ([|u andA v|]) =>> ([|u|]) *** ([|v|])
A, B: Type

forall u v : propA, ([|u andA v|]) =>> ([|u|]) *** ([|v|])
A, B: Type
u, v: propA
a: A
hu: u a
hv: v a

satisfyT (([|u|]) *** ([|v|])) (Tnil a)
A, B: Type
u, v: propA
a: A
hu: u a
hv: v a

followsT (singletonT v) (Tnil a) (Tnil a)
A, B: Type
u, v: propA
a: A
hu: u a
hv: v a

singletonT v (Tnil a)
exact: nil_singletonT. Qed.
A, B: Type

forall (v : propA) (p : propT), (([|v|]) *** p) =>> p
A, B: Type

forall (v : propA) (p : propT), (([|v|]) *** p) =>> p
by move => v [p hp] tr0 /= [tr1 [[a [h0 h2]] h1]]; invs h1; invs h2. Qed.
A, B: Type

forall p : propT, (([|ttA|]) *** p) =>> p
A, B: Type

forall p : propT, (([|ttA|]) *** p) =>> p
A, B: Type
p: propT

(([|ttA|]) *** p) =>> p
exact: SingletonT_AppendT. Qed.
A, B: Type

forall p : propT, p =>> ([|ttA|]) *** p
A, B: Type

forall p : propT, p =>> ([|ttA|]) *** p
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0

(singletonT ttA *+* p) tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0

singletonT ttA (Tnil (hd tr0))
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0
followsT p (Tnil (hd tr0)) tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0

singletonT ttA (Tnil (hd tr0))
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0
followsT p (Tnil (hd tr0)) tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0

followsT p (Tnil (hd tr0)) tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0

followsT p (Tnil (hd tr0)) tr0
exact: followsT_nil. Qed.
A, B: Type

forall p : trace -> Prop, setoidT p -> forall (u : propA) (tr : trace), (p *+* singletonT u) tr -> p tr
A, B: Type

forall p : trace -> Prop, setoidT p -> forall (u : propA) (tr : trace), (p *+* singletonT u) tr -> p tr
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
tr0, tr1: trace
h1: p tr1
h2: followsT (singletonT u) tr1 tr0

p tr0
exact: (hp _ h1 _ (followsT_singletonT h2)). Qed.
A, B: Type

forall (p : propT) (v : propA), (p *** ([|v|])) =>> p
A, B: Type

forall (p : propT) (v : propA), (p *** ([|v|])) =>> p
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
tr0: trace

(p *+* singletonT v) tr0 -> p tr0
exact: appendT_singletonT. Qed.
A, B: Type

forall p : propT, (p *** ([|ttA|])) =>> p
A, B: Type

forall p : propT, (p *** ([|ttA|])) =>> p
A, B: Type
p: propT

(p *** ([|ttA|])) =>> p
exact: AppendT_Singleton. Qed.
A, B: Type

forall p : propT, p =>> p *** ([|ttA|])
A, B: Type

forall p : propT, p =>> p *** ([|ttA|])
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0

(p *+* singletonT ttA) tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0

followsT (singletonT ttA) tr0 tr0
A, B: Type
p: trace -> Prop

forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0

forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A

followsT (singletonT ttA) (Tnil a) (Tnil a)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: trace
followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A

followsT (singletonT ttA) (Tnil a) (Tnil a)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: trace
followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A

singletonT ttA (Tnil a)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: trace
followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: trace

followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: trace

followsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
exact/followsT_delay/CIH. Qed.
A, B: Type

(TtT *** TtT) =>> TtT
A, B: Type

(TtT *** TtT) =>> TtT
by []. Qed.
A, B: Type

(FiniteT *** FiniteT) =>> FiniteT
A, B: Type

(FiniteT *** FiniteT) =>> FiniteT
A, B: Type
tr0, tr1: trace
Hfin: finiteT tr1
Hfol: followsT (fun tr : trace => finiteT tr) tr1 tr0

satisfyT FiniteT tr0
A, B: Type
tr1: trace
a: A
b: B
tr1': trace
h0: finiteT tr1'
IH: forall tr0 : trace, followsT (fun tr : trace => finiteT tr) tr1' tr0 -> satisfyT FiniteT tr0
tr': trace
H3: followsT (fun tr : trace => finiteT tr) tr1' tr'

satisfyT FiniteT (Tcons a b tr')
exact/finiteT_delay/IH. Qed.
A, B: Type

FiniteT =>> FiniteT *** FiniteT
A, B: Type

FiniteT =>> FiniteT *** FiniteT
A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0

satisfyT (FiniteT *** FiniteT) tr0
A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0

finiteT (Tnil (hd tr0))
A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0
followsT (fun tr : trace => finiteT tr) (Tnil (hd tr0)) tr0
A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0

finiteT (Tnil (hd tr0))
A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0
followsT (fun tr : trace => finiteT tr) (Tnil (hd tr0)) tr0
A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0

followsT (fun tr : trace => finiteT tr) (Tnil (hd tr0)) tr0
A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0

followsT (fun tr : trace => finiteT tr) (Tnil (hd tr0)) tr0
exact: followsT_nil. Qed.
A, B: Type

forall u : propA, (FiniteT *** ([|u|])) =>> FiniteT
A, B: Type

forall u : propA, (FiniteT *** ([|u|])) =>> FiniteT
A, B: Type
u: propA
tr, tr1: trace
h0: finiteT tr1
h1: followsT (singletonT u) tr1 tr

finiteT tr
exact: (finiteT_setoidT h0 (followsT_singletonT h1)). Qed.
A, B: Type

InfiniteT =>> TtT *** ([|ffA|])
A, B: Type

InfiniteT =>> TtT *** ([|ffA|])
A, B: Type
tr0: trace
a: A
b: B
tr1: trace
HinfT: infiniteT tr1

(ttT *+* singletonT ffA) (Tcons a b tr1)
A, B: Type
a: A
b: B
tr1: trace
HinfT: infiniteT tr1

followsT (singletonT ffA) (Tcons a b tr1) (Tcons a b tr1)
A, B: Type

forall (a : A) (b : B) (tr1 : trace), infiniteT tr1 -> followsT (singletonT ffA) (Tcons a b tr1) (Tcons a b tr1)
A, B: Type
CIH: forall (a : A) (b : B) (tr1 : trace), infiniteT tr1 -> followsT (singletonT ffA) (Tcons a b tr1) (Tcons a b tr1)

forall (a : A) (b : B) (tr1 : trace), infiniteT tr1 -> followsT (singletonT ffA) (Tcons a b tr1) (Tcons a b tr1)
A, B: Type
CIH: forall (a : A) (b : B) (tr1 : trace), infiniteT tr1 -> followsT (singletonT ffA) (Tcons a b tr1) (Tcons a b tr1)
a: A
b: B
a0: A
b0: B
tr: trace
H: infiniteT tr

followsT (singletonT ffA) (Tcons a b (Tcons a0 b0 tr)) (Tcons a b (Tcons a0 b0 tr))
exact/followsT_delay/CIH. Qed.
A, B: Type

(TtT *** ([|ffA|])) =>> InfiniteT
A, B: Type

(TtT *** ([|ffA|])) =>> InfiniteT
A, B: Type
tr0, tr1: trace
h1: followsT (singletonT ffA) tr1 tr0

infiniteT tr0
A, B: Type
CIH: forall tr0 tr1 : trace, followsT (singletonT ffA) tr1 tr0 -> infiniteT tr0
tr0: trace
H0: singletonT ffA tr0

infiniteT tr0
A, B: Type
CIH: forall tr0 tr1 : trace, followsT (singletonT ffA) tr1 tr0 -> infiniteT tr0
a: A
b: B
tr, tr': trace
H: followsT (singletonT ffA) tr tr'
infiniteT (Tcons a b tr')
A, B: Type
CIH: forall tr0 tr1 : trace, followsT (singletonT ffA) tr1 tr0 -> infiniteT tr0
tr0: trace
H0: singletonT ffA tr0

infiniteT tr0
A, B: Type
CIH: forall tr0 tr1 : trace, followsT (singletonT ffA) tr1 tr0 -> infiniteT tr0
a: A
b: B
tr, tr': trace
H: followsT (singletonT ffA) tr tr'
infiniteT (Tcons a b tr')
A, B: Type
CIH: forall tr0 tr1 : trace, followsT (singletonT ffA) tr1 tr0 -> infiniteT tr0
a: A
b: B
tr, tr': trace
H: followsT (singletonT ffA) tr tr'

infiniteT (Tcons a b tr')
A, B: Type
CIH: forall tr0 tr1 : trace, followsT (singletonT ffA) tr1 tr0 -> infiniteT tr0
a: A
b: B
tr, tr': trace
H: followsT (singletonT ffA) tr tr'

infiniteT (Tcons a b tr')
exact: infiniteT_delay _ _ (CIH _ _ H). Qed.

Iteration property

CoInductive iterT (p : trace -> Prop) : trace -> Prop :=
| iterT_stop : forall a,
   iterT p (Tnil a)
| iterT_loop : forall tr tr0,
   p tr ->
   followsT (iterT p) tr tr0 ->
   iterT p tr0.

A, B: Type

forall p : trace -> Prop, setoidT p -> setoidT (iterT p)
A, B: Type

forall p : trace -> Prop, setoidT p -> setoidT (iterT p)
A, B: Type
p: trace -> Prop
hp: setoidT p

setoidT (iterT p)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)

setoidT (iterT p)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)

forall tr : trace, setoidT (followsT (iterT p) tr)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
setoidT (iterT p)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
CIH1: forall tr : trace, setoidT (followsT (iterT p) tr)

forall tr : trace, setoidT (followsT (iterT p) tr)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
setoidT (iterT p)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
CIH1: forall tr : trace, setoidT (followsT (iterT p) tr)
tr, tr0: trace
h0: followsT (iterT p) tr tr0
tr1: trace
h1: bisim tr0 tr1

followsT (iterT p) tr tr1
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
setoidT (iterT p)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
CIH1: forall tr : trace, setoidT (followsT (iterT p) tr)
tr0, tr1: trace
h1: bisim tr0 tr1
H0: iterT p tr0

followsT (iterT p) (Tnil (hd tr0)) tr1
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
setoidT (iterT p)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
CIH1: forall tr : trace, setoidT (followsT (iterT p) tr)
tr0, tr1: trace
h1: bisim tr0 tr1
H0: iterT p tr0

iterT p tr1
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
setoidT (iterT p)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)

setoidT (iterT p)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
a: A
tr1: trace
h2: bisim (Tnil a) tr1

iterT p tr1
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
tr0, tr1: trace
h2: bisim tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
iterT p tr1
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
a: A
tr1: trace
h2: bisim (Tnil a) tr1

iterT p tr1
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
tr0, tr1: trace
h2: bisim tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
iterT p tr1
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
a: A

iterT p (Tnil a)
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
tr0, tr1: trace
h2: bisim tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
iterT p tr1
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
tr0, tr1: trace
h2: bisim tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0

iterT p tr1
A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
tr0, tr1: trace
h2: bisim tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0

iterT p tr1
exact: iterT_loop H (h0 _ _ H0 _ h2). Qed.
A, B: Type

forall p0 p1 : trace -> Prop, (forall tr : trace, p0 tr -> p1 tr) -> forall tr : trace, iterT p0 tr -> iterT p1 tr
A, B: Type

forall p0 p1 : trace -> Prop, (forall tr : trace, p0 tr -> p1 tr) -> forall tr : trace, iterT p0 tr -> iterT p1 tr
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr

forall tr : trace, iterT p0 tr -> iterT p1 tr
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr

forall tr : trace, iterT p0 tr -> iterT p1 tr
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr

forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr
h: forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1
forall tr : trace, iterT p0 tr -> iterT p1 tr
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr
CIH0: forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1

forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr
h: forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1
forall tr : trace, iterT p0 tr -> iterT p1 tr
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr
CIH0: forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1
tr0, tr1: trace
h0: followsT (iterT p0) tr0 tr1

followsT (iterT p1) tr0 tr1
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr
h: forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1
forall tr : trace, iterT p0 tr -> iterT p1 tr
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr
CIH0: forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1
tr1: trace
H0: iterT p0 tr1

followsT (iterT p1) (Tnil (hd tr1)) tr1
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr
h: forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1
forall tr : trace, iterT p0 tr -> iterT p1 tr
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr
h: forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1

forall tr : trace, iterT p0 tr -> iterT p1 tr
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 tr
h: forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1
tr0, tr: trace
H: p0 tr
H0: followsT (iterT p0) tr tr0

iterT p1 tr0
exact: iterT_loop (hp _ H) (h _ _ H0). Qed.
A, B: Type

forall (u : propA) (p : trace -> Prop) (b : B) (tr : trace), u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
A, B: Type

forall (u : propA) (p : trace -> Prop) (b : B) (tr : trace), u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B

forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr

forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
a: A
h0: u (hd (Tnil a))

followsT (singletonT u) (Tnil a) (Tnil a)
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
tr: trace
h0: u (hd tr)
tr0: trace
H: (p *+* dupT u b) tr0
H0: followsT (iterT (p *+* dupT u b)) tr0 tr
followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
a: A
h0: u (hd (Tnil a))

followsT (singletonT u) (Tnil a) (Tnil a)
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
tr: trace
h0: u (hd tr)
tr0: trace
H: (p *+* dupT u b) tr0
H0: followsT (iterT (p *+* dupT u b)) tr0 tr
followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
a: A
h0: u (hd (Tnil a))

singletonT u (Tnil a)
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
tr: trace
h0: u (hd tr)
tr0: trace
H: (p *+* dupT u b) tr0
H0: followsT (iterT (p *+* dupT u b)) tr0 tr
followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
tr: trace
h0: u (hd tr)
tr0: trace
H: (p *+* dupT u b) tr0
H0: followsT (iterT (p *+* dupT u b)) tr0 tr

followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
tr: trace
h0: u (hd tr)
tr0: trace
H: (p *+* dupT u b) tr0
H0: followsT (iterT (p *+* dupT u b)) tr0 tr

followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
tr, tr0: trace
H0: followsT (iterT (p *+* dupT u b)) tr0 tr
tr1: trace
h1: followsT (dupT u b) tr1 tr0

followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr

forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr

forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
tr0, tr2: trace
h1: followsT (iterT (p *+* dupT u b)) tr2 tr0
H0: dupT u b tr2

followsT (singletonT u) tr0 tr0
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
tr0: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (p *+* dupT u b)) (Tcons a b0 tr') tr0
H: followsT (dupT u b) tr tr'
followsT (singletonT u) tr0 tr0
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
tr0, tr2: trace
h1: followsT (iterT (p *+* dupT u b)) tr2 tr0
H0: dupT u b tr2

followsT (singletonT u) tr0 tr0
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
tr0: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (p *+* dupT u b)) (Tcons a b0 tr') tr0
H: followsT (dupT u b) tr tr'
followsT (singletonT u) tr0 tr0
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
tr0, tr2: trace
h1: followsT (iterT (p *+* dupT u b)) tr2 tr0
a: A
h0: u a
h3: bisim tr2 (Tcons a b (Tnil a))

followsT (singletonT u) tr0 tr0
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
tr0: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (p *+* dupT u b)) (Tcons a b0 tr') tr0
H: followsT (dupT u b) tr tr'
followsT (singletonT u) tr0 tr0
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
tr': trace
h0: u (hd tr')
H1: iterT (p *+* dupT u b) tr'

followsT (singletonT u) (Tcons (hd tr') b tr') (Tcons (hd tr') b tr')
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
tr0: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (p *+* dupT u b)) (Tcons a b0 tr') tr0
H: followsT (dupT u b) tr tr'
followsT (singletonT u) tr0 tr0
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
tr0: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (p *+* dupT u b)) (Tcons a b0 tr') tr0
H: followsT (dupT u b) tr tr'

followsT (singletonT u) tr0 tr0
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
tr0: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (p *+* dupT u b)) (Tcons a b0 tr') tr0
H: followsT (dupT u b) tr tr'

followsT (singletonT u) tr0 tr0
A, B: Type
u: propA
p: trace -> Prop
b: B
CIH: forall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr tr
CIH1: forall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr tr
a: A
b0: B
tr, tr', tr'0: trace
H: followsT (dupT u b) tr tr'
H4: followsT (iterT (p *+* dupT u b)) tr' tr'0

followsT (singletonT u) (Tcons a b0 tr'0) (Tcons a b0 tr'0)
exact: followsT_delay _ _ (CIH1 _ _ _ H H4). Qed. Definition IterT (p : propT) : propT := let: exist f0 h0 := p in exist _ (iterT f0) (iterT_setoidT h0).
A, B: Type

forall p q : propT, p =>> q -> IterT p =>> IterT q
A, B: Type

forall p q : propT, p =>> q -> IterT p =>> IterT q
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
h0: exist (fun p : trace -> Prop => setoidT p) p hp =>> exist (fun p : trace -> Prop => setoidT p) q hq
tr0: trace

iterT p tr0 -> iterT q tr0
exact: (iterT_cont (fun tr => h0 tr)). Qed.
A, B: Type

forall (p : trace -> Prop) (tr : trace), iterT p tr -> singletonT ttA tr \/ (p *+* iterT p) tr
A, B: Type

forall (p : trace -> Prop) (tr : trace), iterT p tr -> singletonT ttA tr \/ (p *+* iterT p) tr
A, B: Type
p: trace -> Prop
a: A

singletonT ttA (Tnil a) \/ (p *+* iterT p) (Tnil a)
A, B: Type
p: trace -> Prop
tr, tr0: trace
H: p tr0
H0: followsT (iterT p) tr0 tr
singletonT ttA tr \/ (p *+* iterT p) tr
A, B: Type
p: trace -> Prop
a: A

singletonT ttA (Tnil a) \/ (p *+* iterT p) (Tnil a)
A, B: Type
p: trace -> Prop
tr, tr0: trace
H: p tr0
H0: followsT (iterT p) tr0 tr
singletonT ttA tr \/ (p *+* iterT p) tr
A, B: Type
p: trace -> Prop
tr, tr0: trace
H: p tr0
H0: followsT (iterT p) tr0 tr

singletonT ttA tr \/ (p *+* iterT p) tr
A, B: Type
p: trace -> Prop
tr, tr0: trace
H: p tr0
H0: followsT (iterT p) tr0 tr

singletonT ttA tr \/ (p *+* iterT p) tr
by right; exists tr0. Qed.
A, B: Type

forall p : propT, IterT p =>> ([|ttA|]) orT p *** IterT p
A, B: Type

forall p : propT, IterT p =>> ([|ttA|]) orT p *** IterT p
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
h0: iterT p tr0

singletonT ttA tr0 \/ (p *+* iterT p) tr0
exact: iterT_split_1 h0. Qed.
A, B: Type

forall (tr : trace) (p : trace -> Prop), singletonT ttA tr \/ (p *+* iterT p) tr -> iterT p tr
A, B: Type

forall (tr : trace) (p : trace -> Prop), singletonT ttA tr \/ (p *+* iterT p) tr -> iterT p tr
A, B: Type
tr: trace
p: trace -> Prop
a: A
h0: ttA a
h1: bisim tr (Tnil a)

iterT p tr
A, B: Type
tr: trace
p: trace -> Prop
tr0: trace
h0: p tr0
h1: followsT (iterT p) tr0 tr
iterT p tr
A, B: Type
tr: trace
p: trace -> Prop
a: A
h0: ttA a
h1: bisim tr (Tnil a)

iterT p tr
A, B: Type
tr: trace
p: trace -> Prop
tr0: trace
h0: p tr0
h1: followsT (iterT p) tr0 tr
iterT p tr
A, B: Type
p: trace -> Prop
a: A
h0: ttA a

iterT p (Tnil a)
A, B: Type
tr: trace
p: trace -> Prop
tr0: trace
h0: p tr0
h1: followsT (iterT p) tr0 tr
iterT p tr
A, B: Type
tr: trace
p: trace -> Prop
tr0: trace
h0: p tr0
h1: followsT (iterT p) tr0 tr

iterT p tr
A, B: Type
tr: trace
p: trace -> Prop
tr0: trace
h0: p tr0
h1: followsT (iterT p) tr0 tr

iterT p tr
exact: iterT_loop h0 h1. Qed.
A, B: Type

forall p : propT, (([|ttA|]) orT p *** IterT p) =>> IterT p
A, B: Type

forall p : propT, (([|ttA|]) orT p *** IterT p) =>> IterT p
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace

singletonT ttA tr0 \/ (p *+* iterT p) tr0 -> iterT p tr0
exact: iterT_split_2. Qed.
A, B: Type

forall (p : trace -> Prop) (tr : trace), (iterT p *+* p) tr -> iterT p tr
A, B: Type

forall (p : trace -> Prop) (tr : trace), (iterT p *+* p) tr -> iterT p tr
A, B: Type
p: trace -> Prop
tr, tr0: trace
h0: iterT p tr0
h1: followsT p tr0 tr

iterT p tr
A, B: Type
p: trace -> Prop

forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr

forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr1: trace
a: A
h1: followsT p (Tnil a) tr1

iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr0, tr1: trace
h1: followsT p tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr1: trace
a: A
h1: followsT p (Tnil a) tr1

iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr0, tr1: trace
h1: followsT p tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr1: trace
H1: p tr1

iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr0, tr1: trace
h1: followsT p tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr1: trace
H1: p tr1

followsT (iterT p) tr1 tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr0, tr1: trace
h1: followsT p tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr

forall tr1 : trace, followsT (iterT p) tr1 tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr0, tr1: trace
h1: followsT p tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr1 : trace, followsT (iterT p) tr1 tr1

forall tr1 : trace, followsT (iterT p) tr1 tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr0, tr1: trace
h1: followsT p tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr1 : trace, followsT (iterT p) tr1 tr1
a: A
b: B
tr0: trace

followsT (iterT p) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr0, tr1: trace
h1: followsT p tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr0, tr1: trace
h1: followsT p tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0

iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr0, tr1: trace
h1: followsT p tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0

iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr0, tr1: trace
h1: followsT p tr0 tr1
tr: trace
H: p tr
H0: followsT (iterT p) tr tr0

followsT (iterT p) tr tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr

forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1

forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
tr1, tr2: trace
h1: followsT p tr1 tr2
H0: iterT p tr1

followsT (iterT p) (Tnil (hd tr1)) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
tr2: trace
a: A
b: B
tr, tr': trace
h1: followsT p (Tcons a b tr') tr2
H: followsT (iterT p) tr tr'
followsT (iterT p) (Tcons a b tr) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
tr1, tr2: trace
h1: followsT p tr1 tr2
H0: iterT p tr1

followsT (iterT p) (Tnil (hd tr1)) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
tr2: trace
a: A
b: B
tr, tr': trace
h1: followsT p (Tcons a b tr') tr2
H: followsT (iterT p) tr tr'
followsT (iterT p) (Tcons a b tr) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
tr1, tr2: trace
h1: followsT p tr1 tr2
H0: iterT p tr1

followsT (iterT p) (Tnil (hd tr2)) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
tr2: trace
a: A
b: B
tr, tr': trace
h1: followsT p (Tcons a b tr') tr2
H: followsT (iterT p) tr tr'
followsT (iterT p) (Tcons a b tr) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
tr2: trace
a: A
b: B
tr, tr': trace
h1: followsT p (Tcons a b tr') tr2
H: followsT (iterT p) tr tr'

followsT (iterT p) (Tcons a b tr) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
tr2: trace
a: A
b: B
tr, tr': trace
h1: followsT p (Tcons a b tr') tr2
H: followsT (iterT p) tr tr'

followsT (iterT p) (Tcons a b tr) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
CIH0: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1
a: A
b: B
tr, tr', tr'0: trace
H: followsT (iterT p) tr tr'
H4: followsT p tr' tr'0

followsT (iterT p) (Tcons a b tr) (Tcons a b tr'0)
exact: followsT_delay _ _ (CIH0 _ _ _ H H4). Qed.
A, B: Type

forall p : propT, (IterT p *** p) =>> IterT p
A, B: Type

forall p : propT, (IterT p *** p) =>> IterT p
A, B: Type
p: trace -> Prop
hp: setoidT p
tr: trace
h0: (iterT p *+* p) tr

iterT p tr
exact: iterT_unfold_1 h0. Qed.
A, B: Type

forall p : propT, (([|ttA|]) orT IterT p *** p) =>> IterT p
A, B: Type

forall p : propT, (([|ttA|]) orT IterT p *** p) =>> IterT p
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
a: A
h0: bisim tr0 (Tnil a)

iterT p tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
H: (iterT p *+* p) tr0
iterT p tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
a: A
h0: bisim tr0 (Tnil a)

iterT p tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
H: (iterT p *+* p) tr0
iterT p tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
a: A

iterT p (Tnil a)
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
H: (iterT p *+* p) tr0
iterT p tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
H: (iterT p *+* p) tr0

iterT p tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
H: (iterT p *+* p) tr0

iterT p tr0
exact: iterT_unfold_1 H. Qed.
A, B: Type

forall p : propT, ([|ttA|]) =>> IterT p
A, B: Type

forall p : propT, ([|ttA|]) =>> IterT p
A, B: Type
p: trace -> Prop
hp: setoidT p
x: A

iterT p (Tnil x)
exact: iterT_stop. Qed.
A, B: Type

forall p : propT, (p *** IterT p) =>> IterT p
A, B: Type

forall p : propT, (p *** IterT p) =>> IterT p
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0, tr1: trace
h0: p tr1
h1: followsT (iterT p) tr1 tr0

iterT p tr0
exact: (iterT_loop h0). Qed.
A, B: Type

forall (p : trace -> Prop) (tr : trace), iterT p tr -> (iterT p *+* iterT p) tr
A, B: Type

forall (p : trace -> Prop) (tr : trace), iterT p tr -> (iterT p *+* iterT p) tr
A, B: Type
p: trace -> Prop
tr0: trace
h0: iterT p tr0

(iterT p *+* iterT p) tr0
A, B: Type
p: trace -> Prop
tr0: trace
h0: iterT p tr0

followsT (iterT p) tr0 tr0
A, B: Type
p: trace -> Prop

forall tr0 : trace, followsT (iterT p) tr0 tr0
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0

forall tr0 : trace, followsT (iterT p) tr0 tr0
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: A

followsT (iterT p) (Tnil a) (Tnil a)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: A
b: B
tr0: trace
followsT (iterT p) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: A

followsT (iterT p) (Tnil a) (Tnil a)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: A
b: B
tr0: trace
followsT (iterT p) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: A

iterT p (Tnil a)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: A
b: B
tr0: trace
followsT (iterT p) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: A
b: B
tr0: trace

followsT (iterT p) (Tcons a b tr0) (Tcons a b tr0)
A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: A
b: B
tr0: trace

followsT (iterT p) (Tcons a b tr0) (Tcons a b tr0)
exact/followsT_delay/CIH. Qed.
A, B: Type

forall p : propT, IterT p =>> IterT p *** IterT p
A, B: Type

forall p : propT, IterT p =>> IterT p *** IterT p
A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace

iterT p tr0 -> (iterT p *+* iterT p) tr0
exact: iterT_iterT_2. Qed.
A, B: Type

forall (p : trace -> Prop) (tr : trace), (iterT p *+* iterT p) tr -> iterT p tr
A, B: Type

forall (p : trace -> Prop) (tr : trace), (iterT p *+* iterT p) tr -> iterT p tr
A, B: Type
p: trace -> Prop
tr0, tr1: trace
h0: iterT p tr1
h1: followsT (iterT p) tr1 tr0

iterT p tr0
A, B: Type
p: trace -> Prop

forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0

forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
tr1: trace
a: A
h0: followsT (iterT p) (Tnil a) tr1

iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
tr0, tr1, tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
h0: followsT (iterT p) tr0 tr1
iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
tr1: trace
a: A
h0: followsT (iterT p) (Tnil a) tr1

iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
tr0, tr1, tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
h0: followsT (iterT p) tr0 tr1
iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
tr0, tr1, tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
h0: followsT (iterT p) tr0 tr1

iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
tr0, tr1, tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
h0: followsT (iterT p) tr0 tr1

iterT p tr1
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
tr0, tr1, tr: trace
H: p tr
H0: followsT (iterT p) tr tr0
h0: followsT (iterT p) tr0 tr1

followsT (iterT p) tr tr1
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0

forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
CIH2: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1

forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
CIH2: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
tr1, tr2: trace
H0: iterT p tr1
h0: followsT (iterT p) tr1 tr2

followsT (iterT p) (Tnil (hd tr1)) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
CIH2: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
tr2: trace
a: A
b: B
tr, tr': trace
H: followsT (iterT p) tr tr'
h0: followsT (iterT p) (Tcons a b tr') tr2
followsT (iterT p) (Tcons a b tr) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
CIH2: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
tr1, tr2: trace
H0: iterT p tr1
h0: followsT (iterT p) tr1 tr2

followsT (iterT p) (Tnil (hd tr1)) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
CIH2: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
tr2: trace
a: A
b: B
tr, tr': trace
H: followsT (iterT p) tr tr'
h0: followsT (iterT p) (Tcons a b tr') tr2
followsT (iterT p) (Tcons a b tr) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
CIH2: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
tr1, tr2: trace
H0: iterT p tr1
h0: followsT (iterT p) tr1 tr2

followsT (iterT p) (Tnil (hd tr2)) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
CIH2: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
tr2: trace
a: A
b: B
tr, tr': trace
H: followsT (iterT p) tr tr'
h0: followsT (iterT p) (Tcons a b tr') tr2
followsT (iterT p) (Tcons a b tr) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
CIH2: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
tr2: trace
a: A
b: B
tr, tr': trace
H: followsT (iterT p) tr tr'
h0: followsT (iterT p) (Tcons a b tr') tr2

followsT (iterT p) (Tcons a b tr) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
CIH2: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
tr2: trace
a: A
b: B
tr, tr': trace
H: followsT (iterT p) tr tr'
h0: followsT (iterT p) (Tcons a b tr') tr2

followsT (iterT p) (Tcons a b tr) tr2
A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0
CIH2: forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1
a: A
b: B
tr, tr': trace
H: followsT (iterT p) tr tr'
tr'0: trace
H4: followsT (iterT p) tr' tr'0

followsT (iterT p) (Tcons a b tr) (Tcons a b tr'0)
exact: followsT_delay _ _ (CIH2 _ _ _ H H4). Qed.
A, B: Type

forall p : propT, (IterT p *** IterT p) =>> IterT p
A, B: Type

forall p : propT, (IterT p *** IterT p) =>> IterT p
A, B: Type
p: trace -> Prop
hp: setoidT p
tr: trace

(iterT p *+* iterT p) tr -> iterT p tr
exact: iterT_iterT. Qed.
A, B: Type

forall (v : propA) (b : B), (([|v|]) *** IterT (TtT *** (<< v; b >>))) =>> TtT *** ([|v|])
A, B: Type

forall (v : propA) (b : B), (([|v|]) *** IterT (TtT *** (<< v; b >>))) =>> TtT *** ([|v|])
A, B: Type
v: propA
b: B
tr0: trace
h0: v (hd tr0)
H1: iterT (ttT *+* dupT v b) tr0

(ttT *+* singletonT v) tr0
A, B: Type
v: propA
b: B
tr0: trace
h0: v (hd tr0)
H1: iterT (ttT *+* dupT v b) tr0

ttT tr0 /\ followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
tr0: trace
h0: v (hd tr0)
H1: iterT (ttT *+* dupT v b) tr0

followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B

forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0

forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
a: A
h0: v (hd (Tnil a))

followsT (singletonT v) (Tnil a) (Tnil a)
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
tr0: trace
h0: v (hd tr0)
tr: trace
H: (ttT *+* dupT v b) tr
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0
followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
a: A
h0: v (hd (Tnil a))

followsT (singletonT v) (Tnil a) (Tnil a)
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
tr0: trace
h0: v (hd tr0)
tr: trace
H: (ttT *+* dupT v b) tr
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0
followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
a: A
h0: v (hd (Tnil a))

singletonT v (Tnil a)
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
tr0: trace
h0: v (hd tr0)
tr: trace
H: (ttT *+* dupT v b) tr
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0
followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
tr0: trace
h0: v (hd tr0)
tr: trace
H: (ttT *+* dupT v b) tr
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0

followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
tr0: trace
h0: v (hd tr0)
tr: trace
H: (ttT *+* dupT v b) tr
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0

followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
tr0, tr: trace
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0
tr1: trace
h1: followsT (dupT v b) tr1 tr

followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0

forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0

forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr1, tr2: trace
h1: followsT (iterT (ttT *+* dupT v b)) tr1 tr2
H0: dupT v b tr1

followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'
followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr1, tr2: trace
h1: followsT (iterT (ttT *+* dupT v b)) tr1 tr2
H0: dupT v b tr1

followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'
followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr1, tr2: trace
h1: followsT (iterT (ttT *+* dupT v b)) tr1 tr2
a: A
h0: v a
h2: bisim tr1 (Tcons a b (Tnil a))

followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'
followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr': trace
h0: v (hd tr')
H1: iterT (ttT *+* dupT v b) tr'

followsT (singletonT v) (Tcons (hd tr') b tr') (Tcons (hd tr') b tr')
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'
followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'

followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'

followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
a: A
b0: B
tr, tr', tr'0: trace
H: followsT (dupT v b) tr tr'
H4: followsT (iterT (ttT *+* dupT v b)) tr' tr'0

followsT (singletonT v) (Tcons a b0 tr'0) (Tcons a b0 tr'0)
exact: followsT_delay _ _ (CIH0 _ _ _ H H4). Qed.

Last property

Definition lastA (p : trace -> Prop) : propA :=
fun a => exists tr, p tr /\ finalTA tr a.

A, B: Type

forall p q : trace -> Prop, (forall tr : trace, p tr -> q tr) -> lastA p ->> lastA q
A, B: Type

forall p q : trace -> Prop, (forall tr : trace, p tr -> q tr) -> lastA p ->> lastA q
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
a: A
tr: trace
h0: p0 tr
h1: finalTA tr a

lastA p1 a
A, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
a: A
tr: trace
h0: p0 tr
h1: finalTA tr a

finalTA tr a
exact: h1. Qed. Definition LastA (p : propT) : propA := let: exist f0 h0 := p in lastA f0.
A, B: Type

forall p q : propT, p =>> q -> LastA p ->> LastA q
A, B: Type

forall p q : propT, p =>> q -> LastA p ->> LastA q
A, B: Type
f: trace -> Prop
hf: setoidT f
g: trace -> Prop
hg: setoidT g
h0: exist (fun p : trace -> Prop => setoidT p) f hf =>> exist (fun p : trace -> Prop => setoidT p) g hg

lastA f ->> lastA g
exact/lastA_cont/h0. Qed.
A, B: Type

forall u : propA, LastA ([|u|]) ->> u
A, B: Type

forall u : propA, LastA ([|u|]) ->> u
by move => u a [tr0 [[st1 [h1 h3]] h2]]; invs h3; invs h2. Qed.
A, B: Type

forall u : propA, u ->> LastA ([|u|])
A, B: Type

forall u : propA, u ->> LastA ([|u|])
A, B: Type
u: propA
a: A
h0: u a

LastA ([|u|]) a
A, B: Type
u: propA
a: A
h0: u a

singletonT u (Tnil a)
A, B: Type
u: propA
a: A
h0: u a
finalTA (Tnil a) a
A, B: Type
u: propA
a: A
h0: u a

singletonT u (Tnil a)
A, B: Type
u: propA
a: A
h0: u a
finalTA (Tnil a) a
A, B: Type
u: propA
a: A
h0: u a

finalTA (Tnil a) a
A, B: Type
u: propA
a: A
h0: u a

finalTA (Tnil a) a
exact: finalTA_nil. Qed.
A, B: Type

forall (p q : trace -> Prop) (a : A), lastA (p *+* q) a -> lastA q a
A, B: Type

forall (p q : trace -> Prop) (a : A), lastA (p *+* q) a -> lastA q a
A, B: Type
p, q: trace -> Prop
a: A
tr0, tr: trace
h2: followsT q tr tr0
h1: finalTA tr0 a

lastA q a
A, B: Type
p, q: trace -> Prop
a: A
H0: q (Tnil a)

lastA q a
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
H0: q (Tcons a b tr0)
lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
tr1: trace
H1: followsT q tr1 tr0
lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
H0: q (Tnil a)

lastA q a
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
H0: q (Tcons a b tr0)
lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
tr1: trace
H1: followsT q tr1 tr0
lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
H0: q (Tnil a)

q (Tnil a) /\ finalTA (Tnil a) a
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
H0: q (Tcons a b tr0)
lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
tr1: trace
H1: followsT q tr1 tr0
lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
H0: q (Tcons a b tr0)

lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
tr1: trace
H1: followsT q tr1 tr0
lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
H0: q (Tcons a b tr0)

lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
tr1: trace
H1: followsT q tr1 tr0
lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
H0: q (Tcons a b tr0)

q (Tcons a b tr0) /\ finalTA (Tcons a b tr0) a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
tr1: trace
H1: followsT q tr1 tr0
lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
tr1: trace
H1: followsT q tr1 tr0

lastA q a'
A, B: Type
p, q: trace -> Prop
a: A
b: B
a': A
tr0: trace
Hfinal: finalTA tr0 a'
IH: forall tr : trace, followsT q tr tr0 -> lastA q a'
tr1: trace
H1: followsT q tr1 tr0

lastA q a'
exact: IH _ H1. Qed.
A, B: Type

forall (p : propT) (v : propA), LastA (p *** ([|v|])) ->> v
A, B: Type

forall (p : propT) (v : propA), LastA (p *** ([|v|])) ->> v
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
tr, tr': trace
h0: followsT (singletonT v) tr' tr
h1: finalTA tr a

v a
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
H0: singletonT v (Tnil a)

v a
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
b: B
a': A
tr: trace
Hfinal: finalTA tr a'
IH: forall tr' : trace, followsT (singletonT v) tr' tr -> v a'
H0: singletonT v (Tcons a b tr)
v a'
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
b: B
a': A
tr: trace
Hfinal: finalTA tr a'
IH: forall tr' : trace, followsT (singletonT v) tr' tr -> v a'
tr1: trace
H1: followsT (singletonT v) tr1 tr
v a'
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
H0: singletonT v (Tnil a)

v a
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
b: B
a': A
tr: trace
Hfinal: finalTA tr a'
IH: forall tr' : trace, followsT (singletonT v) tr' tr -> v a'
H0: singletonT v (Tcons a b tr)
v a'
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
b: B
a': A
tr: trace
Hfinal: finalTA tr a'
IH: forall tr' : trace, followsT (singletonT v) tr' tr -> v a'
tr1: trace
H1: followsT (singletonT v) tr1 tr
v a'
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
b: B
a': A
tr: trace
Hfinal: finalTA tr a'
IH: forall tr' : trace, followsT (singletonT v) tr' tr -> v a'
H0: singletonT v (Tcons a b tr)

v a'
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
b: B
a': A
tr: trace
Hfinal: finalTA tr a'
IH: forall tr' : trace, followsT (singletonT v) tr' tr -> v a'
tr1: trace
H1: followsT (singletonT v) tr1 tr
v a'
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
b: B
a': A
tr: trace
Hfinal: finalTA tr a'
IH: forall tr' : trace, followsT (singletonT v) tr' tr -> v a'
H0: singletonT v (Tcons a b tr)

v a'
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
b: B
a': A
tr: trace
Hfinal: finalTA tr a'
IH: forall tr' : trace, followsT (singletonT v) tr' tr -> v a'
tr1: trace
H1: followsT (singletonT v) tr1 tr
v a'
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
b: B
a': A
tr: trace
Hfinal: finalTA tr a'
IH: forall tr' : trace, followsT (singletonT v) tr' tr -> v a'
tr1: trace
H1: followsT (singletonT v) tr1 tr

v a'
A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
b: B
a': A
tr: trace
Hfinal: finalTA tr a'
IH: forall tr' : trace, followsT (singletonT v) tr' tr -> v a'
tr1: trace
H1: followsT (singletonT v) tr1 tr

v a'
exact: IH _ H1. Qed.
A, B: Type

forall (p : propT) (u : propA), (LastA p andA u) ->> LastA (p *** ([|u|]))
A, B: Type

forall (p : propT) (u : propA), (LastA p andA u) ->> LastA (p *** ([|u|]))
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
a: A
tr0: trace
h2: p tr0
h3: finalTA tr0 a
h1: u a

LastA (exist (fun p : trace -> Prop => setoidT p) p hp *** ([|u|])) a
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
a: A
tr0: trace
h2: p tr0
h3: finalTA tr0 a
h1: u a

(p *+* singletonT u) tr0 /\ finalTA tr0 a
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
a: A
tr0: trace
h2: p tr0
h3: finalTA tr0 a
h1: u a

(p *+* singletonT u) tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
a: A
tr0: trace
h2: p tr0
h3: finalTA tr0 a
h1: u a

p tr0 /\ followsT (singletonT u) tr0 tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
a: A
tr0: trace
h2: p tr0
h3: finalTA tr0 a
h1: u a

followsT (singletonT u) tr0 tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA

forall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
CIH: forall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0

forall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
CIH: forall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0
a: A
h0: u a

followsT (singletonT u) (Tnil a) (Tnil a)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
CIH: forall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0
a, a0: A
b: B
tr: trace
H: finalTA tr a
h0: u a
followsT (singletonT u) (Tcons a0 b tr) (Tcons a0 b tr)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
CIH: forall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0
a: A
h0: u a

followsT (singletonT u) (Tnil a) (Tnil a)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
CIH: forall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0
a, a0: A
b: B
tr: trace
H: finalTA tr a
h0: u a
followsT (singletonT u) (Tcons a0 b tr) (Tcons a0 b tr)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
CIH: forall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0
a, a0: A
b: B
tr: trace
H: finalTA tr a
h0: u a

followsT (singletonT u) (Tcons a0 b tr) (Tcons a0 b tr)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
CIH: forall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0
a, a0: A
b: B
tr: trace
H: finalTA tr a
h0: u a

followsT (singletonT u) (Tcons a0 b tr) (Tcons a0 b tr)
exact: followsT_delay _ _ (CIH _ _ H h0). Qed.
A, B: Type

forall (v : propA) (b : B) (p : propT), LastA (([|v|]) *** IterT (p *** (<< v; b >>))) ->> v
A, B: Type

forall (v : propA) (b : B) (p : propT), LastA (([|v|]) *** IterT (p *** (<< v; b >>))) ->> v
A, B: Type
v: propA
b: B
p: propT
a: A
h0: LastA (([|v|]) *** IterT (p *** (<< v; b >>))) a

v a
A, B: Type
v: propA
b: B
p: propT
a: A
h0: LastA (([|v|]) *** IterT (p *** (<< v; b >>))) a
h1: p =>> TtT

v a
A, B: Type
v: propA
b: B
p: propT
a: A
h0: LastA (([|v|]) *** IterT (p *** (<< v; b >>))) a
h1: p =>> TtT
h2: LastA (([|v|]) *** IterT (TtT *** (<< v; b >>))) a

v a
A, B: Type
v: propA
b: B
p: propT
a: A
h0: LastA (([|v|]) *** IterT (p *** (<< v; b >>))) a
h1: p =>> TtT
h2: LastA (([|v|]) *** IterT (TtT *** (<< v; b >>))) a

LastA (TtT *** ([|v|])) a -> v a
exact: LastA_AppendA. Qed.
A, B: Type

forall (v : propA) (b : B), ((<< v; b >>) *** IterT (TtT *** (<< v; b >>))) =>> TtT *** ([|v|])
A, B: Type

forall (v : propA) (b : B), ((<< v; b >>) *** IterT (TtT *** (<< v; b >>))) =>> TtT *** ([|v|])
A, B: Type
v: propA
b: B
tr0, tr1: trace
a: A
h0: v a
h2: bisim tr1 (Tcons a b (Tnil a))
h1: followsT (iterT (ttT *+* dupT v b)) tr1 tr0

satisfyT (TtT *** ([|v|])) tr0
A, B: Type
v: propA
b: B
tr': trace
h0: v (hd tr')
H1: iterT (ttT *+* dupT v b) tr'

(ttT *+* singletonT v) (Tcons (hd tr') b tr')
A, B: Type
v: propA
b: B
tr': trace
h0: v (hd tr')
H1: iterT (ttT *+* dupT v b) tr'

ttT (Tcons (hd tr') b tr') /\ followsT (singletonT v) (Tcons (hd tr') b tr') (Tcons (hd tr') b tr')
A, B: Type
v: propA
b: B
tr': trace
h0: v (hd tr')
H1: iterT (ttT *+* dupT v b) tr'

followsT (singletonT v) (Tcons (hd tr') b tr') (Tcons (hd tr') b tr')
A, B: Type
v: propA
b: B
tr': trace
h0: v (hd tr')
H1: iterT (ttT *+* dupT v b) tr'

followsT (singletonT v) tr' tr'
A, B: Type
v: propA
b: B

forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'

forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
a: A
h0: v (hd (Tnil a))

followsT (singletonT v) (Tnil a) (Tnil a)
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
tr0: trace
h0: v (hd tr0)
tr: trace
H: (ttT *+* dupT v b) tr
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0
followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
a: A
h0: v (hd (Tnil a))

followsT (singletonT v) (Tnil a) (Tnil a)
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
tr0: trace
h0: v (hd tr0)
tr: trace
H: (ttT *+* dupT v b) tr
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0
followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
tr0: trace
h0: v (hd tr0)
tr: trace
H: (ttT *+* dupT v b) tr
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0

followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
tr0: trace
h0: v (hd tr0)
tr: trace
H: (ttT *+* dupT v b) tr
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0

followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
tr0, tr: trace
H0: followsT (iterT (ttT *+* dupT v b)) tr tr0
tr1: trace
h1: followsT (dupT v b) tr1 tr

followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'

forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0

forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr1, tr2: trace
h1: followsT (iterT (ttT *+* dupT v b)) tr1 tr2
H0: dupT v b tr1

followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'
followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr1, tr2: trace
h1: followsT (iterT (ttT *+* dupT v b)) tr1 tr2
H0: dupT v b tr1

followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'
followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr1, tr2: trace
h1: followsT (iterT (ttT *+* dupT v b)) tr1 tr2
a: A
h0: v a
h2: bisim tr1 (Tcons a b (Tnil a))

followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'
followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr': trace
h0: v (hd tr')
H1: iterT (ttT *+* dupT v b) tr'

followsT (singletonT v) (Tcons (hd tr') b tr') (Tcons (hd tr') b tr')
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'
followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'

followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
tr2: trace
a: A
b0: B
tr, tr': trace
h1: followsT (iterT (ttT *+* dupT v b)) (Tcons a b0 tr') tr2
H: followsT (dupT v b) tr tr'

followsT (singletonT v) tr2 tr2
A, B: Type
v: propA
b: B
CIH: forall tr' : trace, v (hd tr') -> iterT (ttT *+* dupT v b) tr' -> followsT (singletonT v) tr' tr'
CIH0: forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0
a: A
b0: B
tr, tr', tr'0: trace
H: followsT (dupT v b) tr tr'
H4: followsT (iterT (ttT *+* dupT v b)) tr' tr'0

followsT (singletonT v) (Tcons a b0 tr'0) (Tcons a b0 tr'0)
exact: followsT_delay _ _ (CIH0 _ _ _ H H4). Qed.
A, B: Type

forall p q : propT, LastA (([|LastA p|]) *** q) ->> LastA (p *** q)
A, B: Type

forall p q : propT, LastA (([|LastA p|]) *** q) ->> LastA (p *** q)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h0: lastA p (hd tr1)
h1: finalTA tr1 a
H1: q tr1

lastA (p *+* q) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)

lastA (p *+* q) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)

(p *+* q) (tr2 +++ tr1) /\ finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)

(p *+* q) (tr2 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)

(p *+* q) (tr2 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)

p tr2 /\ followsT q tr2 (tr2 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)

followsT q tr2 (tr2 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1

forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)

forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
h0: finalTA (Tnil a0) (hd tr1)

followsT q (Tnil a0) (Tnil a0 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
b: B
tr0: trace
h0: finalTA (Tcons a0 b tr0) (hd tr1)
followsT q (Tcons a0 b tr0) (Tcons a0 b tr0 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
h0: finalTA (Tnil a0) (hd tr1)

followsT q (Tnil a0) (Tnil a0 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
b: B
tr0: trace
h0: finalTA (Tcons a0 b tr0) (hd tr1)
followsT q (Tcons a0 b tr0) (Tcons a0 b tr0 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
h0: finalTA (Tnil a0) (hd tr1)

followsT q (Tnil a0) tr1
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
b: B
tr0: trace
h0: finalTA (Tcons a0 b tr0) (hd tr1)
followsT q (Tcons a0 b tr0) (Tcons a0 b tr0 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
h0: finalTA (Tnil a0) (hd tr1)

hd tr1 = a0
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
b: B
tr0: trace
h0: finalTA (Tcons a0 b tr0) (hd tr1)
followsT q (Tcons a0 b tr0) (Tcons a0 b tr0 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
b: B
tr0: trace
h0: finalTA (Tcons a0 b tr0) (hd tr1)

followsT q (Tcons a0 b tr0) (Tcons a0 b tr0 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
b: B
tr0: trace
h0: finalTA (Tcons a0 b tr0) (hd tr1)

followsT q (Tcons a0 b tr0) (Tcons a0 b tr0 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
b: B
tr0: trace
H4: finalTA tr0 (hd tr1)

followsT q (Tcons a0 b tr0) (Tcons a0 b tr0 +++ tr1)
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1
CIH: forall tr2 : trace, finalTA tr2 (hd tr1) -> followsT q tr2 (tr2 +++ tr1)
a0: A
b: B
tr0: trace
H4: finalTA tr0 (hd tr1)

followsT q (Tcons a0 b tr0) (Tcons a0 b (tr0 +++ tr1))
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)
finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)

finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
H1: q tr1
tr2: trace
h0: p tr2
h2: finalTA tr2 (hd tr1)

finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
h1: finalTA tr1 a
tr2: trace
a0: A
h0: hd tr1 = a0
h2: finalTA tr2 a0

finalTA (tr2 +++ tr1) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a, a0: A
tr0: trace
h0: hd tr0 = a0
h1: finalTA tr0 a

finalTA (Tnil a0 +++ tr0) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a, a0: A
b: B
a1: A
tr2: trace
Hfinal: finalTA tr2 a1
IH: forall tr1 : trace, hd tr1 = a1 -> finalTA tr1 a -> finalTA (tr2 +++ tr1) a
tr0: trace
h0: hd tr0 = a1
h1: finalTA tr0 a
finalTA (Tcons a0 b tr2 +++ tr0) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a, a0: A
tr0: trace
h0: hd tr0 = a0
h1: finalTA tr0 a

finalTA (Tnil a0 +++ tr0) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a, a0: A
b: B
a1: A
tr2: trace
Hfinal: finalTA tr2 a1
IH: forall tr1 : trace, hd tr1 = a1 -> finalTA tr1 a -> finalTA (tr2 +++ tr1) a
tr0: trace
h0: hd tr0 = a1
h1: finalTA tr0 a
finalTA (Tcons a0 b tr2 +++ tr0) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a, a0: A
b: B
a1: A
tr2: trace
Hfinal: finalTA tr2 a1
IH: forall tr1 : trace, hd tr1 = a1 -> finalTA tr1 a -> finalTA (tr2 +++ tr1) a
tr0: trace
h0: hd tr0 = a1
h1: finalTA tr0 a

finalTA (Tcons a0 b tr2 +++ tr0) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a, a0: A
b: B
a1: A
tr2: trace
Hfinal: finalTA tr2 a1
IH: forall tr1 : trace, hd tr1 = a1 -> finalTA tr1 a -> finalTA (tr2 +++ tr1) a
tr0: trace
h0: hd tr0 = a1
h1: finalTA tr0 a

finalTA (Tcons a0 b tr2 +++ tr0) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a, a0: A
b: B
a1: A
tr2: trace
Hfinal: finalTA tr2 a1
IH: forall tr1 : trace, hd tr1 = a1 -> finalTA tr1 a -> finalTA (tr2 +++ tr1) a
tr0: trace
h0: hd tr0 = a1
h1: finalTA tr0 a

finalTA (Tcons a0 b (tr2 +++ tr0)) a
A, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a, a0: A
b: B
a1: A
tr2: trace
Hfinal: finalTA tr2 a1
IH: forall tr1 : trace, hd tr1 = a1 -> finalTA tr1 a -> finalTA (tr2 +++ tr1) a
tr0: trace
h0: hd tr0 = a1
h1: finalTA tr0 a

finalTA (tr2 +++ tr0) a
exact: IH _ h0 h1. Qed.
A, B: Type

forall u v : propA, (v andA u) ->> LastA (([|v|]) *** ([|u|]))
A, B: Type

forall u v : propA, (v andA u) ->> LastA (([|v|]) *** ([|u|]))
A, B: Type
u, v: propA
a: A
h0: v a
h1: u a

LastA (([|v|]) *** ([|u|])) a
A, B: Type
u, v: propA
a: A
h0: v a
h1: u a

(singletonT v *+* singletonT u) (Tnil a)
A, B: Type
u, v: propA
a: A
h0: v a
h1: u a

followsT (singletonT u) (Tnil a) (Tnil a)
exact/followsT_nil/nil_singletonT. Qed. CoFixpoint lastdup (tr : trace) (b : B) : trace := match tr with | Tnil a => Tcons a b (Tnil a) | Tcons a b' tr' => Tcons a b' (lastdup tr' b) end.
A, B: Type

forall (tr : trace) (b : B), hd tr = hd (lastdup tr b)
A, B: Type

forall (tr : trace) (b : B), hd tr = hd (lastdup tr b)
by case => [a b | a b tr b0]; rewrite [lastdup _ _]trace_destr. Qed.
A, B: Type

forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
A, B: Type

forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)

forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
H: hd (Tnil a) = a
H0: singletonT u (Tnil a)

followsT (dupT u b) (Tnil a) (lastdup (Tnil a) b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
b0: B
tr: trace
H1: followsT (singletonT u) tr tr
followsT (dupT u b) (Tcons a b0 tr) (lastdup (Tcons a b0 tr) b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
H: hd (Tnil a) = a
H0: singletonT u (Tnil a)

followsT (dupT u b) (Tnil a) (lastdup (Tnil a) b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
b0: B
tr: trace
H1: followsT (singletonT u) tr tr
followsT (dupT u b) (Tcons a b0 tr) (lastdup (Tcons a b0 tr) b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
H: hd (Tnil a) = a
H0: singletonT u (Tnil a)

followsT (dupT u b) (Tnil a) (Tcons a b (Tnil a))
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
b0: B
tr: trace
H1: followsT (singletonT u) tr tr
followsT (dupT u b) (Tcons a b0 tr) (lastdup (Tcons a b0 tr) b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a0: A
H: hd (Tnil a0) = a0
h0: u a0

followsT (dupT u b) (Tnil a0) (Tcons a0 b (Tnil a0))
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
b0: B
tr: trace
H1: followsT (singletonT u) tr tr
followsT (dupT u b) (Tcons a b0 tr) (lastdup (Tcons a b0 tr) b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a0: A
H: hd (Tnil a0) = a0
h0: u a0

dupT u b (Tcons a0 b (Tnil a0))
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
b0: B
tr: trace
H1: followsT (singletonT u) tr tr
followsT (dupT u b) (Tcons a b0 tr) (lastdup (Tcons a b0 tr) b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
b0: B
tr: trace
H1: followsT (singletonT u) tr tr

followsT (dupT u b) (Tcons a b0 tr) (lastdup (Tcons a b0 tr) b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
b0: B
tr: trace
H1: followsT (singletonT u) tr tr

followsT (dupT u b) (Tcons a b0 tr) (lastdup (Tcons a b0 tr) b)
A, B: Type
CIH: forall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)
u: propA
b: B
a: A
b0: B
tr: trace
H1: followsT (singletonT u) tr tr

followsT (dupT u b) (Tcons a b0 tr) (Tcons a b0 (lastdup tr b))
exact/followsT_delay/CIH. Qed.
A, B: Type

forall (tr : trace) (a : A) (b : B), finalTA tr a -> finalTA (lastdup tr b) a
A, B: Type

forall (tr : trace) (a : A) (b : B), finalTA tr a -> finalTA (lastdup tr b) a
A, B: Type
b1: B
a: A

finalTA (lastdup (Tnil a) b1) a
A, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2
finalTA (lastdup (Tcons a1 b2 tr) b1) a2
A, B: Type
b1: B
a: A

finalTA (lastdup (Tnil a) b1) a
A, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2
finalTA (lastdup (Tcons a1 b2 tr) b1) a2
A, B: Type
b1: B
a: A

finalTA (Tcons a b1 (Tnil a)) a
A, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2
finalTA (lastdup (Tcons a1 b2 tr) b1) a2
A, B: Type
b1: B
a: A

finalTA (Tnil a) a
A, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2
finalTA (lastdup (Tcons a1 b2 tr) b1) a2
A, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2

finalTA (lastdup (Tcons a1 b2 tr) b1) a2
A, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2

finalTA (lastdup (Tcons a1 b2 tr) b1) a2
A, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2

finalTA (Tcons a1 b2 (lastdup tr b1)) a2
exact: finalTA_delay. Qed.
A, B: Type

forall (p : propT) (u : propA) (b : B), LastA (p *** ([|u|])) ->> LastA (p *** (<< u; b >>))
A, B: Type

forall (p : propT) (u : propA) (b : B), LastA (p *** ([|u|])) ->> LastA (p *** (<< u; b >>))
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
b: B
a: A
tr0, tr1: trace
h0: p tr1
h2: followsT (singletonT u) tr1 tr0
h1: finalTA tr0 a

LastA (exist (fun p : trace -> Prop => setoidT p) p hp *** (<< u; b >>)) a
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
b: B
a: A
tr0, tr1: trace
h0: p tr1
h2: followsT (singletonT u) tr1 tr0
h1: finalTA tr0 a

(p *+* dupT u b) (lastdup tr0 b)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
b: B
a: A
tr0, tr1: trace
h0: p tr1
h2: followsT (singletonT u) tr1 tr0
h1: finalTA tr0 a
h3: bisim tr1 tr0

(p *+* dupT u b) (lastdup tr0 b)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
b: B
a: A
tr0, tr1: trace
h0: p tr1
h2: followsT (singletonT u) tr1 tr0
h1: finalTA tr0 a
h3: bisim tr1 tr0

p tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
b: B
a: A
tr0, tr1: trace
h0: p tr1
h2: followsT (singletonT u) tr1 tr0
h1: finalTA tr0 a
h3: bisim tr1 tr0
followsT (dupT u b) tr0 (lastdup tr0 b)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
b: B
a: A
tr0, tr1: trace
h0: p tr1
h2: followsT (singletonT u) tr1 tr0
h1: finalTA tr0 a
h3: bisim tr1 tr0

p tr0
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
b: B
a: A
tr0, tr1: trace
h0: p tr1
h2: followsT (singletonT u) tr1 tr0
h1: finalTA tr0 a
h3: bisim tr1 tr0
followsT (dupT u b) tr0 (lastdup tr0 b)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
b: B
a: A
tr0, tr1: trace
h0: p tr1
h2: followsT (singletonT u) tr1 tr0
h1: finalTA tr0 a
h3: bisim tr1 tr0

followsT (dupT u b) tr0 (lastdup tr0 b)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
b: B
a: A
tr0, tr1: trace
h0: p tr1
h2: followsT (singletonT u) tr1 tr0
h1: finalTA tr0 a
h3: bisim tr1 tr0

followsT (dupT u b) tr0 (lastdup tr0 b)
A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
b: B
a: A
tr0, tr1: trace
h0: p tr1
h1: finalTA tr0 a
h3: bisim tr1 tr0
h4: followsT (singletonT u) tr0 tr0

followsT (dupT u b) tr0 (lastdup tr0 b)
exact: followsT_dupT b h4. Qed.

Midpoint property

This property identifies a trace that is both a suffix of tr0 and a prefix of tr1, and is the stepping stone to showing the right associativity of the append property.
CoInductive midpointT
  (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (appendT p0 p1) tr0 tr1)
  : trace -> Prop :=
| midpointT_nil : forall tr,
   tr0 = Tnil (hd tr1) ->
   p0 tr ->
   followsT p1 tr tr1 ->
   midpointT h tr
| midpointT_delay : forall tr2 tr3 (h1 : followsT (appendT p0 p1) tr2 tr3) (a : A) (b : B) tr',
   tr0 = Tcons a b tr2 ->
   tr1 = Tcons a b tr3 ->
   @midpointT p0 p1 tr2 tr3 h1 tr' ->
   midpointT h (Tcons a b tr').

A, B: Type

forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
A, B: Type

forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'

forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
tr1: trace
h: followsT (p0 *+* p1) (Tnil (hd tr1)) tr1
a0: (p0 *+* p1) tr1

forall tr' : trace, midpointT (followsT_nil eq_refl a0) tr' -> followsT p0 (Tnil (hd tr1)) tr'
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
forall tr'0 : trace, midpointT (followsT_delay a b f) tr'0 -> followsT p0 (Tcons a b tr) tr'0
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
tr1: trace
h: followsT (p0 *+* p1) (Tnil (hd tr1)) tr1
a0: (p0 *+* p1) tr1

forall tr' : trace, midpointT (followsT_nil eq_refl a0) tr' -> followsT p0 (Tnil (hd tr1)) tr'
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
forall tr'0 : trace, midpointT (followsT_delay a b f) tr'0 -> followsT p0 (Tcons a b tr) tr'0
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
tr1: trace
h: followsT (p0 *+* p1) (Tnil (hd tr1)) tr1
a0: (p0 *+* p1) tr1
tr': trace
hm: midpointT (followsT_nil eq_refl a0) tr'

followsT p0 (Tnil (hd tr1)) tr'
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
forall tr'0 : trace, midpointT (followsT_delay a b f) tr'0 -> followsT p0 (Tcons a b tr) tr'0
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
tr1, tr': trace
H0: p0 tr'
H1: followsT p1 tr' tr1
x: trace
H2: p0 x
H3: followsT p1 x tr1
H4: hd tr1 = hd tr1
H5: (p0 *+* p1) tr1

followsT p0 (Tnil (hd tr1)) tr'
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
forall tr'0 : trace, midpointT (followsT_delay a b f) tr'0 -> followsT p0 (Tcons a b tr) tr'0
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
tr1, tr': trace
H0: p0 tr'
H1: followsT p1 tr' tr1
x: trace
H2: p0 x
H3: followsT p1 x tr1
H4: hd tr1 = hd tr1
H5: (p0 *+* p1) tr1

hd tr' = hd tr1
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
forall tr'0 : trace, midpointT (followsT_delay a b f) tr'0 -> followsT p0 (Tcons a b tr) tr'0
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'

forall tr'0 : trace, midpointT (followsT_delay a b f) tr'0 -> followsT p0 (Tcons a b tr) tr'0
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'

forall tr'0 : trace, midpointT (followsT_delay a b f) tr'0 -> followsT p0 (Tcons a b tr) tr'0
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
a0: A
b0: B
tr0: trace
hm: midpointT (followsT_delay a b f) (Tcons a0 b0 tr0)

followsT p0 (Tcons a b tr) (Tcons a0 b0 tr0)
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'
p0, p1: trace -> Prop
a0: A
b0: B
tr2, tr3: trace
h: followsT (p0 *+* p1) (Tcons a0 b0 tr2) (Tcons a0 b0 tr3)
f: followsT (p0 *+* p1) tr2 tr3
tr0: trace
h1: followsT (p0 *+* p1) tr2 tr3
H4: midpointT h1 tr0

followsT p0 (Tcons a0 b0 tr2) (Tcons a0 b0 tr0)
exact: followsT_delay _ _ (CIH _ _ _ _ h1 _ _). Qed.
A, B: Type

forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1
A, B: Type

forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1

forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1
p0, p1: trace -> Prop
tr1: trace
h: followsT (p0 *+* p1) (Tnil (hd tr1)) tr1
a0: (p0 *+* p1) tr1
tr0: trace
hm: midpointT (followsT_nil eq_refl a0) tr0

followsT p1 tr0 tr1
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
tr0: trace
hm: midpointT (followsT_delay a b f) tr0
followsT p1 tr0 (Tcons a b tr')
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1
p0, p1: trace -> Prop
tr1: trace
h: followsT (p0 *+* p1) (Tnil (hd tr1)) tr1
a0: (p0 *+* p1) tr1
tr0: trace
hm: midpointT (followsT_nil eq_refl a0) tr0

followsT p1 tr0 tr1
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
tr0: trace
hm: midpointT (followsT_delay a b f) tr0
followsT p1 tr0 (Tcons a b tr')
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
tr0: trace
hm: midpointT (followsT_delay a b f) tr0

followsT p1 tr0 (Tcons a b tr')
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
tr0: trace
hm: midpointT (followsT_delay a b f) tr0

followsT p1 tr0 (Tcons a b tr')
A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1
p0, p1: trace -> Prop
a0: A
b0: B
tr2, tr3: trace
h: followsT (p0 *+* p1) (Tcons a0 b0 tr2) (Tcons a0 b0 tr3)
f: followsT (p0 *+* p1) tr2 tr3
tr'0: trace
h1: followsT (p0 *+* p1) tr2 tr3
H1: midpointT h1 tr'0

followsT p1 (Tcons a0 b0 tr'0) (Tcons a0 b0 tr3)
exact: followsT_delay _ _ (CIH _ _ _ _ h1 _ _). Qed. End sec_trace_properties.

Trace property operators and notations

Identifier 'andT' now a keyword
Identifier 'orT' now a keyword
Infix "=>>" := propT_imp (at level 60, right associativity). Infix "->>" := propA_imp (at level 60, right associativity).
Identifier 'andA' now a keyword
Notation "[| p |]" := (@SingletonT _ _ p) (at level 80). Infix "*+*" := appendT (at level 60, right associativity). Infix "***" := AppendT (at level 60, right associativity). Notation "<< p ; b >>" := (@DupT _ _ p b) (at level 80).