let H1, H2 be CTL-formula; for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
let S be non empty set ; for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
let R be total Relation of S,S; for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
let s be Element of S; for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
let BASSIGN be non empty Subset of (ModelSP S); for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
let kai be Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)); ( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
A1:
( ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) ) & pai . m |= Evaluate (H2,kai) ) ) implies ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
proof
given pai being
inf_path of
R such that A2:
pai . 0 = s
and A3:
ex
m being
Element of
NAT st
( ( for
j being
Element of
NAT st
j < m holds
pai . j |= Evaluate (
H1,
kai) ) &
pai . m |= Evaluate (
H2,
kai) )
;
ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) )
take
pai
;
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) )
consider m being
Element of
NAT such that A4:
for
j being
Element of
NAT st
j < m holds
pai . j |= Evaluate (
H1,
kai)
and A5:
pai . m |= Evaluate (
H2,
kai)
by A3;
A6:
for
j being
Element of
NAT st
j < m holds
pai . j,
kai |= H1
by A4;
(
pai . m |= Evaluate (
H2,
kai) iff
pai . m,
kai |= H2 )
;
hence
(
pai . 0 = s & ex
m being
Element of
NAT st
( ( for
j being
Element of
NAT st
j < m holds
pai . j,
kai |= H1 ) &
pai . m,
kai |= H2 ) )
by A2, A5, A6;
verum
end;
A7:
( ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) implies ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) ) & pai . m |= Evaluate (H2,kai) ) ) )
proof
given pai being
inf_path of
R such that A8:
pai . 0 = s
and A9:
ex
m being
Element of
NAT st
( ( for
j being
Element of
NAT st
j < m holds
pai . j,
kai |= H1 ) &
pai . m,
kai |= H2 )
;
ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) ) & pai . m |= Evaluate (H2,kai) ) )
take
pai
;
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= Evaluate (H1,kai) ) & pai . m |= Evaluate (H2,kai) ) )
consider m being
Element of
NAT such that A10:
for
j being
Element of
NAT st
j < m holds
pai . j,
kai |= H1
and A11:
pai . m,
kai |= H2
by A9;
A12:
for
j being
Element of
NAT st
j < m holds
pai . j |= Evaluate (
H1,
kai)
by A10, Def60;
thus
(
pai . 0 = s & ex
m being
Element of
NAT st
( ( for
j being
Element of
NAT st
j < m holds
pai . j |= Evaluate (
H1,
kai) ) &
pai . m |= Evaluate (
H2,
kai) ) )
by A8, A11, A12;
verum
end;
( s,kai |= H1 EU H2 iff s |= (Evaluate (H1,kai)) EU (Evaluate (H2,kai)) )
by Th9;
hence
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )
by A1, A7, Th16; verum