let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |-0 'G' A holds

F |-0 'G' ('X' A)

let F be Subset of LTLB_WFF; :: thesis: ( F |-0 'G' A implies F |-0 'G' ('X' A) )

assume F |-0 'G' A ; :: thesis: F |-0 'G' ('X' A)

then consider f being FinSequence of LTLB_WFF such that

A1: f . (len f) = 'G' A and

A2: 1 <= len f and

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

prc0 f,F,i ;

set g = f ^ <*('G' ('X' A))*>;

A4: len (f ^ <*('G' ('X' A))*>) = (len f) + (len <*('G' ('X' A))*>) by FINSEQ_1:22

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

then A5: len f < len (f ^ <*('G' ('X' A))*>) by NAT_1:16;

then A6: (f ^ <*('G' ('X' A))*>) /. (len f) = (f ^ <*('G' ('X' A))*>) . (len f) by A2, Lm1

.= 'G' A by A1, A2, FINSEQ_1:64 ;

1 <= len (f ^ <*('G' ('X' A))*>) by A2, A4, NAT_1:16;

then (f ^ <*('G' ('X' A))*>) /. (len (f ^ <*('G' ('X' A))*>)) = (f ^ <*('G' ('X' A))*>) . (len (f ^ <*('G' ('X' A))*>)) by Lm1

.= 'G' ('X' A) by A4, FINSEQ_1:42 ;

then (f ^ <*('G' ('X' A))*>) /. (len f) NEX0_rule (f ^ <*('G' ('X' A))*>) /. (len (f ^ <*('G' ('X' A))*>)) by A6;

then prc0 f ^ <*('G' ('X' A))*>,F, len (f ^ <*('G' ('X' A))*>) by A2, A5;

hence F |-0 'G' ('X' A) by A2, A3, Th40; :: thesis: verum

F |-0 'G' ('X' A)

let F be Subset of LTLB_WFF; :: thesis: ( F |-0 'G' A implies F |-0 'G' ('X' A) )

assume F |-0 'G' A ; :: thesis: F |-0 'G' ('X' A)

then consider f being FinSequence of LTLB_WFF such that

A1: f . (len f) = 'G' A and

A2: 1 <= len f and

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

prc0 f,F,i ;

set g = f ^ <*('G' ('X' A))*>;

A4: len (f ^ <*('G' ('X' A))*>) = (len f) + (len <*('G' ('X' A))*>) by FINSEQ_1:22

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

then A5: len f < len (f ^ <*('G' ('X' A))*>) by NAT_1:16;

then A6: (f ^ <*('G' ('X' A))*>) /. (len f) = (f ^ <*('G' ('X' A))*>) . (len f) by A2, Lm1

.= 'G' A by A1, A2, FINSEQ_1:64 ;

1 <= len (f ^ <*('G' ('X' A))*>) by A2, A4, NAT_1:16;

then (f ^ <*('G' ('X' A))*>) /. (len (f ^ <*('G' ('X' A))*>)) = (f ^ <*('G' ('X' A))*>) . (len (f ^ <*('G' ('X' A))*>)) by Lm1

.= 'G' ('X' A) by A4, FINSEQ_1:42 ;

then (f ^ <*('G' ('X' A))*>) /. (len f) NEX0_rule (f ^ <*('G' ('X' A))*>) /. (len (f ^ <*('G' ('X' A))*>)) by A6;

then prc0 f ^ <*('G' ('X' A))*>,F, len (f ^ <*('G' ('X' A))*>) by A2, A5;

hence F |-0 'G' ('X' A) by A2, A3, Th40; :: thesis: verum