let H, v be LTL-formula; :: thesis: for N being strict LTLnode of v
for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & H is Until holds
( w |= * N iff ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) )
let N be strict LTLnode of v; :: thesis: for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & H is Until holds
( w |= * N iff ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) )
let w be Element of Inf_seq AtomicFamily ; :: thesis: ( H in the LTLnew of N & H is Until implies ( w |= * N iff ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) ) )
assume that
A1: H in the LTLnew of N and
A2: H is Until ; :: thesis: ( w |= * N iff ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) )
set SN1 = SuccNode1 H,N;
set SN1O = the LTLold of (SuccNode1 H,N);
set SN1N = the LTLnew of (SuccNode1 H,N);
set SN1X = the LTLnext of (SuccNode1 H,N);
set XSN1X = 'X' (CastLTL the LTLnext of (SuccNode1 H,N));
set SN2 = SuccNode2 H,N;
set SN2O = the LTLold of (SuccNode2 H,N);
set SN2N = the LTLnew of (SuccNode2 H,N);
set SN2X = the LTLnext of (SuccNode2 H,N);
set XSN2X = 'X' (CastLTL the LTLnext of (SuccNode2 H,N));
set NO = the LTLold of N;
set NN = the LTLnew of N;
set NX = the LTLnext of N;
set XNX = 'X' (CastLTL the LTLnext of N);
A3: H in * N by LemSUM01, A1;
set H1 = the_left_argument_of H;
set H2 = the_right_argument_of H;
H = (the_left_argument_of H) 'U' (the_right_argument_of H) by A2, MODELC_2:8;
then ( w |= H iff w |= (the_right_argument_of H) 'or' ((the_left_argument_of H) '&' ('X' H)) ) by MODELC_2:75;
then A4: ( w |= H iff ( w |= the_right_argument_of H or w |= (the_left_argument_of H) '&' ('X' H) ) ) by MODELC_2:66;
A5: LTLNew1 H = {(the_left_argument_of H)} by A2, Def203;
A6: LTLNew2 H = {(the_right_argument_of H)} by A2, Def204;
A7: LTLNext H = {H} by A2, Def205;
A8: the LTLold of (SuccNode1 H,N) = the LTLold of N \/ {H} by A1, Def206;
A9: the LTLnew of (SuccNode1 H,N) = (the LTLnew of N \ {H}) \/ ({(the_left_argument_of H)} \ the LTLold of N) by A1, Def206, A5;
A10: the LTLnext of (SuccNode1 H,N) = the LTLnext of N \/ {H} by A1, Def206, A7;
A11: the LTLold of (SuccNode2 H,N) = the LTLold of N \/ {H} by A1, A2, Def207;
A12: the LTLnew of (SuccNode2 H,N) = (the LTLnew of N \ {H}) \/ ({(the_right_argument_of H)} \ the LTLold of N) by A1, A2, Def207, A6;
A13: the LTLnext of (SuccNode2 H,N) = the LTLnext of N by A1, A2, Def207;
Alem1: for F being LTL-formula holds
( not F in * (SuccNode1 H,N) or F in * N or F = the_left_argument_of H or F = 'X' H )

proof

let F be LTL-formula; :: thesis: ( not F in * (SuccNode1 H,N) or F in * N or F = the_left_argument_of H or F = 'X' H )
assume B1: F in * (SuccNode1 H,N) ; :: thesis: ( F in * N or F = the_left_argument_of H or F = 'X' H )

now

per cases ( F in the LTLold of (SuccNode1 H,N) or F in the LTLnew of (SuccNode1 H,N) or F in 'X' (CastLTL the LTLnext of (SuccNode1 H,N)) ) by B1, LemSUM01;

suppose F in the LTLold of (SuccNode1 H,N) ; :: thesis: ( F in * N or F = the_left_argument_of H or F = 'X' H )

then ( F in the LTLold of N or F in {H} ) by A8, XBOOLE_0:def 3;
hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) by LemSUM01, A3, TARSKI:def 1; :: thesis: verum

end;

suppose F in the LTLnew of (SuccNode1 H,N) ; :: thesis: ( F in * N or F = the_left_argument_of H or F = 'X' H )

then ( F in the LTLnew of N \ {H} or F in {(the_left_argument_of H)} \ the LTLold of N ) by A9, XBOOLE_0:def 3;
then ( F in the LTLnew of N or F in {(the_left_argument_of H)} ) by XBOOLE_0:def 5;
hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) by LemSUM01, TARSKI:def 1; :: thesis: verum

end;

suppose F in 'X' (CastLTL the LTLnext of (SuccNode1 H,N)) ; :: thesis: ( F in * N or F = the_left_argument_of H or F = 'X' H )

then consider G being LTL-formula such that
C1: F = G and
C2: ex G1 being LTL-formula st
( G1 in CastLTL the LTLnext of (SuccNode1 H,N) & G = 'X' G1 ) ;
consider G1 being LTL-formula such that
C3: G1 in the LTLnext of (SuccNode1 H,N) and
C4: G = 'X' G1 by C2;
C5: ( G1 in the LTLnext of N or G1 in {H} ) by C3, A10, XBOOLE_0:def 3;

now

per cases ( G1 in the LTLnext of N or G1 = H ) by C5, TARSKI:def 1;

suppose G1 in the LTLnext of N ; :: thesis: ( F in * N or F = the_left_argument_of H or F = 'X' H )

then F in 'X' (CastLTL the LTLnext of N) by C1, C4;
hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) by LemSUM01; :: thesis: verum

end;

suppose G1 = H ; :: thesis: ( F in * N or F = the_left_argument_of H or F = 'X' H )

hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) by C1, C4; :: thesis: verum

end;

end;

end;

hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) ; :: thesis: verum

end;

end;

end;

hence ( F in * N or F = the_left_argument_of H or F = 'X' H ) ; :: thesis: verum

end;

Alem2: for F being LTL-formula holds
( not F in * (SuccNode2 H,N) or F in * N or F = the_right_argument_of H )

proof

let F be LTL-formula; :: thesis: ( not F in * (SuccNode2 H,N) or F in * N or F = the_right_argument_of H )
assume B1: F in * (SuccNode2 H,N) ; :: thesis: ( F in * N or F = the_right_argument_of H )

now

per cases ( F in the LTLold of (SuccNode2 H,N) or F in the LTLnew of (SuccNode2 H,N) or F in 'X' (CastLTL the LTLnext of (SuccNode2 H,N)) ) by B1, LemSUM01;

suppose F in the LTLold of (SuccNode2 H,N) ; :: thesis: ( F in * N or F = the_right_argument_of H )

then ( F in the LTLold of N or F in {H} ) by A11, XBOOLE_0:def 3;
hence ( F in * N or F = the_right_argument_of H ) by LemSUM01, A3, TARSKI:def 1; :: thesis: verum

end;

suppose F in the LTLnew of (SuccNode2 H,N) ; :: thesis: ( F in * N or F = the_right_argument_of H )

then ( F in the LTLnew of N \ {H} or F in {(the_right_argument_of H)} \ the LTLold of N ) by A12, XBOOLE_0:def 3;
then ( F in the LTLnew of N or F in {(the_right_argument_of H)} ) by XBOOLE_0:def 5;
hence ( F in * N or F = the_right_argument_of H ) by LemSUM01, TARSKI:def 1; :: thesis: verum

end;

suppose F in 'X' (CastLTL the LTLnext of (SuccNode2 H,N)) ; :: thesis: ( F in * N or F = the_right_argument_of H )

then consider G being LTL-formula such that
C1: F = G and
C2: ex G1 being LTL-formula st
( G1 in CastLTL the LTLnext of (SuccNode2 H,N) & G = 'X' G1 ) ;
consider G1 being LTL-formula such that
C3: G1 in the LTLnext of (SuccNode2 H,N) and
C4: G = 'X' G1 by C2;
F in 'X' (CastLTL the LTLnext of N) by C1, C4, C3, A13;
hence ( F in * N or F = the_right_argument_of H ) by LemSUM01; :: thesis: verum

end;

end;

end;

hence ( F in * N or F = the_right_argument_of H ) ; :: thesis: verum

end;

Alem3: for F being LTL-formula st F in * N holds
( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) )

proof

let F be LTL-formula; :: thesis: ( F in * N implies ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) ) )
assume B1: F in * N ; :: thesis: ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) )

now

per cases ( F in the LTLold of N or F in the LTLnew of N or F in 'X' (CastLTL the LTLnext of N) ) by B1, LemSUM01;

suppose F in the LTLold of N ; :: thesis: ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) )

then ( F in the LTLold of (SuccNode1 H,N) & F in the LTLold of (SuccNode2 H,N) ) by A8, A11, XBOOLE_0:def 3;
hence ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) ) by LemSUM01; :: thesis: verum

end;

suppose C2: F in the LTLnew of N ; :: thesis: ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) )

now

per cases ( F = H or F <> H ) ;

suppose F = H ; :: thesis: ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) )

then F in {H} by TARSKI:def 1;
then ( F in the LTLold of (SuccNode1 H,N) & F in the LTLold of (SuccNode2 H,N) ) by A8, A11, XBOOLE_0:def 3;
hence ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) ) by LemSUM01; :: thesis: verum

end;

suppose F <> H ; :: thesis: ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) )

then not F in {H} by TARSKI:def 1;
then F in the LTLnew of N \ {H} by C2, XBOOLE_0:def 5;
then ( F in the LTLnew of (SuccNode1 H,N) & F in the LTLnew of (SuccNode2 H,N) ) by A9, A12, XBOOLE_0:def 3;
hence ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) ) by LemSUM01; :: thesis: verum

end;

end;

end;

hence ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) ) ; :: thesis: verum

end;

suppose F in 'X' (CastLTL the LTLnext of N) ; :: thesis: ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) )

then consider G being LTL-formula such that
C1: F = G and
C2: ex G1 being LTL-formula st
( G1 in CastLTL the LTLnext of N & G = 'X' G1 ) ;
consider G1 being LTL-formula such that
C3: G1 in the LTLnext of N and
C4: G = 'X' G1 by C2;
C5: G1 in the LTLnext of (SuccNode1 H,N) by C3, A10, XBOOLE_0:def 3;
( F in 'X' (CastLTL the LTLnext of (SuccNode1 H,N)) & F in 'X' (CastLTL the LTLnext of (SuccNode2 H,N)) ) by C1, C4, C3, C5, A13;
hence ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) ) by LemSUM01; :: thesis: verum

end;

end;

end;

hence ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) ) ; :: thesis: verum

end;

A17: ( not w |= * N or w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) )

proof

assume B1: w |= * N ; :: thesis: ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) )

now

per cases ( ( w |= the_left_argument_of H & w |= 'X' H ) or w |= the_right_argument_of H ) by A3, A4, B1, MODELC_2:65, MODELC_2:def 66;

suppose B3: ( w |= the_left_argument_of H & w |= 'X' H ) ; :: thesis: ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) )

for F being LTL-formula st F in * (SuccNode1 H,N) holds
w |= F

proof

let F be LTL-formula; :: thesis: ( F in * (SuccNode1 H,N) implies w |= F )
assume F in * (SuccNode1 H,N) ; :: thesis: w |= F
then ( F in * N or F = the_left_argument_of H or F = 'X' H ) by Alem1;
hence w |= F by B1, B3, MODELC_2:def 66; :: thesis: verum

end;

hence ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) by MODELC_2:def 66; :: thesis: verum

end;

suppose B4: w |= the_right_argument_of H ; :: thesis: ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) )

for F being LTL-formula st F in * (SuccNode2 H,N) holds
w |= F

proof

let F be LTL-formula; :: thesis: ( F in * (SuccNode2 H,N) implies w |= F )
assume F in * (SuccNode2 H,N) ; :: thesis: w |= F
then ( F in * N or F = the_right_argument_of H ) by Alem2;
hence w |= F by B1, B4, MODELC_2:def 66; :: thesis: verum

end;

hence ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) by MODELC_2:def 66; :: thesis: verum

end;

end;

end;

hence ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) ; :: thesis: verum

end;

( ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) implies w |= * N )

proof

assume B1: ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) ; :: thesis: w |= * N
for F being LTL-formula st F in * N holds
w |= F

proof

let F be LTL-formula; :: thesis: ( F in * N implies w |= F )
assume F in * N ; :: thesis: w |= F
then C1: ( F in * (SuccNode1 H,N) & F in * (SuccNode2 H,N) ) by Alem3;

now

per cases ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) by B1;

suppose w |= * (SuccNode1 H,N) ; :: thesis: w |= F

hence w |= F by C1, MODELC_2:def 66; :: thesis: verum

end;

suppose w |= * (SuccNode2 H,N) ; :: thesis: w |= F

hence w |= F by C1, MODELC_2:def 66; :: thesis: verum

end;

end;

end;

hence w |= F ; :: thesis: verum

end;

hence w |= * N by MODELC_2:def 66; :: thesis: verum

end;

hence ( w |= * N iff ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) ) by A17; :: thesis: verum