[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
enrich
IOtrace,
set-union
with
predicates
≤F : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
fwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('as × 'cs → Bool);
≤sF : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
simplefwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('as × 'cs → Bool) × ('ca → Option('aa));
≤nF : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
nfwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('as × 'cs → Bool) × ('cs × 'ca × 'cs × 'as → Nat);
≤BI : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
bwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool) × ('cs → Bool) × ('as → Bool);
≤B : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
bwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool);
≤wB : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
weakbwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool) × ('as → Bool);
≤bF : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
bfwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('as × 'cs → Bool);
≤iBI : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
imfinbwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool) × ('cs → Bool) × ('as → Bool);
variables
r : 'as × 'cs → Bool;
t : 'cs × 'as → Bool;
rbc : 'bs × 'cs → Bool;
rab : 'as × 'bs → Bool;
cal : List('ca);
bal : List('ba);
aal : List('aa);
el : List('e);
csf : Nat → 'cs;
bsf : Nat → 'bs;
asf : Nat → 'as;
csl : List('cs);
bsl : List('bs);
asl : List('as);
as : 'as;
as' : 'as;
bs : 'bs;
cs : 'cs;
cs' : 'cs;
ca : 'ca;
ba : 'ba;
aa : 'aa;
cα : Stream('aa);
bα : Stream('ba);
aα : Stream('aa);
β : Stream('e);
cσ : Stream('cs);
bσ : Stream('bs);
aσ : Stream('as);
cstart : 'cs → Bool;
bstart : 'bs → Bool;
astart : 'as → Bool;
cstep : 'cs × 'ca × 'cs → Bool;
bstep : 'bs × 'ba × 'bs → Bool;
astep : 'as × 'aa × 'as → Bool;
cext : 'ca → Option('e);
bext : 'ba → Option('e);
aext : 'aa → Option('e);
cioaut : IOAutomaton('cs, 'ca, 'e);
bioaut : IOAutomaton('bs, 'ba, 'e);
aioaut : IOAutomaton('as, 'aa, 'e);
size01f : 'cs × 'ca × 'cs × 'as → Nat;
aabs : 'ca → Option('aa);
aINV : 'as → Bool;
cINV : 'cs → Bool;
ass : Set('as);
axioms
forwardsim-def: ≤F(cioaut, aioaut) ↔ (∃ r. fwsim(cioaut, aioaut, r));
proofobls-forwardsim:
fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r)
↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)))
∧ (∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (∃ as0. move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ r(as0, cs0)));
simpleforwardsim-def: ≤sF(cioaut, aioaut) ↔ (∃ r, aabs. simplefwsim(cioaut, aioaut, r, aabs));
proofobls-simpleforwardsim:
simplefwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, aabs)
↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)))
∧ (∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (aabs(ca) = None ⊃ r(as, cs0);∃ as0. astep(as, aabs(ca).get, as0) ∧ r(as0, cs0)))
∧ (∀ ca. (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get)));
normedforwardsim-def: ≤nF(cioaut, aioaut) ↔ (∃ r, size01f. nfwsim(cioaut, aioaut, r, size01f));
proofobls-normedforwardsim:
nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f)
↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)))
∧ (∀ cs, ca, cs', as.
r(as, cs) ∧ cstep(cs, ca, cs')
→ r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs'))
∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as)));
branchingforwardsim-def: ≤bF(cioaut, aioaut) ↔ (∃ r. bfwsim(cioaut, aioaut, r));
proofobls-branchingforwardsim:
bfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r)
↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as)))
∧ (∀ cs, ca, cs0, as.
r(as, cs) ∧ cstep(cs, ca, cs0)
→ (cext(ca) = None
⊃ r(as, cs0)
;∃ asl, aal, aa, as1.
frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → r(as, cs))
∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ r(as1, cs0)
));
imfinbackwardsim-def: ≤iBI(cioaut, aioaut) ↔ (∃ t, aINV, cINV. imfinbwsim(cioaut, aioaut, t, cINV, aINV));
proofobls-imfinbackwardsim:
imfinbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, cINV, aINV)
↔ bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, cINV, aINV)
∧ (∀ cs. cINV(cs) → (∃ ass. ∀ as. t(cs, as) ∧ aINV(as) ↔ as ∈ ass));
backwardsim-def: ≤B(cioaut, aioaut) ↔ (∃ t. bwsim(cioaut, aioaut, t));
proofobls-backwardsim:
bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t)
↔ (∀ cs. ∃ as. t(cs, as)) ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) → astart(as))
∧ (∀ cs, ca, cs0, as0. cstep(cs, ca, cs0) ∧ t(cs0, as0) → (∃ as. move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as)));
backwardsiminv-def: ≤BI(cioaut, aioaut) ↔ (∃ t, aINV, cINV. bwsim(cioaut, aioaut, t, cINV, aINV));
proofobls-backwardsiminv:
bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, cINV, aINV)
↔ (∀ cs. cstart(cs) → cINV(cs)) ∧ (∀ as. astart(as) → aINV(as)) ∧ (∀ cs, ca, cs0. cINV(cs) ∧ cstep(cs, ca, cs0) → cINV(cs0))
∧ (∀ as, aa, as0. aINV(as) ∧ astep(as, aa, as0) → aINV(as0)) ∧ (∀ cs. cINV(cs) → (∃ as. t(cs, as) ∧ aINV(as)))
∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as))
∧ (∀ cs, ca, cs0, as0.
cINV(cs) ∧ cstep(cs, ca, cs0) ∧ t(cs0, as0) ∧ aINV(as0)
→ (∃ as. aINV(as) ∧ move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as)));
weakbackwardsim-def: ≤wB(cioaut, aioaut) ↔ (∃ t, aINV. weakbwsim(cioaut, aioaut, t, aINV));
proofobls-weakbackwardsim:
weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV)
↔ (∀ csl, cal. exec*(IOAut(cstart, cstep, cext))(csl, cal) → (∃ as. t(csl.last, as) ∧ aINV(as)))
∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as)) ∧ (∀ asl, aal. exec*(IOAut(astart, astep, aext))(asl, aal) → aINV(asl.last))
∧ (∀ csl, cal, ca, cs0, as0.
exec*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstep(csl.last, ca, cs0) ∧ t(cs0, as0) ∧ aINV(as0)
→ (∃ as. aINV(as) ∧ move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(csl.last, as)));
end enrich