From Coq Require Import Program.Equality.Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits.
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 }.
CoInductive infiniteT : trace -> Prop := | infiniteT_delay : forall a b tr, infiniteT tr -> infiniteT (Tcons a b tr).A, B: TypesetoidT infiniteTA, B: TypesetoidT infiniteTA, B: Type
CIH: setoidT infiniteTsetoidT infiniteTexact: (infiniteT_delay a b (CIH _ H _ H4)). Qed. Definition InfiniteT : propT := exist _ (fun tr => infiniteT tr) infiniteT_setoidT.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')A, B: Typeforall (a : A) (b : B) (tr : trace), infiniteT (Tcons a b tr) -> infiniteT trby move => a b tr Hinf; inversion Hinf. Qed.A, B: Typeforall (a : A) (b : B) (tr : trace), infiniteT (Tcons a b tr) -> infiniteT trA, B: Typeforall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr' +++ tr)A, B: Typeforall 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 trforall 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': traceinfiniteT (Tcons a b tr' +++ tr)exact/infiniteT_delay/CIH. Qed.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': traceinfiniteT (Tcons a b (tr' +++ tr))A, B: Typeforall tr : trace, infiniteT tr -> forall tr' : trace, infiniteT (tr +++ tr')A, B: Typeforall 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': traceinfiniteT (Tcons a b tr0 +++ tr')exact/infiniteT_delay/CIH. Qed.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': traceinfiniteT (Tcons a b (tr0 +++ tr'))
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: TypesetoidT finiteTA, B: TypesetoidT finiteTA, B: Type
tr1: trace
a: AfiniteT (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: AfiniteT (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')exact/finiteT_delay/IH. Qed. Definition FiniteT : propT := exist _ (fun tr => finiteT tr) finiteT_setoidT.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
a: A
b: B
tr: trace
h: finiteT (Tcons a b tr)finiteT trby inversion h. Defined.A, B: Type
a: A
b: B
tr: trace
h: finiteT (Tcons a b tr)finiteT tr
Equality coincides with bisimilarity for finite traces.
A, B: Typeforall tr : trace, finiteT tr -> forall tr' : trace, bisim tr tr' -> tr = tr'A, B: Typeforall tr : trace, finiteT tr -> forall tr' : trace, bisim tr tr' -> tr = tr'by rewrite (IH _ H3). Qed.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'0Tcons a b tr0 = Tcons a b tr'0
Basic connections between finiteness and infiniteness.
A, B: Typeforall tr : trace, finiteT tr -> infiniteT tr -> Falseby move => tr; elim => [a | a b tr' Hfin IH] Hinf; inversion Hinf. Qed.A, B: Typeforall tr : trace, finiteT tr -> infiniteT tr -> FalseA, B: Typeforall tr : trace, ~ finiteT tr -> infiniteT trA, B: Typeforall tr : trace, ~ finiteT tr -> infiniteT trA, B: Type
CIH: forall tr : trace, ~ finiteT tr -> infiniteT trforall tr : trace, ~ finiteT tr -> infiniteT trA, 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 trA, B: Type
a: A
b: B
tr: trace
Hfin: ~ finiteT (Tcons a b tr)
Hinf: finiteT trFalseexact: finiteT_delay. Qed.A, B: Type
a: A
b: B
tr: trace
Hinf: finiteT trfiniteT (Tcons a b tr)
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: Typeforall (tr : trace) (a : A), finalTA tr a -> finiteT trA, B: Typeforall (tr : trace) (a : A), finalTA tr a -> finiteT trA, B: Type
tr: trace
a, a1: AfiniteT (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: AfiniteT (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')exact/finiteT_delay/IH. Qed.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: Typeforall (tr : trace) (b : B), finalTB tr b -> finiteT trA, B: Typeforall (tr : trace) (b : B), finalTB tr b -> finiteT trA, B: Type
tr: trace
b: B
a1: A
b1: B
a2: AfiniteT (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 a2finiteT (Tcons a1 b1 a2)A, B: Type
tr: trace
b: B
a1: A
b1: B
a2: AfiniteT (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 a2finiteT (Tcons a1 b1 a2)A, B: Type
tr: trace
b: B
a1: A
b1, b2: B
a2: trace
Hfin: finalTB a2 b2
IH: finiteT a2finiteT (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
tr: trace
b: B
a1: A
b1, b2: B
a2: trace
Hfin: finalTB a2 b2
IH: finiteT a2finiteT (Tcons a1 b1 a2)A, B: Typeforall (tr : trace) (h : finiteT tr), finalTA tr (finalA h)A, B: Typeforall (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 trfinalTA 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 = afinalTA (Tnil a) aA, 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 = trfinalTA (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 = afinalTA (Tnil a) aA, 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 = trfinalTA (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 = trfinalTA (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
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 = trfinalTA (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: Typeforall (tr0 : trace) (a : A), finalTA tr0 a -> forall tr1 : trace, hd tr1 = a -> hd (tr0 +++ tr1) = hd tr0by move => tr a; elim => {tr a} [a tr <- | a b a' tr Hfinal IH tr'] //=. Qed.A, B: Typeforall (tr0 : trace) (a : A), finalTA tr0 a -> forall tr1 : trace, hd tr1 = a -> hd (tr0 +++ tr1) = hd tr0
Definition ttT : trace -> Prop := fun tr => True.A, B: TypesetoidT ttTby []. Qed. Definition TtT : propT := exist _ ttT ttT_setoidT. Definition ffT : trace -> Prop := fun tr => False.A, B: TypesetoidT ttTA, B: TypesetoidT ffTby []. Qed. Definition FfT : propT := exist _ ffT ffT_setoidT. Definition notT (p : trace -> Prop) : trace -> Prop := fun tr => ~ p tr.A, B: TypesetoidT ffTA, B: Typeforall p : trace -> Prop, setoidT p -> setoidT (notT p)A, B: Typeforall 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'Falseapply: 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: Type
p: trace -> Prop
hp: setoidT p
tr, tr': trace
h2: bisim tr tr'
h3: p tr'p trA, B, T: Type
p: T -> propTsetoidT (fun tr : trace => exists x : T, satisfyT (p x) tr)A, B, T: Type
p: T -> propTsetoidT (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 tr1exists x : T, satisfyT (p x) tr1A, B, T: Type
p: T -> propT
tr0: trace
x: T
h0: satisfyT (p x) tr0
tr1: trace
h1: bisim tr0 tr1satisfyT (p x) tr1exact: h2 _ h0 _ h1. Defined.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 tr0f0 tr1A, B: Typeforall f0 f1 : trace -> Prop, setoidT f0 -> setoidT f1 -> setoidT (fun tr : trace => f0 tr /\ f1 tr)A, B: Typeforall 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 tr1f0 tr1A, 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 tr1f1 tr1A, 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 tr1f0 tr1A, 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 tr1f1 tr1A, 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 tr1f1 tr1exact: 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).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 tr1f1 tr1A, B: Typeforall f0 f1 : trace -> Prop, setoidT f0 -> setoidT f1 -> setoidT (fun tr : trace => f0 tr \/ f1 tr)A, B: Typeforall 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 tr1f0 tr1 \/ f1 tr1A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f1 tr0
tr1: trace
h3: bisim tr0 tr1f0 tr1 \/ f1 tr1A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f0 tr0
tr1: trace
h3: bisim tr0 tr1f0 tr1 \/ f1 tr1A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f1 tr0
tr1: trace
h3: bisim tr0 tr1f0 tr1 \/ f1 tr1A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f1 tr0
tr1: trace
h3: bisim tr0 tr1f0 tr1 \/ f1 tr1by 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).A, B: Type
f0, f1: trace -> Prop
h0: setoidT f0
h1: setoidT f1
tr0: trace
h2: f1 tr0
tr1: trace
h3: bisim tr0 tr1f0 tr1 \/ f1 tr1Definition 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: Typeforall p0 p1 q : propT, p0 =>> p1 -> p1 =>> q -> p0 =>> qA, B: Typeforall p0 p1 q : propT, p0 =>> p1 -> p1 =>> q -> p0 =>> qexact/h1/h0. Qed.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 tr0q tr0A, B: Typeforall p q0 q1 : propT, q0 =>> q1 -> p =>> q0 -> p =>> q1A, B: Typeforall p q0 q1 : propT, q0 =>> q1 -> p =>> q0 -> p =>> q1exact/h0/h1. Qed.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 tr0q1 tr0A, B: Typeforall p q0 q1 : propT, p =>> q0 -> p =>> q1 -> p =>> q0 andT q1A, B: Typeforall p q0 q1 : propT, p =>> q0 -> p =>> q1 -> p =>> q0 andT q1A, 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 tr0q0 tr0 /\ q1 tr0A, 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 tr0q0 tr0A, 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 tr0q1 tr0A, 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 tr0q0 tr0A, 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 tr0q1 tr0A, 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 tr0q1 tr0exact: h1. Qed.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 tr0q1 tr0A, B: Typeforall p : propT, p =>> pby move => p. Qed.A, B: Typeforall p : propT, p =>> pA, B: Typeforall p0 p1 : propT, p0 =>> p1 -> forall tr : trace, satisfyT p0 tr -> satisfyT p1 trA, B: Typeforall p0 p1 : propT, p0 =>> p1 -> forall tr : trace, satisfyT p0 tr -> satisfyT p1 trexact: h2. Qed.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 trf1 trA, B: Typeforall p q r : propT, p =>> q -> q =>> r -> p =>> rA, B: Typeforall p q r : propT, p =>> q -> q =>> r -> p =>> rexact/(satisfyT_cont h1)/(satisfyT_cont h0 h2). Qed.A, B: Type
p, q, r: propT
h0: p =>> q
h1: q =>> r
tr0: trace
h2: satisfyT p tr0satisfyT r tr0A, B: Typeforall p1 p2 : propT, p1 =>> p1 orT p2by move => [f1 hf1] [f2 hf2] tr /= h1; left. Qed.A, B: Typeforall p1 p2 : propT, p1 =>> p1 orT p2A, B: Typeforall p1 p2 : propT, p2 =>> p1 orT p2by move => [f1 hf1] [f2 hf2] tr /= h1; right. Qed.A, B: Typeforall p1 p2 : propT, p2 =>> p1 orT p2
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.Definition exA {T : Type} (u : T -> propA) : propA := fun st => exists x, u x st.
Definition singletonT (u : propA) : trace -> Prop := fun tr => exists a, u a /\ bisim tr (Tnil a).A, B: Typeforall (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: Typeforall (u : propA) (a : A), u a -> singletonT u (Tnil a)A, B: Typeforall u : propA, setoidT (singletonT u)A, B: Typeforall u : propA, setoidT (singletonT u)exact: nil_singletonT. Qed.A, B: Type
u: propA
a: A
h0: u asingletonT u (Tnil a)A, B: Typeforall u v : propA, u ->> v -> forall tr : trace, singletonT u tr -> singletonT v trA, B: Typeforall u v : propA, u ->> v -> forall tr : trace, singletonT u tr -> singletonT v trexact/nil_singletonT/huv. Qed.A, B: Type
u, v: propA
huv: u ->> v
a: A
h0: u asingletonT v (Tnil a)A, B: Typeforall (u : propA) (a : A), singletonT u (Tnil a) -> u aby 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: Typeforall (u : propA) (a : A), singletonT u (Tnil a) -> u aA, B: Typeforall u v : propA, u ->> v -> ([|u|]) =>> ([|v|])A, B: Typeforall u v : propA, u ->> v -> ([|u|]) =>> ([|v|])exact/nil_singletonT/h0. Qed.A, B: Type
u, v: propA
h0: u ->> v
a: A
h1: u asatisfyT ([|v|]) (Tnil a)
Definition dupT (u : propA) (b : B) : trace -> Prop := fun tr => exists a, u a /\ bisim tr (Tcons a b (Tnil a)).A, B: Typeforall (u : propA) (a : A) (b : B), u a -> dupT u b (Tcons a b (Tnil a))A, B: Typeforall (u : propA) (a : A) (b : B), u a -> dupT u b (Tcons a b (Tnil a))by exists a; split; [apply: h | apply: bisim_refl]. Qed.A, B: Type
u: propA
a: A
b: B
h: u adupT u b (Tcons a b (Tnil a))A, B: Typeforall (u0 u1 : propA) (b : B), u0 ->> u1 -> forall tr : trace, dupT u0 b tr -> dupT u1 b trA, B: Typeforall (u0 u1 : propA) (b : B), u0 ->> u1 -> forall tr : trace, dupT u0 b tr -> dupT u1 b trexact/dupT_Tcons/hu. Qed.A, B: Type
u0, u1: propA
b: B
hu: u0 ->> u1
a: A
h0: u0 adupT u1 b (Tcons a b (Tnil a))A, B: Typeforall (u : propA) (b : B), setoidT (dupT u b)A, B: Typeforall (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 tr1dupT u b tr1exact/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
u: propA
b: B
a: A
h0: u adupT u b (Tcons a b (Tnil a))A, B: Typeforall (u v : propA) (b : B), u ->> v -> (<< u; b >>) =>> (<< v; b >>)A, B: Typeforall (u v : propA) (b : B), u ->> v -> (<< u; b >>) =>> (<< v; b >>)exact: dupT_cont. Qed.A, B: Type
u, v: propA
b: B
h0: u ->> v
tr0: tracedupT u b tr0 -> dupT v b tr0
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: Typeforall (p : trace -> Prop) (tr0 tr1 : trace), followsT p tr0 tr1 -> hd tr0 = hd tr1by move => p tr0 tr1 h0; invs h0. Qed.A, B: Typeforall (p : trace -> Prop) (tr0 tr1 : trace), followsT p tr0 tr1 -> hd tr0 = hd tr1A, B: Typeforall (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: Typeforall (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'}}}})%typeA, 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'}}}})%typeA, 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'}}}})%typeA, 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'}}}})%typeA, 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'}}}})%typeA, 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'}}}})%typeA, 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'}}}})%typeA, 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'}}}})%typeA, 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'}}}})%typeA, 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'}}}})%typeA, 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'}}}})%typeby right; exists tr0, tr1, a, b; inversion h. Defined.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'}}}})%typeA, B: Typeforall 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 tr3A, B: Typeforall 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 tr3A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3A, 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 tr3forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> forall tr3 : trace, bisim tr1 tr3 -> followsT p tr2 tr3A, 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 tr1followsT p tr2 tr3A, 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 tr3A, 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 tr1followsT p tr2 tr3A, 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 tr3A, 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 tr1followsT p (Tnil (hd tr1)) tr3A, 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 tr3A, 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 tr3followsT p (Tnil (hd tr1)) tr3A, 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 tr3A, 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 tr1followsT p (Tnil (hd tr1)) tr3A, 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 tr3A, 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 tr3A, 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 tr3exact: (followsT_delay a b (CIH _ _ H _ H5 _ H4)). Qed.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'1followsT p (Tcons a b tr'1) (Tcons a b tr'0)A, B: Typeforall (p : trace -> Prop) (tr0 tr1 : trace), followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1A, B: Typeforall (p : trace -> Prop) (tr0 tr1 : trace), followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1A, B: Type
p: trace -> Propforall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1A, B: Type
p: trace -> Prop
CIH: forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1forall tr0 tr1 : trace, followsT p tr0 tr1 -> forall tr2 : trace, bisim tr0 tr2 -> followsT p tr2 tr1A, 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 tr0followsT p (Tnil (hd tr0)) tr0A, 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'0followsT 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 tr0followsT p (Tnil (hd tr0)) tr0A, 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'0followsT 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'0followsT p (Tcons a b tr'0) (Tcons a b tr')exact: (followsT_delay a b (CIH _ _ H _ H4)). Qed.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'0followsT p (Tcons a b tr'0) (Tcons a b tr')A, B: Typeforall 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 tr1A, B: Typeforall 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 tr1A, B: Type
p: trace -> Prop
hp: forall tr0 : trace, p tr0 -> forall tr1 : trace, bisim tr0 tr1 -> p tr1forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1A, 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 tr1forall tr tr0 : trace, followsT p tr tr0 -> forall tr1 : trace, bisim tr0 tr1 -> followsT p tr tr1A, 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 tr0followsT p (Tnil (hd tr0)) tr1A, 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) tr1A, 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 tr0followsT p (Tnil (hd tr0)) tr1A, 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) tr1A, 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 tr0p tr1A, 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) tr1A, 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) tr1A, 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) tr1exact: (followsT_delay a b (CIH _ _ H _ H4)). Qed.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'0followsT p (Tcons a b tr2) (Tcons a b tr'0)A, B: Typeforall p q : trace -> Prop, (forall tr : trace, p tr -> q tr) -> forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1A, B: Typeforall p q : trace -> Prop, (forall tr : trace, p tr -> q tr) -> forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1A, B: Type
p, q: trace -> Prop
hpq: forall tr : trace, p tr -> q trforall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1A, 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 tr1forall tr0 tr1 : trace, followsT p tr0 tr1 -> followsT q tr0 tr1A, 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 tr1followsT q (Tnil (hd tr1)) tr1A, 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 tr1followsT q (Tnil (hd tr1)) tr1A, 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 tr1q tr1A, 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
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: Typeforall (u : propA) (tr0 tr1 : trace), followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1A, B: Typeforall (u : propA) (tr0 tr1 : trace), followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1A, B: Type
u: propAforall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1A, B: Type
u: propA
CIH: forall tr0 tr1 : trace, followsT (singletonT u) tr0 tr1 -> bisim tr0 tr1
tr1: trace
H0: singletonT u tr1bisim (Tnil (hd tr1)) tr1A, 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 tr1bisim (Tnil (hd tr1)) tr1A, 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 abisim (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')exact/bisim_cons/CIH. Qed.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: Typeforall (u0 u1 : propA) (tr0 : trace), followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0A, B: Typeforall (u0 u1 : propA) (tr0 : trace), followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0A, B: Type
u0, u1: propAforall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u0) tr0 tr0forall 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 tr0forall (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 tr0forall 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 tr0forall (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 afollowsT (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 tr0forall (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 tr0forall (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 tr0forall (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 tr0forall (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 tr0forall (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 tr0forall (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 tr0forall (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 tr0forall (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)exact/followsT_delay/CIH. Qed.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 tr0followsT (singletonT u0) (Tcons a b tr0) (Tcons a b tr0)A, B: Typeforall (u0 u1 : propA) (tr0 : trace), followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0A, B: Typeforall (u0 u1 : propA) (tr0 : trace), followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0A, B: Type
u0, u1: propAforall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0A, B: Type
u0, u1: propA
CIH: forall tr0 : trace, followsT (singletonT (u0 andA u1)) tr0 tr0 -> followsT (singletonT u1) tr0 tr0forall 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 tr0forall (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 tr0forall 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 tr0forall (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 afollowsT (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 tr0forall (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 tr0forall (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 tr0forall (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 tr0forall (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 tr0forall (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 tr0forall (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 tr0forall (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 tr0forall (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)exact/followsT_delay/CIH. Qed.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 tr0followsT (singletonT u1) (Tcons a b tr0) (Tcons a b tr0)A, B: Typeforall (u v : propA) (tr : trace), followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr trA, B: Typeforall (u v : propA) (tr : trace), followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr trA, B: Type
u, v: propAforall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr trA, 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 trforall tr : trace, followsT (singletonT u) tr tr -> followsT (singletonT v) tr tr -> followsT (singletonT (u andA v)) tr trA, 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 tr0followsT (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 tr0followsT (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 tr0followsT (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) aA, 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 tr0followsT (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 tr0followsT (singletonT (u andA v)) (Tcons a b tr0) (Tcons a b tr0)exact/followsT_delay/CIH. Qed.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 tr0followsT (singletonT (u andA v)) (Tcons a b tr0) (Tcons a b tr0)A, B: Typeforall tr : trace, followsT (singletonT ttA) tr trA, B: Typeforall tr : trace, followsT (singletonT ttA) tr trA, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr trforall tr : trace, followsT (singletonT ttA) tr trA, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: AfollowsT (singletonT ttA) (Tnil a) (Tnil a)A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A
b: B
tr0: tracefollowsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: AfollowsT (singletonT ttA) (Tnil a) (Tnil a)A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A
b: B
tr0: tracefollowsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: AsingletonT ttA (Tnil a)A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A
b: B
tr0: tracefollowsT (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: tracefollowsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)exact/followsT_delay/CIH. Qed.A, B: Type
CIH: forall tr : trace, followsT (singletonT ttA) tr tr
a: A
b: B
tr0: tracefollowsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)
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: Typeforall 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) trA, B: Typeforall 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) trA, 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) trA, 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 trfollowsT q1 tr0 trA, B: Type
p0, p1, q0, q1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
hq: forall tr : trace, q0 tr -> q1 trforall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 trA, 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 trforall tr0 tr : trace, followsT q0 tr0 tr -> followsT q1 tr0 trA, 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 tr1followsT q1 (Tnil (hd tr1)) tr1A, 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 tr1followsT q1 (Tnil (hd tr1)) tr1A, 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 tr1q1 tr1A, 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
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: Typeforall p0 p1 q : trace -> Prop, (forall tr : trace, p0 tr -> p1 tr) -> forall tr : trace, (p0 *+* q) tr -> (p1 *+* q) trA, B: Typeforall p0 p1 q : trace -> Prop, (forall tr : trace, p0 tr -> p1 tr) -> forall tr : trace, (p0 *+* q) tr -> (p1 *+* q) trexact: (@appendT_cont _ _ q q hp _). Qed.A, B: Type
p0, p1, q: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
tr: trace(p0 *+* q) tr -> (p1 *+* q) trA, B: Typeforall p q0 q1 : trace -> Prop, (forall tr : trace, q0 tr -> q1 tr) -> forall tr : trace, (p *+* q0) tr -> (p *+* q1) trA, B: Typeforall p q0 q1 : trace -> Prop, (forall tr : trace, q0 tr -> q1 tr) -> forall tr : trace, (p *+* q0) tr -> (p *+* q1) trexact: (@appendT_cont p p _ _ _ hq). Qed.A, B: Type
p, q0, q1: trace -> Prop
hq: forall tr : trace, q0 tr -> q1 tr
tr: trace(p *+* q0) tr -> (p *+* q1) trA, B: Typeforall p0 p1 : trace -> Prop, setoidT p1 -> setoidT (p0 *+* p1)A, B: Typeforall 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) tr1A, 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) tr1exact: (followsT_setoidT_R hp1 h2 h1). Qed.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 tr0followsT p1 tr2 tr1A, B: Typeforall (p q : trace -> Prop) (tr0 tr1 tr2 : trace), followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2A, B: Typeforall (p q : trace -> Prop) (tr0 tr1 tr2 : trace), followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2A, B: Type
p, q: trace -> Propforall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2forall (a : A) (tr1 tr2 : trace), followsT p (Tnil a) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tnil a) tr2A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2forall (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) tr2A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2forall (a : A) (tr1 tr2 : trace), followsT p (Tnil a) tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) (Tnil a) tr2A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2forall (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) tr2A, 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 tr1followsT (p *+* q) (Tnil (hd tr1)) tr2A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2forall (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) tr2A, 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 tr2followsT (p *+* q) (Tnil (hd tr1)) tr2A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2forall (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) tr2A, 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) tr2A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2forall (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) tr2A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2forall (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) tr2A, B: Type
p, q: trace -> Prop
CIH: forall tr0 tr1 tr2 : trace, followsT p tr0 tr1 -> followsT q tr1 tr2 -> followsT (p *+* q) tr0 tr2forall (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) tr2exact: followsT_delay _ _ (CIH _ _ _ H3 H4). Qed.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'0followsT (p *+* q) (Tcons a b tr0) (Tcons a b tr'0)A, B: Typeforall (p1 p2 p3 : trace -> Prop) (tr : trace), ((p1 *+* p2) *+* p3) tr -> (p1 *+* p2 *+* p3) trA, B: Typeforall (p1 p2 p3 : trace -> Prop) (tr : trace), ((p1 *+* p2) *+* p3) tr -> (p1 *+* p2 *+* p3) trA, B: Type
p1, p2, p3: trace -> Prop
tr0: trace
h1: ((p1 *+* p2) *+* p3) tr0(p1 *+* p2 *+* p3) tr0A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h1: (p1 *+* p2) tr1
h2: followsT p3 tr1 tr0(p1 *+* p2 *+* p3) tr0A, 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) tr0A, 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) tr0A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h2: followsT p3 tr1 tr0
tr2: trace
h3: followsT p2 tr2 tr1followsT (p2 *+* p3) tr2 tr0A, B: Type
p1, p2, p3: trace -> Propforall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0A, 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 tr0forall tr2 tr0 tr1 : trace, followsT p3 tr1 tr0 -> followsT p2 tr2 tr1 -> followsT (p2 *+* p3) tr2 tr0A, 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 tr2followsT (p2 *+* p3) (Tnil (hd tr2)) tr1A, 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) tr1A, 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 tr2followsT (p2 *+* p3) (Tnil (hd tr2)) tr1A, 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) tr1A, 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 tr2hd tr1 = hd tr2A, 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) tr1A, 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 tr2hd tr2 = hd tr1A, 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) tr1A, 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) tr1A, 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) tr1exact: followsT_delay _ _ (CIH _ _ _ H4 H). Qed.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'0followsT (p2 *+* p3) (Tcons a b tr) (Tcons a b tr'0)A, B: Typeforall (p q : trace -> Prop) (tr0 tr1 : trace), p tr0 -> q tr1 -> finalTA tr0 (hd tr1) -> (p *+* q) (tr0 +++ tr1)A, B: Typeforall (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 -> Propforall 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) tr0A, 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 tr0followsT q (Tnil (hd tr0)) tr0A, 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)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
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))A, B: Typeforall p1 p2 p3 : propT, ((p1 *** p2) *** p3) =>> p1 *** p2 *** p3A, B: Typeforall p1 p2 p3 : propT, ((p1 *** p2) *** p3) =>> p1 *** p2 *** p3exact: appendT_assoc_L. Qed.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) tr0A, B: Typeforall p1 p2 q1 q2 : propT, p1 =>> p2 -> q1 =>> q2 -> (p1 *** q1) =>> p2 *** q2A, B: Typeforall p1 p2 q1 q2 : propT, p1 =>> p2 -> q1 =>> q2 -> (p1 *** q1) =>> p2 *** q2A, 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) tr0A, 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) tr0forall tr : trace, p1 tr -> p2 trA, 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) tr0forall tr : trace, q1 tr -> q2 trA, 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) tr0forall tr : trace, p1 tr -> p2 trA, 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) tr0forall tr : trace, q1 tr -> q2 trA, 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) tr0forall tr : trace, q1 tr -> q2 trexact: h1. Qed.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) tr0forall tr : trace, q1 tr -> q2 trA, B: Typeforall p1 p2 q : propT, p1 =>> p2 -> (p1 *** q) =>> p2 *** qA, B: Typeforall p1 p2 q : propT, p1 =>> p2 -> (p1 *** q) =>> p2 *** qexact: appendT_cont_L. Qed.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) tr0A, B: Typeforall q p1 p2 : propT, p1 =>> p2 -> (q *** p1) =>> q *** p2A, B: Typeforall q p1 p2 : propT, p1 =>> p2 -> (q *** p1) =>> q *** p2exact: (@appendT_cont q q p1 p2). Qed.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) tr0A, B: Typeforall p : propT, p =>> p *** ([|ttA|])A, B: Typeforall p : propT, p =>> p *** ([|ttA|])A, B: Type
f: trace -> Prop
hp: setoidT f
tr0: trace
h0: f tr0(f *+* singletonT ttA) tr0A, B: Type
f: trace -> Prop
hp: setoidT f
tr0: trace
h0: f tr0followsT (singletonT ttA) tr0 tr0A, B: Type
f: trace -> Propforall tr0 : trace, followsT (singletonT ttA) tr0 tr0A, B: Type
f: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0forall tr0 : trace, followsT (singletonT ttA) tr0 tr0A, B: Type
f: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: AfollowsT (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: tracefollowsT (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: AfollowsT (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: tracefollowsT (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: tracefollowsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)exact/followsT_delay/CIH. Qed.A, B: Type
f: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: tracefollowsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)A, B: Typeforall (u v : propA) (b : B), (([|u|]) *** (<< v; b >>)) =>> (<< u andA v; b >>)A, B: Typeforall (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 tr0dupT (u andA v) b tr0exact: dupT_Tcons. Qed.A, B: Type
u, v: propA
b: B
a: A
h0: u (hd (Tcons a b (Tnil a)))
h1: v adupT (u andA v) b (Tcons a b (Tnil a))A, B: Typeforall (u v : propA) (b : B), (<< u andA v; b >>) =>> ([|u|]) *** (<< v; b >>)A, B: Typeforall (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 asatisfyT (([|u|]) *** (<< v; b >>)) (Tcons a b (Tnil a))A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v afollowsT (dupT v b) (Tnil a) (Tcons a b (Tnil a))exact: dupT_Tcons. Qed.A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v adupT v b (Tcons a b (Tnil a))A, B: Typeforall (u v : propA) (b : B), (<< u andA v; b >>) =>> (<< u; b >>) *** ([|v|])A, B: Typeforall (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 asatisfyT ((<< u; b >>) *** ([|v|])) (Tcons a b (Tnil a))A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v adupT u b (Tcons a b (Tnil a))A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v afollowsT (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 adupT u b (Tcons a b (Tnil a))A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v afollowsT (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 afollowsT (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 afollowsT (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 afollowsT (singletonT v) (Tnil a) (Tnil a)exact: nil_singletonT. Qed.A, B: Type
u, v: propA
b: B
a: A
hu: u a
hv: v asingletonT v (Tnil a)A, B: Typeforall (u v : propA) (b : B), ((<< u; b >>) *** ([|v|])) =>> (<< u andA v; b >>)A, B: Typeforall (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 tr0satisfyT (<< u andA v; b >>) tr0exact: dupT_Tcons. Qed.A, B: Type
u, v: propA
b: B
a: A
hu: u (hd (Tnil a))
hv: v adupT (u andA v) b (Tcons a b (Tnil a))A, B: Typeforall u v : propA, (([|u|]) *** ([|v|])) =>> ([|u andA v|])A, B: Typeforall 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 tr0satisfyT ([|u andA v|]) tr0exact: nil_singletonT. Qed.A, B: Type
u, v: propA
a: A
hu: u (hd (Tnil a))
hv: v asingletonT (u andA v) (Tnil a)A, B: Typeforall u v : propA, ([|u andA v|]) =>> ([|u|]) *** ([|v|])A, B: Typeforall u v : propA, ([|u andA v|]) =>> ([|u|]) *** ([|v|])A, B: Type
u, v: propA
a: A
hu: u a
hv: v asatisfyT (([|u|]) *** ([|v|])) (Tnil a)A, B: Type
u, v: propA
a: A
hu: u a
hv: v afollowsT (singletonT v) (Tnil a) (Tnil a)exact: nil_singletonT. Qed.A, B: Type
u, v: propA
a: A
hu: u a
hv: v asingletonT v (Tnil a)A, B: Typeforall (v : propA) (p : propT), (([|v|]) *** p) =>> pby move => v [p hp] tr0 /= [tr1 [[a [h0 h2]] h1]]; invs h1; invs h2. Qed.A, B: Typeforall (v : propA) (p : propT), (([|v|]) *** p) =>> pA, B: Typeforall p : propT, (([|ttA|]) *** p) =>> pA, B: Typeforall p : propT, (([|ttA|]) *** p) =>> pexact: SingletonT_AppendT. Qed.A, B: Type
p: propT(([|ttA|]) *** p) =>> pA, B: Typeforall p : propT, p =>> ([|ttA|]) *** pA, B: Typeforall p : propT, p =>> ([|ttA|]) *** pA, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0(singletonT ttA *+* p) tr0A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0singletonT ttA (Tnil (hd tr0))A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0followsT p (Tnil (hd tr0)) tr0A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0singletonT ttA (Tnil (hd tr0))A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0followsT p (Tnil (hd tr0)) tr0A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0followsT p (Tnil (hd tr0)) tr0exact: followsT_nil. Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0followsT p (Tnil (hd tr0)) tr0A, B: Typeforall p : trace -> Prop, setoidT p -> forall (u : propA) (tr : trace), (p *+* singletonT u) tr -> p trA, B: Typeforall p : trace -> Prop, setoidT p -> forall (u : propA) (tr : trace), (p *+* singletonT u) tr -> p trexact: (hp _ h1 _ (followsT_singletonT h2)). Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
tr0, tr1: trace
h1: p tr1
h2: followsT (singletonT u) tr1 tr0p tr0A, B: Typeforall (p : propT) (v : propA), (p *** ([|v|])) =>> pA, B: Typeforall (p : propT) (v : propA), (p *** ([|v|])) =>> pexact: appendT_singletonT. Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
tr0: trace(p *+* singletonT v) tr0 -> p tr0A, B: Typeforall p : propT, (p *** ([|ttA|])) =>> pA, B: Typeforall p : propT, (p *** ([|ttA|])) =>> pexact: AppendT_Singleton. Qed.A, B: Type
p: propT(p *** ([|ttA|])) =>> pA, B: Typeforall p : propT, p =>> p *** ([|ttA|])A, B: Typeforall p : propT, p =>> p *** ([|ttA|])A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0(p *+* singletonT ttA) tr0A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
htr0: p tr0followsT (singletonT ttA) tr0 tr0A, B: Type
p: trace -> Propforall tr0 : trace, followsT (singletonT ttA) tr0 tr0A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0forall tr0 : trace, followsT (singletonT ttA) tr0 tr0A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: AfollowsT (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: tracefollowsT (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: AfollowsT (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: tracefollowsT (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: AsingletonT ttA (Tnil a)A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: tracefollowsT (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: tracefollowsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)exact/followsT_delay/CIH. Qed.A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (singletonT ttA) tr0 tr0
a: A
b: B
tr0: tracefollowsT (singletonT ttA) (Tcons a b tr0) (Tcons a b tr0)A, B: Type(TtT *** TtT) =>> TtTby []. Qed.A, B: Type(TtT *** TtT) =>> TtTA, B: Type(FiniteT *** FiniteT) =>> FiniteTA, B: Type(FiniteT *** FiniteT) =>> FiniteTA, B: Type
tr0, tr1: trace
Hfin: finiteT tr1
Hfol: followsT (fun tr : trace => finiteT tr) tr1 tr0satisfyT FiniteT tr0exact/finiteT_delay/IH. Qed.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')A, B: TypeFiniteT =>> FiniteT *** FiniteTA, B: TypeFiniteT =>> FiniteT *** FiniteTA, B: Type
tr0: trace
h0: satisfyT FiniteT tr0satisfyT (FiniteT *** FiniteT) tr0A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0finiteT (Tnil (hd tr0))A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0followsT (fun tr : trace => finiteT tr) (Tnil (hd tr0)) tr0A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0finiteT (Tnil (hd tr0))A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0followsT (fun tr : trace => finiteT tr) (Tnil (hd tr0)) tr0A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0followsT (fun tr : trace => finiteT tr) (Tnil (hd tr0)) tr0exact: followsT_nil. Qed.A, B: Type
tr0: trace
h0: satisfyT FiniteT tr0followsT (fun tr : trace => finiteT tr) (Tnil (hd tr0)) tr0A, B: Typeforall u : propA, (FiniteT *** ([|u|])) =>> FiniteTA, B: Typeforall u : propA, (FiniteT *** ([|u|])) =>> FiniteTexact: (finiteT_setoidT h0 (followsT_singletonT h1)). Qed.A, B: Type
u: propA
tr, tr1: trace
h0: finiteT tr1
h1: followsT (singletonT u) tr1 trfiniteT trA, B: TypeInfiniteT =>> TtT *** ([|ffA|])A, B: TypeInfiniteT =>> 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 tr1followsT (singletonT ffA) (Tcons a b tr1) (Tcons a b tr1)A, B: Typeforall (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)exact/followsT_delay/CIH. Qed.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 trfollowsT (singletonT ffA) (Tcons a b (Tcons a0 b0 tr)) (Tcons a b (Tcons a0 b0 tr))A, B: Type(TtT *** ([|ffA|])) =>> InfiniteTA, B: Type(TtT *** ([|ffA|])) =>> InfiniteTA, B: Type
tr0, tr1: trace
h1: followsT (singletonT ffA) tr1 tr0infiniteT tr0A, B: Type
CIH: forall tr0 tr1 : trace, followsT (singletonT ffA) tr1 tr0 -> infiniteT tr0
tr0: trace
H0: singletonT ffA tr0infiniteT tr0A, 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 tr0infiniteT tr0A, 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.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')
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: Typeforall p : trace -> Prop, setoidT p -> setoidT (iterT p)A, B: Typeforall p : trace -> Prop, setoidT p -> setoidT (iterT p)A, B: Type
p: trace -> Prop
hp: setoidT psetoidT (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 tr1followsT (iterT p) tr tr1A, 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 tr0followsT (iterT p) (Tnil (hd tr0)) tr1A, 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 tr0iterT p tr1A, 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) tr1iterT p tr1A, 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 tr0iterT p tr1A, 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) tr1iterT p tr1A, 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 tr0iterT p tr1A, B: Type
p: trace -> Prop
hp: setoidT p
CIH: setoidT (iterT p)
h0: forall tr : trace, setoidT (followsT (iterT p) tr)
a: AiterT 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 tr0iterT p tr1A, 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 tr0iterT p tr1exact: iterT_loop H (h0 _ _ H0 _ h2). Qed.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 tr0iterT p tr1A, B: Typeforall p0 p1 : trace -> Prop, (forall tr : trace, p0 tr -> p1 tr) -> forall tr : trace, iterT p0 tr -> iterT p1 trA, B: Typeforall p0 p1 : trace -> Prop, (forall tr : trace, p0 tr -> p1 tr) -> forall tr : trace, iterT p0 tr -> iterT p1 trA, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 trforall tr : trace, iterT p0 tr -> iterT p1 trA, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 trforall tr : trace, iterT p0 tr -> iterT p1 trA, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
CIH: forall tr : trace, iterT p0 tr -> iterT p1 trforall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1A, 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 tr1forall tr : trace, iterT p0 tr -> iterT p1 trA, 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 tr1forall tr0 tr1 : trace, followsT (iterT p0) tr0 tr1 -> followsT (iterT p1) tr0 tr1A, 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 tr1forall tr : trace, iterT p0 tr -> iterT p1 trA, 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 tr1followsT (iterT p1) tr0 tr1A, 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 tr1forall tr : trace, iterT p0 tr -> iterT p1 trA, 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 tr1followsT (iterT p1) (Tnil (hd tr1)) tr1A, 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 tr1forall tr : trace, iterT p0 tr -> iterT p1 trA, 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 tr1forall tr : trace, iterT p0 tr -> iterT p1 trexact: iterT_loop (hp _ H) (h _ _ H0). Qed.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 tr0iterT p1 tr0A, B: Typeforall (u : propA) (p : trace -> Prop) (b : B) (tr : trace), u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr trA, B: Typeforall (u : propA) (p : trace -> Prop) (b : B) (tr : trace), u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr trA, B: Type
u: propA
p: trace -> Prop
b: Bforall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr trA, 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 trforall tr : trace, u (hd tr) -> iterT (p *+* dupT u b) tr -> followsT (singletonT u) tr trA, 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 trfollowsT (singletonT u) tr trA, 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 trfollowsT (singletonT u) tr trA, 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 trfollowsT (singletonT u) tr trA, 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 trfollowsT (singletonT u) tr trA, 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 trfollowsT (singletonT u) tr trA, 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 tr0followsT (singletonT u) tr trA, 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 trforall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr trA, 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 trforall tr tr1 tr0 : trace, followsT (dupT u b) tr1 tr0 -> followsT (iterT (p *+* dupT u b)) tr0 tr -> followsT (singletonT u) tr trA, 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 tr2followsT (singletonT u) tr0 tr0A, 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 tr0A, 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 tr2followsT (singletonT u) tr0 tr0A, 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 tr0A, 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 tr0A, 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 tr0A, 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 tr0A, 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 tr0A, 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 tr0exact: 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
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'0followsT (singletonT u) (Tcons a b0 tr'0) (Tcons a b0 tr'0)A, B: Typeforall p q : propT, p =>> q -> IterT p =>> IterT qA, B: Typeforall p q : propT, p =>> q -> IterT p =>> IterT qexact: (iterT_cont (fun tr => h0 tr)). Qed.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: traceiterT p tr0 -> iterT q tr0A, B: Typeforall (p : trace -> Prop) (tr : trace), iterT p tr -> singletonT ttA tr \/ (p *+* iterT p) trA, B: Typeforall (p : trace -> Prop) (tr : trace), iterT p tr -> singletonT ttA tr \/ (p *+* iterT p) trA, B: Type
p: trace -> Prop
a: AsingletonT 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 trsingletonT ttA tr \/ (p *+* iterT p) trA, B: Type
p: trace -> Prop
a: AsingletonT 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 trsingletonT ttA tr \/ (p *+* iterT p) trA, B: Type
p: trace -> Prop
tr, tr0: trace
H: p tr0
H0: followsT (iterT p) tr0 trsingletonT ttA tr \/ (p *+* iterT p) trby right; exists tr0. Qed.A, B: Type
p: trace -> Prop
tr, tr0: trace
H: p tr0
H0: followsT (iterT p) tr0 trsingletonT ttA tr \/ (p *+* iterT p) trA, B: Typeforall p : propT, IterT p =>> ([|ttA|]) orT p *** IterT pA, B: Typeforall p : propT, IterT p =>> ([|ttA|]) orT p *** IterT pexact: iterT_split_1 h0. Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
h0: iterT p tr0singletonT ttA tr0 \/ (p *+* iterT p) tr0A, B: Typeforall (tr : trace) (p : trace -> Prop), singletonT ttA tr \/ (p *+* iterT p) tr -> iterT p trA, B: Typeforall (tr : trace) (p : trace -> Prop), singletonT ttA tr \/ (p *+* iterT p) tr -> iterT p trA, B: Type
tr: trace
p: trace -> Prop
a: A
h0: ttA a
h1: bisim tr (Tnil a)iterT p trA, B: Type
tr: trace
p: trace -> Prop
tr0: trace
h0: p tr0
h1: followsT (iterT p) tr0 triterT p trA, B: Type
tr: trace
p: trace -> Prop
a: A
h0: ttA a
h1: bisim tr (Tnil a)iterT p trA, B: Type
tr: trace
p: trace -> Prop
tr0: trace
h0: p tr0
h1: followsT (iterT p) tr0 triterT p trA, B: Type
p: trace -> Prop
a: A
h0: ttA aiterT p (Tnil a)A, B: Type
tr: trace
p: trace -> Prop
tr0: trace
h0: p tr0
h1: followsT (iterT p) tr0 triterT p trA, B: Type
tr: trace
p: trace -> Prop
tr0: trace
h0: p tr0
h1: followsT (iterT p) tr0 triterT p trexact: iterT_loop h0 h1. Qed.A, B: Type
tr: trace
p: trace -> Prop
tr0: trace
h0: p tr0
h1: followsT (iterT p) tr0 triterT p trA, B: Typeforall p : propT, (([|ttA|]) orT p *** IterT p) =>> IterT pA, B: Typeforall p : propT, (([|ttA|]) orT p *** IterT p) =>> IterT pexact: iterT_split_2. Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: tracesingletonT ttA tr0 \/ (p *+* iterT p) tr0 -> iterT p tr0A, B: Typeforall (p : trace -> Prop) (tr : trace), (iterT p *+* p) tr -> iterT p trA, B: Typeforall (p : trace -> Prop) (tr : trace), (iterT p *+* p) tr -> iterT p trA, B: Type
p: trace -> Prop
tr, tr0: trace
h0: iterT p tr0
h1: followsT p tr0 triterT p trA, B: Type
p: trace -> Propforall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p trA, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p trforall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p trA, 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) tr1iterT p tr1A, 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 tr0iterT p tr1A, 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) tr1iterT p tr1A, 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 tr0iterT p tr1A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr1: trace
H1: p tr1iterT p tr1A, 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 tr0iterT p tr1A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p tr
tr1: trace
H1: p tr1followsT (iterT p) tr1 tr1A, 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 tr0iterT p tr1A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p trforall tr1 : trace, followsT (iterT p) tr1 tr1A, 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 tr0iterT p tr1A, 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 tr1forall tr1 : trace, followsT (iterT p) tr1 tr1A, 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 tr0iterT p tr1A, 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: tracefollowsT (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 tr0iterT p tr1A, 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 tr0iterT p tr1A, 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 tr0iterT p tr1A, 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 tr0followsT (iterT p) tr tr1A, B: Type
p: trace -> Prop
CIH: forall tr0 tr : trace, iterT p tr0 -> followsT p tr0 tr -> iterT p trforall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1A, 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 tr1forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT p tr0 tr1 -> followsT (iterT p) tr tr1A, 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 tr1followsT (iterT p) (Tnil (hd tr1)) tr2A, 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) tr2A, 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 tr1followsT (iterT p) (Tnil (hd tr1)) tr2A, 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) tr2A, 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 tr1followsT (iterT p) (Tnil (hd tr2)) tr2A, 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) tr2A, 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) tr2A, 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) tr2exact: followsT_delay _ _ (CIH0 _ _ _ H H4). Qed.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'0followsT (iterT p) (Tcons a b tr) (Tcons a b tr'0)A, B: Typeforall p : propT, (IterT p *** p) =>> IterT pA, B: Typeforall p : propT, (IterT p *** p) =>> IterT pexact: iterT_unfold_1 h0. Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
tr: trace
h0: (iterT p *+* p) triterT p trA, B: Typeforall p : propT, (([|ttA|]) orT IterT p *** p) =>> IterT pA, B: Typeforall p : propT, (([|ttA|]) orT IterT p *** p) =>> IterT pA, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
a: A
h0: bisim tr0 (Tnil a)iterT p tr0A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
H: (iterT p *+* p) tr0iterT p tr0A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
a: A
h0: bisim tr0 (Tnil a)iterT p tr0A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
H: (iterT p *+* p) tr0iterT p tr0A, B: Type
p: trace -> Prop
hp: setoidT p
a: AiterT p (Tnil a)A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
H: (iterT p *+* p) tr0iterT p tr0A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
H: (iterT p *+* p) tr0iterT p tr0exact: iterT_unfold_1 H. Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: trace
H: (iterT p *+* p) tr0iterT p tr0A, B: Typeforall p : propT, ([|ttA|]) =>> IterT pA, B: Typeforall p : propT, ([|ttA|]) =>> IterT pexact: iterT_stop. Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
x: AiterT p (Tnil x)A, B: Typeforall p : propT, (p *** IterT p) =>> IterT pA, B: Typeforall p : propT, (p *** IterT p) =>> IterT pexact: (iterT_loop h0). Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
tr0, tr1: trace
h0: p tr1
h1: followsT (iterT p) tr1 tr0iterT p tr0A, B: Typeforall (p : trace -> Prop) (tr : trace), iterT p tr -> (iterT p *+* iterT p) trA, B: Typeforall (p : trace -> Prop) (tr : trace), iterT p tr -> (iterT p *+* iterT p) trA, B: Type
p: trace -> Prop
tr0: trace
h0: iterT p tr0(iterT p *+* iterT p) tr0A, B: Type
p: trace -> Prop
tr0: trace
h0: iterT p tr0followsT (iterT p) tr0 tr0A, B: Type
p: trace -> Propforall tr0 : trace, followsT (iterT p) tr0 tr0A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0forall tr0 : trace, followsT (iterT p) tr0 tr0A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: AfollowsT (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: tracefollowsT (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: AfollowsT (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: tracefollowsT (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: AiterT p (Tnil a)A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: A
b: B
tr0: tracefollowsT (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: tracefollowsT (iterT p) (Tcons a b tr0) (Tcons a b tr0)exact/followsT_delay/CIH. Qed.A, B: Type
p: trace -> Prop
CIH: forall tr0 : trace, followsT (iterT p) tr0 tr0
a: A
b: B
tr0: tracefollowsT (iterT p) (Tcons a b tr0) (Tcons a b tr0)A, B: Typeforall p : propT, IterT p =>> IterT p *** IterT pA, B: Typeforall p : propT, IterT p =>> IterT p *** IterT pexact: iterT_iterT_2. Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
tr0: traceiterT p tr0 -> (iterT p *+* iterT p) tr0A, B: Typeforall (p : trace -> Prop) (tr : trace), (iterT p *+* iterT p) tr -> iterT p trA, B: Typeforall (p : trace -> Prop) (tr : trace), (iterT p *+* iterT p) tr -> iterT p trA, B: Type
p: trace -> Prop
tr0, tr1: trace
h0: iterT p tr1
h1: followsT (iterT p) tr1 tr0iterT p tr0A, B: Type
p: trace -> Propforall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0A, 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) tr1iterT p tr1A, 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 tr1iterT p tr1A, 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) tr1iterT p tr1A, 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 tr1iterT p tr1A, 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 tr1iterT p tr1A, 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 tr1iterT p tr1A, 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 tr1followsT (iterT p) tr tr1A, B: Type
p: trace -> Prop
CIH: forall tr1 tr0 : trace, iterT p tr1 -> followsT (iterT p) tr1 tr0 -> iterT p tr0forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1A, 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 tr1forall tr tr0 tr1 : trace, followsT (iterT p) tr tr0 -> followsT (iterT p) tr0 tr1 -> followsT (iterT p) tr tr1A, 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 tr2followsT (iterT p) (Tnil (hd tr1)) tr2A, 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') tr2followsT (iterT p) (Tcons a b tr) tr2A, 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 tr2followsT (iterT p) (Tnil (hd tr1)) tr2A, 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') tr2followsT (iterT p) (Tcons a b tr) tr2A, 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 tr2followsT (iterT p) (Tnil (hd tr2)) tr2A, 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') tr2followsT (iterT p) (Tcons a b tr) tr2A, 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') tr2followsT (iterT p) (Tcons a b tr) tr2A, 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') tr2followsT (iterT p) (Tcons a b tr) tr2exact: followsT_delay _ _ (CIH2 _ _ _ H H4). Qed.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'0followsT (iterT p) (Tcons a b tr) (Tcons a b tr'0)A, B: Typeforall p : propT, (IterT p *** IterT p) =>> IterT pA, B: Typeforall p : propT, (IterT p *** IterT p) =>> IterT pexact: iterT_iterT. Qed.A, B: Type
p: trace -> Prop
hp: setoidT p
tr: trace(iterT p *+* iterT p) tr -> iterT p trA, B: Typeforall (v : propA) (b : B), (([|v|]) *** IterT (TtT *** (<< v; b >>))) =>> TtT *** ([|v|])A, B: Typeforall (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) tr0A, B: Type
v: propA
b: B
tr0: trace
h0: v (hd tr0)
H1: iterT (ttT *+* dupT v b) tr0ttT tr0 /\ followsT (singletonT v) tr0 tr0A, B: Type
v: propA
b: B
tr0: trace
h0: v (hd tr0)
H1: iterT (ttT *+* dupT v b) tr0followsT (singletonT v) tr0 tr0A, B: Type
v: propA
b: Bforall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0A, 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 tr0followsT (singletonT v) tr0 tr0A, 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 tr0followsT (singletonT v) tr0 tr0A, 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 tr0followsT (singletonT v) tr0 tr0A, 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 tr0followsT (singletonT v) tr0 tr0A, 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 tr0followsT (singletonT v) tr0 tr0A, 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 trfollowsT (singletonT v) tr0 tr0A, B: Type
v: propA
b: B
CIH: forall tr0 : trace, v (hd tr0) -> iterT (ttT *+* dupT v b) tr0 -> followsT (singletonT v) tr0 tr0forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0A, 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 tr0forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0A, 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 tr1followsT (singletonT v) tr2 tr2A, 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 tr2A, 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 tr1followsT (singletonT v) tr2 tr2A, 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 tr2A, 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 tr2A, 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 tr2A, 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 tr2A, 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 tr2A, 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 tr2exact: followsT_delay _ _ (CIH0 _ _ _ H H4). Qed.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'0followsT (singletonT v) (Tcons a b0 tr'0) (Tcons a b0 tr'0)
Definition lastA (p : trace -> Prop) : propA := fun a => exists tr, p tr /\ finalTA tr a.A, B: Typeforall p q : trace -> Prop, (forall tr : trace, p tr -> q tr) -> lastA p ->> lastA qA, B: Typeforall p q : trace -> Prop, (forall tr : trace, p tr -> q tr) -> lastA p ->> lastA qA, B: Type
p0, p1: trace -> Prop
hp: forall tr : trace, p0 tr -> p1 tr
a: A
tr: trace
h0: p0 tr
h1: finalTA tr alastA p1 aexact: h1. Qed. Definition LastA (p : propT) : propA := let: exist f0 h0 := p in lastA f0.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 afinalTA tr aA, B: Typeforall p q : propT, p =>> q -> LastA p ->> LastA qA, B: Typeforall p q : propT, p =>> q -> LastA p ->> LastA qexact/lastA_cont/h0. Qed.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 hglastA f ->> lastA gA, B: Typeforall u : propA, LastA ([|u|]) ->> uby move => u a [tr0 [[st1 [h1 h3]] h2]]; invs h3; invs h2. Qed.A, B: Typeforall u : propA, LastA ([|u|]) ->> uA, B: Typeforall u : propA, u ->> LastA ([|u|])A, B: Typeforall u : propA, u ->> LastA ([|u|])A, B: Type
u: propA
a: A
h0: u aLastA ([|u|]) aA, B: Type
u: propA
a: A
h0: u asingletonT u (Tnil a)A, B: Type
u: propA
a: A
h0: u afinalTA (Tnil a) aA, B: Type
u: propA
a: A
h0: u asingletonT u (Tnil a)A, B: Type
u: propA
a: A
h0: u afinalTA (Tnil a) aA, B: Type
u: propA
a: A
h0: u afinalTA (Tnil a) aexact: finalTA_nil. Qed.A, B: Type
u: propA
a: A
h0: u afinalTA (Tnil a) aA, B: Typeforall (p q : trace -> Prop) (a : A), lastA (p *+* q) a -> lastA q aA, B: Typeforall (p q : trace -> Prop) (a : A), lastA (p *+* q) a -> lastA q aA, B: Type
p, q: trace -> Prop
a: A
tr0, tr: trace
h2: followsT q tr tr0
h1: finalTA tr0 alastA q aA, B: Type
p, q: trace -> Prop
a: A
H0: q (Tnil a)lastA q aA, 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 tr0lastA q a'A, B: Type
p, q: trace -> Prop
a: A
H0: q (Tnil a)lastA q aA, 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 tr0lastA q a'A, B: Type
p, q: trace -> Prop
a: A
H0: q (Tnil a)q (Tnil a) /\ finalTA (Tnil a) aA, 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 tr0lastA 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 tr0lastA 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 tr0lastA 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 tr0lastA 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 tr0lastA q a'exact: IH _ H1. Qed.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 tr0lastA q a'A, B: Typeforall (p : propT) (v : propA), LastA (p *** ([|v|])) ->> vA, B: Typeforall (p : propT) (v : propA), LastA (p *** ([|v|])) ->> vA, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
tr, tr': trace
h0: followsT (singletonT v) tr' tr
h1: finalTA tr av aA, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
H0: singletonT v (Tnil a)v aA, 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 trv a'A, B: Type
p: trace -> Prop
hp: setoidT p
v: propA
a: A
H0: singletonT v (Tnil a)v aA, 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 trv 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 trv 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 trv 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 trv a'exact: IH _ H1. Qed.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 trv a'A, B: Typeforall (p : propT) (u : propA), (LastA p andA u) ->> LastA (p *** ([|u|]))A, B: Typeforall (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 aLastA (exist (fun p : trace -> Prop => setoidT p) p hp *** ([|u|])) aA, 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 aA, 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) tr0A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
a: A
tr0: trace
h2: p tr0
h3: finalTA tr0 a
h1: u ap tr0 /\ followsT (singletonT u) tr0 tr0A, B: Type
p: trace -> Prop
hp: setoidT p
u: propA
a: A
tr0: trace
h2: p tr0
h3: finalTA tr0 a
h1: u afollowsT (singletonT u) tr0 tr0A, B: Type
p: trace -> Prop
hp: setoidT p
u: propAforall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0A, 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 tr0forall (tr0 : trace) (a : A), finalTA tr0 a -> u a -> followsT (singletonT u) tr0 tr0A, 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 afollowsT (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 afollowsT (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 afollowsT (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 afollowsT (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 afollowsT (singletonT u) (Tcons a0 b tr) (Tcons a0 b tr)exact: followsT_delay _ _ (CIH _ _ H h0). Qed.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 afollowsT (singletonT u) (Tcons a0 b tr) (Tcons a0 b tr)A, B: Typeforall (v : propA) (b : B) (p : propT), LastA (([|v|]) *** IterT (p *** (<< v; b >>))) ->> vA, B: Typeforall (v : propA) (b : B) (p : propT), LastA (([|v|]) *** IterT (p *** (<< v; b >>))) ->> vA, B: Type
v: propA
b: B
p: propT
a: A
h0: LastA (([|v|]) *** IterT (p *** (<< v; b >>))) av aA, B: Type
v: propA
b: B
p: propT
a: A
h0: LastA (([|v|]) *** IterT (p *** (<< v; b >>))) a
h1: p =>> TtTv aA, 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 >>))) av aexact: LastA_AppendA. Qed.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 >>))) aLastA (TtT *** ([|v|])) a -> v aA, B: Typeforall (v : propA) (b : B), ((<< v; b >>) *** IterT (TtT *** (<< v; b >>))) =>> TtT *** ([|v|])A, B: Typeforall (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 tr0satisfyT (TtT *** ([|v|])) tr0A, 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: Bforall 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 tr0followsT (singletonT v) tr0 tr0A, 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 tr0followsT (singletonT v) tr0 tr0A, 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 tr0followsT (singletonT v) tr0 tr0A, 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 tr0followsT (singletonT v) tr0 tr0A, 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 trfollowsT (singletonT v) tr0 tr0A, 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 tr0A, 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 tr0forall tr1 tr tr0 : trace, followsT (dupT v b) tr1 tr -> followsT (iterT (ttT *+* dupT v b)) tr tr0 -> followsT (singletonT v) tr0 tr0A, 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 tr1followsT (singletonT v) tr2 tr2A, 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 tr2A, 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 tr1followsT (singletonT v) tr2 tr2A, 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 tr2A, 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 tr2A, 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 tr2A, 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 tr2A, 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 tr2A, 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 tr2exact: followsT_delay _ _ (CIH0 _ _ _ H H4). Qed.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'0followsT (singletonT v) (Tcons a b0 tr'0) (Tcons a b0 tr'0)A, B: Typeforall p q : propT, LastA (([|LastA p|]) *** q) ->> LastA (p *** q)A, B: Typeforall 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 tr1lastA (p *+* q) aA, 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) aA, 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) aA, 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) aA, 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) aA, 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) aA, 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) aA, B: Type
p: trace -> Prop
hp: setoidT p
q: trace -> Prop
hq: setoidT q
a: A
tr1: trace
H1: q tr1forall 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) aA, 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) aA, 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) aA, 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) aA, 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) tr1A, 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) aA, 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 = a0A, 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) aA, 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) aA, 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) aA, 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) aA, 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) aA, 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) aA, 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) aA, 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 a0finalTA (tr2 +++ tr1) aA, 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 afinalTA (Tnil a0 +++ tr0) aA, 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 afinalTA (Tcons a0 b tr2 +++ tr0) aA, 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 afinalTA (Tnil a0 +++ tr0) aA, 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 afinalTA (Tcons a0 b tr2 +++ tr0) aA, 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 afinalTA (Tcons a0 b tr2 +++ tr0) aA, 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 afinalTA (Tcons a0 b tr2 +++ tr0) aA, 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 afinalTA (Tcons a0 b (tr2 +++ tr0)) aexact: IH _ h0 h1. Qed.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 afinalTA (tr2 +++ tr0) aA, B: Typeforall u v : propA, (v andA u) ->> LastA (([|v|]) *** ([|u|]))A, B: Typeforall u v : propA, (v andA u) ->> LastA (([|v|]) *** ([|u|]))A, B: Type
u, v: propA
a: A
h0: v a
h1: u aLastA (([|v|]) *** ([|u|])) aA, B: Type
u, v: propA
a: A
h0: v a
h1: u a(singletonT v *+* singletonT u) (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
u, v: propA
a: A
h0: v a
h1: u afollowsT (singletonT u) (Tnil a) (Tnil a)A, B: Typeforall (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: Typeforall (tr : trace) (b : B), hd tr = hd (lastdup tr b)A, B: Typeforall (u : propA) (tr : trace) (b : B), followsT (singletonT u) tr tr -> followsT (dupT u b) tr (lastdup tr b)A, B: Typeforall (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 trfollowsT (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 trfollowsT (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 trfollowsT (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 a0followsT (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 trfollowsT (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 a0dupT 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 trfollowsT (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 trfollowsT (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 trfollowsT (dupT u b) (Tcons a b0 tr) (lastdup (Tcons a b0 tr) b)exact/followsT_delay/CIH. Qed.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 trfollowsT (dupT u b) (Tcons a b0 tr) (Tcons a b0 (lastdup tr b))A, B: Typeforall (tr : trace) (a : A) (b : B), finalTA tr a -> finalTA (lastdup tr b) aA, B: Typeforall (tr : trace) (a : A) (b : B), finalTA tr a -> finalTA (lastdup tr b) aA, B: Type
b1: B
a: AfinalTA (lastdup (Tnil a) b1) aA, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2finalTA (lastdup (Tcons a1 b2 tr) b1) a2A, B: Type
b1: B
a: AfinalTA (lastdup (Tnil a) b1) aA, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2finalTA (lastdup (Tcons a1 b2 tr) b1) a2A, B: Type
b1: B
a: AfinalTA (Tcons a b1 (Tnil a)) aA, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2finalTA (lastdup (Tcons a1 b2 tr) b1) a2A, B: Type
b1: B
a: AfinalTA (Tnil a) aA, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2finalTA (lastdup (Tcons a1 b2 tr) b1) a2A, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2finalTA (lastdup (Tcons a1 b2 tr) b1) a2A, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2finalTA (lastdup (Tcons a1 b2 tr) b1) a2exact: finalTA_delay. Qed.A, B: Type
b1: B
a1: A
b2: B
a2: A
tr: trace
Hfinal: finalTA tr a2
IH: finalTA (lastdup tr b1) a2finalTA (Tcons a1 b2 (lastdup tr b1)) a2A, B: Typeforall (p : propT) (u : propA) (b : B), LastA (p *** ([|u|])) ->> LastA (p *** (<< u; b >>))A, B: Typeforall (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 aLastA (exist (fun p : trace -> Prop => setoidT p) p hp *** (<< u; b >>)) aA, 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 tr0p tr0A, 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 tr0followsT (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 tr0p tr0A, 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 tr0followsT (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 tr0followsT (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 tr0followsT (dupT u b) tr0 (lastdup tr0 b)exact: followsT_dupT b h4. Qed.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 tr0followsT (dupT u b) tr0 (lastdup tr0 b)
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: Typeforall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p0 tr0 tr'A, B: Typeforall (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) tr1forall 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'0A, 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) tr1forall 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'0A, 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'0A, 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) tr1followsT 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'0A, 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) tr1hd tr' = hd tr1A, 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'0A, 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'0A, 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'0A, 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)exact: followsT_delay _ _ (CIH _ _ _ _ h1 _ _). Qed.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 tr0followsT p0 (Tcons a0 b0 tr2) (Tcons a0 b0 tr0)A, B: Typeforall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1A, B: Typeforall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1A, 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' tr1forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1) (tr' : trace), midpointT h tr' -> followsT p1 tr' tr1A, 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) tr0followsT p1 tr0 tr1A, 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) tr0followsT 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) tr0followsT p1 tr0 tr1A, 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) tr0followsT 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) tr0followsT 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) tr0followsT p1 tr0 (Tcons a b tr')exact: followsT_delay _ _ (CIH _ _ _ _ h1 _ _). Qed. End sec_trace_properties.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'0followsT p1 (Tcons a0 b0 tr'0) (Tcons a0 b0 tr3)
Infix "=>>" := propT_imp (at level 60, right associativity). Infix "->>" := propA_imp (at level 60, right associativity).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).