let A, B be Element of LTLB_WFF ; :: thesis: for n being Element of NAT

for M being LTLModel holds

( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )

let n be Element of NAT ; :: thesis: for M being LTLModel holds

( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )

let M be LTLModel; :: thesis: ( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )

A2: (SAT M) . [n,A] = 1 and

A3: (SAT M) . [n,B] = 1 ; :: thesis: (SAT M) . [n,(A '&&' B)] = 1

((SAT M) . [n,B]) => ((SAT M) . [n,TFALSUM]) = 0 by A3, Def11;

then ((SAT M) . [n,A]) => ((SAT M) . [n,(B => TFALSUM)]) = 0 by A2, Def11;

then (SAT M) . [n,(A => (B => TFALSUM))] = 0 by Def11;

then ((SAT M) . [n,(A => (B => TFALSUM))]) => ((SAT M) . [n,TFALSUM]) = 1 ;

hence (SAT M) . [n,(A '&&' B)] = 1 by Def11; :: thesis: verum

for M being LTLModel holds

( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )

let n be Element of NAT ; :: thesis: for M being LTLModel holds

( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )

let M be LTLModel; :: thesis: ( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )

hereby :: thesis: ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 implies (SAT M) . [n,(A '&&' B)] = 1 )

assume that assume
(SAT M) . [n,(A '&&' B)] = 1
; :: thesis: ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 )

then ((SAT M) . [n,(A => (B => TFALSUM))]) => ((SAT M) . [n,TFALSUM]) = 1 by Def11;

then ((SAT M) . [n,(A => (B => TFALSUM))]) => FALSE = 1 by Def11;

then ((SAT M) . [n,A]) => ((SAT M) . [n,(B => TFALSUM)]) = 0 by Def11;

then ((SAT M) . [n,A]) => (((SAT M) . [n,B]) => ((SAT M) . [n,TFALSUM])) = 0 by Def11;

then A1: ((SAT M) . [n,A]) => (((SAT M) . [n,B]) => FALSE) = 0 by Def11;

( (SAT M) . [n,A] = 0 or (SAT M) . [n,A] = 1 ) by XBOOLEAN:def 3;

hence ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) by A1; :: thesis: verum

end;then ((SAT M) . [n,(A => (B => TFALSUM))]) => ((SAT M) . [n,TFALSUM]) = 1 by Def11;

then ((SAT M) . [n,(A => (B => TFALSUM))]) => FALSE = 1 by Def11;

then ((SAT M) . [n,A]) => ((SAT M) . [n,(B => TFALSUM)]) = 0 by Def11;

then ((SAT M) . [n,A]) => (((SAT M) . [n,B]) => ((SAT M) . [n,TFALSUM])) = 0 by Def11;

then A1: ((SAT M) . [n,A]) => (((SAT M) . [n,B]) => FALSE) = 0 by Def11;

( (SAT M) . [n,A] = 0 or (SAT M) . [n,A] = 1 ) by XBOOLEAN:def 3;

hence ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) by A1; :: thesis: verum

A2: (SAT M) . [n,A] = 1 and

A3: (SAT M) . [n,B] = 1 ; :: thesis: (SAT M) . [n,(A '&&' B)] = 1

((SAT M) . [n,B]) => ((SAT M) . [n,TFALSUM]) = 0 by A3, Def11;

then ((SAT M) . [n,A]) => ((SAT M) . [n,(B => TFALSUM)]) = 0 by A2, Def11;

then (SAT M) . [n,(A => (B => TFALSUM))] = 0 by Def11;

then ((SAT M) . [n,(A => (B => TFALSUM))]) => ((SAT M) . [n,TFALSUM]) = 1 ;

hence (SAT M) . [n,(A '&&' B)] = 1 by Def11; :: thesis: verum