let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) holds
F |= A
let F be Subset of LTLB_WFF; :: thesis: ( ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) implies F |= A )
assume A1: ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) ; :: thesis: F |= A
let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( M |= F implies M |= A )
assume M |= F ; :: thesis: M |= A
let n be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [n,A] = 1
per cases ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) by A1;
suppose A is axltl1 ; :: thesis: (SAT M) . [n,A] = 1
then consider B being Element of LTLB_WFF such that
A2: A = ('not' ('X' B)) => ('X' ('not' B)) ;
thus (SAT M) . [n,A] = 1 by A2, Th15; :: thesis: verum
end;
suppose A is axltl1a ; :: thesis: (SAT M) . [n,A] = 1
then consider B being Element of LTLB_WFF such that
A3: A = ('X' ('not' B)) => ('not' ('X' B)) ;
thus (SAT M) . [n,A] = 1 by A3, Th16; :: thesis: verum
end;
suppose A is axltl2 ; :: thesis: (SAT M) . [n,A] = 1
then consider B, C being Element of LTLB_WFF such that
A4: A = ('X' (B => C)) => (('X' B) => ('X' C)) ;
thus (SAT M) . [n,A] = 1 by A4, Th17; :: thesis: verum
end;
suppose A is axltl3 ; :: thesis: (SAT M) . [n,A] = 1
then consider B being Element of LTLB_WFF such that
A5: A = ('G' B) => (B '&&' ('X' ('G' B))) ;
thus (SAT M) . [n,A] = 1 by A5, Th18; :: thesis: verum
end;
suppose A is axltl4 ; :: thesis: (SAT M) . [n,A] = 1
then consider B, C being Element of LTLB_WFF such that
A6: A = (B 'U' C) => (('X' C) 'or' ('X' (B '&&' (B 'U' C)))) ;
thus (SAT M) . [n,A] = 1 by A6, Th19; :: thesis: verum
end;
suppose A is axltl5 ; :: thesis: (SAT M) . [n,A] = 1
then consider B, C being Element of LTLB_WFF such that
A7: A = (('X' C) 'or' ('X' (B '&&' (B 'U' C)))) => (B 'U' C) ;
thus (SAT M) . [n,A] = 1 by A7, Th20; :: thesis: verum
end;
suppose A is axltl6 ; :: thesis: (SAT M) . [n,A] = 1
then consider B, C being Element of LTLB_WFF such that
A8: A = (B 'U' C) => ('X' ('F' C)) ;
thus (SAT M) . [n,A] = 1 by A8, Th21; :: thesis: verum
end;
end;