:: Weak Completeness Theorem for Propositional Linear Time Temporal Logic
::  by Mariusz Giero
::
:: Received May 7, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI,
      RELAT_1, XBOOLE_0, FUNCT_1, XBOOLEAN, MODELC_2, CQC_THE1, NAT_1,
      XXREAL_0, ORDINAL1, ARYTM_1, ZF_LANG, PARTFUN1, MARGREL1, HILBERT2,
      ZFMISC_1, ZF_MODEL, GLIB_000, FINSET_1, ABCMIZ_0, HENMODEL, PRE_POLY,
      RFINSEQ, FIB_NUM, REWRITE1, MATROID0, MCART_1, UNIALG_2, TREES_1,
      TREES_2, TREES_4, SETFAM_1, NECKLA_3, MEMBER_1, AOFA_I00, FINSEQ_4,
      FINSEQ_2, RFINSEQ2, TREES_9, INT_1, VECTSP_1, LTLAXIO1, LTLAXIO2,
      LTLAXIO3, LTLAXIO4, GOEDCPUC, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
      CARD_1, RELAT_1, FUNCT_1, MCART_1, RELSET_1, PARTFUN1, DOMAIN_1, NUMBERS,
      XCMPLX_0, NAT_1, XXREAL_0, TREES_1, TREES_2, TREES_4, TREES_9, XREAL_0,
      NAT_D, FUNCT_2, FINSET_1, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_2,
      FINSEQ_4, AFINSQ_1, LEXBFS, RFINSEQ, RFINSEQ2, HILBERT1, HILBERT2,
      STRUCT_0, XBOOLEAN, MARGREL1, AOFA_I00, MATROID0, RLAFFIN3, LTLAXIO1,
      LTLAXIO2, LTLAXIO3;
 constructors XXREAL_0, NAT_D, RELSET_1, AOFA_I00, HILBERT2, FINSET_1, RFINSEQ,
      DOMAIN_1, AFINSQ_2, REAL_1, STRUCT_0, FUNCOP_1, XREAL_0, MATROID0,
      LEXBFS, MCART_1, CARD_1, RLAFFIN3, FINSEQ_4, FINSEQ_5, FINSEQ_2,
      RFINSEQ2, BINOP_2, ENUMSET1, SETFAM_1, TREES_9, TREES_2, TREES_4,
      AFINSQ_1, LTLAXIO1, LTLAXIO2, LTLAXIO3;
 registrations SUBSET_1, ORDINAL1, FUNCT_1, XXREAL_0, NAT_1, XBOOLEAN,
      RELSET_1, MARGREL1, XBOOLE_0, XREAL_0, HILBERT1, FINSET_1, FINSEQ_1,
      JORDAN23, FINSEQ_2, CARD_1, TREES_9, TREES_2, XTUPLE_0, LTLAXIO1,
      LTLAXIO3;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;


begin

reserve A,B,p,q,r for Element of LTLB_WFF,
  M for LTLModel,
  j,k,n for Element of NAT,
  i for Nat,
  X for Subset of LTLB_WFF,
  F for finite Subset of LTLB_WFF,
  f for FinSequence of LTLB_WFF,
  g for Function of LTLB_WFF,BOOLEAN,
  x,y,z for set,
  P,Q,R for PNPair;

definition
  let X be finite set;
  redefine mode Enumeration of X -> one-to-one FinSequence of X;
end;

definition
  let E be set,F be finite Subset of E;
  redefine mode Enumeration of F -> one-to-one FinSequence of E;
end;

registration
  let D be set;
  cluster non empty finite for FinSequenceSet of D;
end;

theorem :: LTLAXIO4:1
  for X be set,G be non empty finite FinSequenceSet of X holds
  ex A be FinSequence st A in G &
  for B be FinSequence st B in G holds len B <= len A;

definition
  let T be DecoratedTree;
  let n;
  let t be Node of T;
  redefine func t | n -> Node of T;
end;

theorem :: LTLAXIO4:2
p is FinSequence of NAT;

notation
  let A;
  synonym A is s-until for A is conjunctive;
end;

definition
  let A;
  assume A is s-until;
  func rarg A -> Element of LTLB_WFF means
:: LTLAXIO4:def 1
ex p st p 'U' it = A;
end;

definition
  let A;
  attr A is satisfiable means
:: LTLAXIO4:def 2
ex M,n st (SAT M).[n,A] = 1;
end;

theorem :: LTLAXIO4:3
{} LTLB_WFF |= A iff not 'not' A is satisfiable;

theorem :: LTLAXIO4:4
TVERUM '&&' A is satisfiable implies A is satisfiable;

theorem :: LTLAXIO4:5
  for i being Element of NAT holds
  (SAT M).[i,p 'U' q] = 1 iff
  ex j st j > i & (SAT M).[j,q] = 1 &
  for k st i < k & k < j holds (SAT M).[k,p] = 1;

theorem :: LTLAXIO4:6
(SAT M).[n,(con f)/.(len con f)] = 1
  iff for i st i in dom f holds (SAT M).[n,f/.i] = 1;

theorem :: LTLAXIO4:7
([<*> LTLB_WFF,<*A*>])^ = TVERUM '&&' 'not' A;

theorem :: LTLAXIO4:8
for P be complete PNPair st untn(A,B) in rng P
  holds A in rng P & B in rng P & A 'U' B in rng P;

theorem :: LTLAXIO4:9
rng P c= union Subt rng P;

begin

definition
  let F be Subset of [:LTLB_WFF**,LTLB_WFF**:];
  func F^ -> Subset of LTLB_WFF equals
:: LTLAXIO4:def 3
  {P^ where P is Element of [:LTLB_WFF**,LTLB_WFF**:]: P in F};
end;

registration
  let F be non empty Subset of [:LTLB_WFF**,LTLB_WFF**:];
  cluster F^ -> non empty;
end;

registration
  let F be finite Subset of [:LTLB_WFF**,LTLB_WFF**:];
  cluster F^ -> finite;
  end;

theorem :: LTLAXIO4:10
  for F,G be Subset of [:LTLB_WFF**,LTLB_WFF**:] holds (F \/ G)^ = F^ \/ G^;

theorem :: LTLAXIO4:11
{[<*>LTLB_WFF,<*>LTLB_WFF]}^ = {TVERUM '&&' TVERUM};

definition
  let F be finite Subset of LTLB_WFF;
  func comp F -> non empty finite Subset of [:LTLB_WFF**,LTLB_WFF**:] equals
:: LTLAXIO4:def 4
  {Q where Q is PNPair: rng Q = tau F & rng Q`1 misses rng Q`2};
end;

registration
  let F be finite Subset of LTLB_WFF;
  cluster -> complete for Element of (comp F);
end;

theorem :: LTLAXIO4:12
comp {}LTLB_WFF = {[<*>LTLB_WFF,<*>LTLB_WFF]};

definition
  let P,Q;
  pred Q is_completion_of P means
:: LTLAXIO4:def 5
  rng P`1 c= rng Q`1 & rng P`2 c= rng Q`2 & tau rng P = rng Q;
end;

theorem :: LTLAXIO4:13
Q is_completion_of P implies Q is complete;

definition
  let P;
  func comp P -> finite Subset of [:LTLB_WFF**,LTLB_WFF**:] equals
:: LTLAXIO4:def 6
  {Q where Q is consistent PNPair: Q is_completion_of P};
end;

registration
  let P be consistent PNPair;
  cluster comp P -> non empty;
end;

registration
  let P be consistent PNPair;
  cluster -> consistent for Element of comp P;
end;

definition
  let X be Subset of [:LTLB_WFF**,LTLB_WFF**:];
  func comp X -> Subset of [:LTLB_WFF**,LTLB_WFF**:] equals
:: LTLAXIO4:def 7
  union {comp P where P is Element of [:LTLB_WFF**,LTLB_WFF**:]: P in X};
end;

registration
  let X be finite Subset of [:LTLB_WFF**,LTLB_WFF**:];
  cluster comp X -> finite;
end;

theorem :: LTLAXIO4:14
for X be non empty Subset of [:(LTLB_WFF **),(LTLB_WFF **):]
  st Q in X holds comp Q c= comp X;

theorem :: LTLAXIO4:15
for F be non empty finite Subset of LTLB_WFF
  ex p st p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p};

theorem :: LTLAXIO4:16
for F be finite Subset of LTLB_WFF,f be FinSequence of LTLB_WFF
  st rng f = (comp F)^ holds
  {}LTLB_WFF |- 'not' ((con nega f)/.(len con nega f));

theorem :: LTLAXIO4:17
for P be consistent PNPair,f be FinSequence of LTLB_WFF
  st rng f = (comp P)^
  holds {}LTLB_WFF |- P^ => 'not' ((con nega f)/.(len con nega f));

begin

definition
  let X;
  func untn X -> Subset of LTLB_WFF equals
:: LTLAXIO4:def 8
  {untn(A,B)
  where A is Element of LTLB_WFF,B is Element of LTLB_WFF: A 'U' B in X};
 end;

registration
  let X be finite Subset of LTLB_WFF;
  cluster untn X -> finite;
end;

definition
  let P;
  func untn P -> non empty finite Subset of [:LTLB_WFF**,LTLB_WFF**:] equals
:: LTLAXIO4:def 9
  {Q where Q is PNPair: rng Q`1 = untn rng P`1 & rng Q`2 = untn rng P`2};
end;

theorem :: LTLAXIO4:18
for Q be Element of untn P holds {}LTLB_WFF |- P^ => 'X'(Q^);

registration
  let P be consistent PNPair;
  cluster -> consistent for Element of untn P;
end;

definition
  let P;
  func compn P -> finite Subset of [:LTLB_WFF**,LTLB_WFF**:] equals
:: LTLAXIO4:def 10
  {Q where Q is Element of [:LTLB_WFF**,LTLB_WFF**:]: Q in comp untn P};
end;

registration
  let P be consistent PNPair;
  cluster compn P -> non empty;
end;

registration
  let P be consistent PNPair;
  cluster -> consistent for Element of compn P;
end;

theorem :: LTLAXIO4:19
Q in compn P & R in untn P implies Q is_completion_of R;

theorem :: LTLAXIO4:20
Q in compn P implies Q is complete;

registration
  let P be consistent PNPair;
  cluster -> complete for Element of compn P;
end;

theorem :: LTLAXIO4:21
A 'U' B in rng P`2 & Q in compn P implies untn(A,B) in rng Q`2;

theorem :: LTLAXIO4:22
A 'U' B in rng P`1 & Q in compn P implies untn(A,B) in rng Q`1;

theorem :: LTLAXIO4:23
  R in compn Q & rng Q c= union Subt rng P implies rng R c= union Subt rng P;

theorem :: LTLAXIO4:24
for P be consistent complete PNPair,Q be Element of compn P st
A 'U' B in rng P`2 holds B in rng Q`2 & (A in rng Q`2 or A 'U' B in rng Q`2);

theorem :: LTLAXIO4:25
for P be consistent complete PNPair,Q be Element of compn P st
A 'U' B in rng P`1 holds (B in rng Q`1 or A in rng Q`1 & A 'U' B in rng Q`1);

begin

definition
  let P;
  mode pnptree of P ->
  finite-branching DecoratedTree of [:LTLB_WFF**,LTLB_WFF**:] means
:: LTLAXIO4:def 11
  it.{} = P & for t being Element of dom it
  for w being Element of [:LTLB_WFF**,LTLB_WFF**:] st w = it.t
  holds succ (it,t) = the Enumeration of compn w;
end;

reserve T for pnptree of P,t for Node of T;

definition
  let P,T,t;
  redefine func T|t -> pnptree of T.t;
end;

theorem :: LTLAXIO4:26
 for n being Nat st t^<*n*> in dom T
  holds T.(t^<*n*>) in compn (T.t);

theorem :: LTLAXIO4:27
Q in rng T implies rng Q c= union Subt rng P;

registration
  let P,T;
  cluster rng T -> non empty finite;
end;

registration
  let P be consistent PNPair;
  let T be pnptree of P;
  cluster -> consistent for Element of rng T;
end;

registration
  let P be consistent complete PNPair;
  let T be pnptree of P;
  cluster -> complete for Element of rng T;
end;

registration
  let P be consistent complete PNPair,T be pnptree of P,t be Node of T;
  cluster T.t -> consistent complete for PNPair;
end;

registration
  let P be consistent PNPair,T be pnptree of P;
  let t be Element of dom T;
  cluster succ t -> non empty;
end;

definition
  let P,T;
  func rngr T -> finite Subset of [:LTLB_WFF**,LTLB_WFF**:] equals
:: LTLAXIO4:def 12
  {T.t where t is Node of T: t <> {}};
end;

registration
  let P be consistent PNPair, T be pnptree of P;
  cluster rngr T -> non empty;
end;

theorem :: LTLAXIO4:28
R in rng T & Q in untn R implies comp Q c= rngr T;

theorem :: LTLAXIO4:29
  for P be consistent complete PNPair,T be pnptree of P,
  f be FinSequence of LTLB_WFF st rng f = (rngr T)^ holds
  {}LTLB_WFF |- ('not' ((con nega f)/.(len con nega f))) =>
  ('X' ('not' ((con nega f)/.(len con nega f))));

begin

definition
  let P be consistent PNPair;
  let T be pnptree of P;
  mode path of T -> sequence of dom T means
:: LTLAXIO4:def 13
  it.0 = {} & for k be Nat holds it.(k+1) in succ (it.k);
end;

definition
  let P be consistent complete PNPair,T be pnptree of P,t be path of T,i;
  redefine func t.i -> Node of T;
end;

theorem :: LTLAXIO4:30
  for P be consistent complete PNPair,T be pnptree of P,t be path of T st
  A 'U' B in rng (T.(t.i))`2 holds for j st j > i holds
  (B in rng (T.(t.j))`2 or ex k st i < k & k < j & A in rng (T.(t.k))`2);

theorem :: LTLAXIO4:31
  for P be consistent complete PNPair,T be pnptree of P st
  A 'U' B in rng P`1 & (for Q be Element of rngr T holds not B in rng Q`1)
  holds for Q be Element of rngr T holds B in rng Q`2 & A 'U' B in rng Q`1;

theorem :: LTLAXIO4:32
  for P be consistent complete PNPair,T be pnptree of P st
  A 'U' B in rng P`1 ex R be Element of rngr T st B in rng R`1;

definition
  let P be consistent PNPair,T be pnptree of P;
  let t be path of T;
  attr t is complete means
:: LTLAXIO4:def 14
for i st A 'U' B in rng (T.(t.i))`1
  ex j st j > i & B in rng (T.(t.j))`1 &
  for k st i < k & k < j holds A in rng (T.(t.k))`1;
end;

registration
  let P be consistent complete PNPair,T be pnptree of P;
  cluster complete for path of T;
 end;

registration
  let P be consistent PNPair;
  cluster P^ -> satisfiable;
 end;

::$N Completeness theorem for Propositional Linear Temporal Logic
theorem :: LTLAXIO4:33
F |= A implies F |- A;