let A, B be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF holds
( F \/ {A} |=0 B iff F |=0 A => B )
let F be Subset of LTLB_WFF; :: thesis: ( F \/ {A} |=0 B iff F |=0 A => B )
hereby :: thesis: ( F |=0 A => B implies F \/ {A} |=0 B )
assume A3: F \/ {A} |=0 B ; :: thesis: F |=0 A => B
thus F |=0 A => B :: thesis: verum
proof
let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F implies M |=0 A => B )
assume A4: M |=0 F ; :: thesis: M |=0 A => B
A2: (SAT M) . [0,(A => B)] = ((SAT M) . [0,A]) => ((SAT M) . [0,B]) by LTLAXIO1:def 11;
thus M |=0 A => B :: thesis: verum
proof
per cases ( (SAT M) . [0,A] = 0 or (SAT M) . [0,A] = 1 ) by XBOOLEAN:def 3;
suppose (SAT M) . [0,A] = 0 ; :: thesis: M |=0 A => B
hence (SAT M) . [0,(A => B)] = 1 by A2; :: according to LTLAXIO5:def 1 :: thesis: verum
end;
suppose (SAT M) . [0,A] = 1 ; :: thesis: M |=0 A => B
then M |=0 A ;
then M |=0 {A} by th263pb;
then M |=0 B by A3, th263pa, A4;
hence (SAT M) . [0,(A => B)] = 1 by A2; :: according to LTLAXIO5:def 1 :: thesis: verum
end;
end;
end;
end;
end;
assume A6: F |=0 A => B ; :: thesis: F \/ {A} |=0 B
let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F \/ {A} implies M |=0 B )
assume M |=0 F \/ {A} ; :: thesis: M |=0 B
then A5: ( M |=0 F & M |=0 {A} ) by th263pa;
then A7: M |=0 A by th263pb;
M |=0 A => B by A5, A6;
then ((SAT M) . [0,A]) => ((SAT M) . [0,B]) = 1 by LTLAXIO1:def 11;
hence M |=0 B by A7; :: thesis: verum