let A, B be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(A 'or' B)] = 1 iff ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) )
let n be Element of NAT ; :: thesis: for M being LTLModel holds
( (SAT M) . [n,(A 'or' B)] = 1 iff ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) )
let M be LTLModel; :: thesis: ( (SAT M) . [n,(A 'or' B)] = 1 iff ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) )

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

assume (SAT M) . [n,(A 'or' B)] = 1 ; :: thesis: ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 )
then A1: (SAT M) . [n,(('not' A) '&&' ('not' B))] = 0 by Th5;

per cases ( not (SAT M) . [n,('not' A)] = 1 or not (SAT M) . [n,('not' B)] = 1 ) by A1, Th7;

suppose not (SAT M) . [n,('not' A)] = 1 ; :: thesis: ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 )

hence ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) by XBOOLEAN:def 3, Th5; :: thesis: verum

end;

suppose not (SAT M) . [n,('not' B)] = 1 ; :: thesis: ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 )

hence ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) by XBOOLEAN:def 3, Th5; :: thesis: verum

end;

end;

end;

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

per cases ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) by A2;

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

then not (SAT M) . [n,('not' A)] = 1 by Th5;
then not (SAT M) . [n,(('not' A) '&&' ('not' B))] = 1 by Th7;
hence (SAT M) . [n,(A 'or' B)] = 1 by Th5, XBOOLEAN:def 3; :: thesis: verum

end;

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

then not (SAT M) . [n,('not' B)] = 1 by Th5;
then not (SAT M) . [n,(('not' A) '&&' ('not' B))] = 1 by Th7;
hence (SAT M) . [n,(A 'or' B)] = 1 by Th5, XBOOLEAN:def 3; :: thesis: verum

end;

end;