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

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;

end;

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;A2: A = ('not' ('X' B)) => ('X' ('not' B)) ;

thus (SAT M) . [n,A] = 1 by A2, Th15; :: thesis: verum

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;A3: A = ('X' ('not' B)) => ('not' ('X' B)) ;

thus (SAT M) . [n,A] = 1 by A3, Th16; :: thesis: verum

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;A4: A = ('X' (B => C)) => (('X' B) => ('X' C)) ;

thus (SAT M) . [n,A] = 1 by A4, Th17; :: thesis: verum

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;A5: A = ('G' B) => (B '&&' ('X' ('G' B))) ;

thus (SAT M) . [n,A] = 1 by A5, Th18; :: thesis: verum

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;A6: A = (B 'U' C) => (('X' C) 'or' ('X' (B '&&' (B 'U' C)))) ;

thus (SAT M) . [n,A] = 1 by A6, Th19; :: thesis: verum