let A, B be Element of LTLB_WFF ; 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 ; 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; ( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )
hereby ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 implies (SAT M) . [n,(A '&&' B)] = 1 )
assume
(SAT M) . [n,(A '&&' B)] = 1
;
( (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;
verum
end;
assume that
A2:
(SAT M) . [n,A] = 1
and
A3:
(SAT M) . [n,B] = 1
; (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; verum