let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st X |- p => q & X |- p => ('X' p) holds

X |- p => ('G' q)

let X be Subset of LTLB_WFF; :: thesis: ( X |- p => q & X |- p => ('X' p) implies X |- p => ('G' q) )

assume that

A1: X |- p => q and

A2: X |- p => ('X' p) ; :: thesis: X |- p => ('G' q)

consider f being FinSequence of LTLB_WFF such that

A3: f . (len f) = p => q and

A4: 1 <= len f and

A5: for i being Nat st 1 <= i & i <= len f holds

prc f,X,i by A1;

consider g being FinSequence of LTLB_WFF such that

A6: g . (len g) = p => ('X' p) and

A7: 1 <= len g and

A8: for i being Nat st 1 <= i & i <= len g holds

prc g,X,i by A2;

A9: for i being Nat st 1 <= i & i <= len (f ^ g) holds

prc f ^ g,X,i by A4, A5, A7, A8, Th39;

set h = (f ^ g) ^ <*(p => ('G' q))*>;

A10: (f ^ g) ^ <*(p => ('G' q))*> = f ^ (g ^ <*(p => ('G' q))*>) by FINSEQ_1:32;

A11: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;

then A12: 1 <= len (f ^ g) by A4, NAT_1:12;

A13: len ((f ^ g) ^ <*(p => ('G' q))*>) = (len (f ^ g)) + (len <*(p => ('G' q))*>) by FINSEQ_1:22

.= (len (f ^ g)) + 1 by FINSEQ_1:39 ;

then 1 <= len ((f ^ g) ^ <*(p => ('G' q))*>) by A4, A11, NAT_1:16;

then A14: ((f ^ g) ^ <*(p => ('G' q))*>) /. (len ((f ^ g) ^ <*(p => ('G' q))*>)) = ((f ^ g) ^ <*(p => ('G' q))*>) . (len ((f ^ g) ^ <*(p => ('G' q))*>)) by Lm1

.= p => ('G' q) by A13, FINSEQ_1:42 ;

len ((f ^ g) ^ <*(p => ('G' q))*>) = (len f) + ((len g) + 1) by A11, A13;

then A15: len f < len ((f ^ g) ^ <*(p => ('G' q))*>) by NAT_1:16;

then A16: ((f ^ g) ^ <*(p => ('G' q))*>) /. (len f) = ((f ^ g) ^ <*(p => ('G' q))*>) . (len f) by A4, Lm1

.= p => q by A3, A4, A10, FINSEQ_1:64 ;

A17: len (f ^ g) < len ((f ^ g) ^ <*(p => ('G' q))*>) by A13, NAT_1:16;

then ((f ^ g) ^ <*(p => ('G' q))*>) /. (len (f ^ g)) = ((f ^ g) ^ <*(p => ('G' q))*>) . (len (f ^ g)) by A12, Lm1

.= (f ^ g) . (len (f ^ g)) by A12, FINSEQ_1:64

.= (f ^ g) . ((len f) + (len g)) by FINSEQ_1:22

.= p => ('X' p) by A6, A7, FINSEQ_1:65 ;

then ((f ^ g) ^ <*(p => ('G' q))*>) /. (len f),((f ^ g) ^ <*(p => ('G' q))*>) /. (len (f ^ g)) IND_rule ((f ^ g) ^ <*(p => ('G' q))*>) /. (len ((f ^ g) ^ <*(p => ('G' q))*>)) by A16, A14;

then prc (f ^ g) ^ <*(p => ('G' q))*>,X, len ((f ^ g) ^ <*(p => ('G' q))*>) by A4, A12, A15, A17;

hence X |- p => ('G' q) by A12, A9, Th40; :: thesis: verum

X |- p => ('G' q)

let X be Subset of LTLB_WFF; :: thesis: ( X |- p => q & X |- p => ('X' p) implies X |- p => ('G' q) )

assume that

A1: X |- p => q and

A2: X |- p => ('X' p) ; :: thesis: X |- p => ('G' q)

consider f being FinSequence of LTLB_WFF such that

A3: f . (len f) = p => q and

A4: 1 <= len f and

A5: for i being Nat st 1 <= i & i <= len f holds

prc f,X,i by A1;

consider g being FinSequence of LTLB_WFF such that

A6: g . (len g) = p => ('X' p) and

A7: 1 <= len g and

A8: for i being Nat st 1 <= i & i <= len g holds

prc g,X,i by A2;

A9: for i being Nat st 1 <= i & i <= len (f ^ g) holds

prc f ^ g,X,i by A4, A5, A7, A8, Th39;

set h = (f ^ g) ^ <*(p => ('G' q))*>;

A10: (f ^ g) ^ <*(p => ('G' q))*> = f ^ (g ^ <*(p => ('G' q))*>) by FINSEQ_1:32;

A11: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;

then A12: 1 <= len (f ^ g) by A4, NAT_1:12;

A13: len ((f ^ g) ^ <*(p => ('G' q))*>) = (len (f ^ g)) + (len <*(p => ('G' q))*>) by FINSEQ_1:22

.= (len (f ^ g)) + 1 by FINSEQ_1:39 ;

then 1 <= len ((f ^ g) ^ <*(p => ('G' q))*>) by A4, A11, NAT_1:16;

then A14: ((f ^ g) ^ <*(p => ('G' q))*>) /. (len ((f ^ g) ^ <*(p => ('G' q))*>)) = ((f ^ g) ^ <*(p => ('G' q))*>) . (len ((f ^ g) ^ <*(p => ('G' q))*>)) by Lm1

.= p => ('G' q) by A13, FINSEQ_1:42 ;

len ((f ^ g) ^ <*(p => ('G' q))*>) = (len f) + ((len g) + 1) by A11, A13;

then A15: len f < len ((f ^ g) ^ <*(p => ('G' q))*>) by NAT_1:16;

then A16: ((f ^ g) ^ <*(p => ('G' q))*>) /. (len f) = ((f ^ g) ^ <*(p => ('G' q))*>) . (len f) by A4, Lm1

.= p => q by A3, A4, A10, FINSEQ_1:64 ;

A17: len (f ^ g) < len ((f ^ g) ^ <*(p => ('G' q))*>) by A13, NAT_1:16;

then ((f ^ g) ^ <*(p => ('G' q))*>) /. (len (f ^ g)) = ((f ^ g) ^ <*(p => ('G' q))*>) . (len (f ^ g)) by A12, Lm1

.= (f ^ g) . (len (f ^ g)) by A12, FINSEQ_1:64

.= (f ^ g) . ((len f) + (len g)) by FINSEQ_1:22

.= p => ('X' p) by A6, A7, FINSEQ_1:65 ;

then ((f ^ g) ^ <*(p => ('G' q))*>) /. (len f),((f ^ g) ^ <*(p => ('G' q))*>) /. (len (f ^ g)) IND_rule ((f ^ g) ^ <*(p => ('G' q))*>) /. (len ((f ^ g) ^ <*(p => ('G' q))*>)) by A16, A14;

then prc (f ^ g) ^ <*(p => ('G' q))*>,X, len ((f ^ g) ^ <*(p => ('G' q))*>) by A4, A12, A15, A17;

hence X |- p => ('G' q) by A12, A9, Th40; :: thesis: verum