:: The Properties of Sets of Temporal Logic Subformulas
::  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, ARYTM_1, ZF_LANG, PARTFUN1, MARGREL1, FUNCT_2, HILBERT2,
      ZFMISC_1, FUNCOP_1, ZF_MODEL, PBOOLE, GLIB_000, FINSET_1, ABCMIZ_0,
      HENMODEL, PRE_POLY, RFINSEQ, FIB_NUM, REWRITE1, MATROID0, MCART_1,
      UNIALG_2, MEMBER_1, FINSEQ_5, LTLAXIO1, LTLAXIO2, LTLAXIO3, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
      CARD_1, RELAT_1, FUNCT_1, XTUPLE_0, 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, FINSEQ_5, AFINSQ_1, LEXBFS, RFINSEQ, RFINSEQ2,
      HILBERT1, HILBERT2, PBOOLE, STRUCT_0, XBOOLEAN, MARGREL1, AOFA_I00,
      MATROID0, LTLAXIO1, LTLAXIO2;
 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, XTUPLE_0;
 registrations SUBSET_1, ORDINAL1, FUNCT_1, NAT_1, XBOOLEAN, RELSET_1,
      MARGREL1, XREAL_0, HILBERT1, FINSET_1, FINSEQ_1, LTLAXIO1, JORDAN23,
      CARD_1, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;


begin

reserve A,B,p,q,r,s for Element of LTLB_WFF,
  n for Element of NAT,
  X for Subset of LTLB_WFF,
  g for Function of LTLB_WFF,BOOLEAN,
  x,y for set;

theorem :: LTLAXIO3:1
  for X be non empty set,t be FinSequence of X,k be Nat st k+1 <= len t
  holds t/^k = <*t.(k+1)*>^(t/^(k+1));

theorem :: LTLAXIO3:2
NAT --> {} is LTLModel;

definition
  let X;
  attr X is without_implication means
:: LTLAXIO3:def 1
  for p st p in X holds not p is conditional;
end;

definition
  let D be set;
  func D** -> set means
:: LTLAXIO3:def 2
  for x holds (x in it iff x is one-to-one FinSequence of D);
  end;

registration
  let D be set;
  cluster D** -> non empty;
end;

registration
  let D be finite set;
  cluster D** -> finite;
end;

theorem :: LTLAXIO3:3
for D1, D2 being set st D1 c= D2 holds D1 ** c= D2 **;

definition
  let a1 be set;
  let a2 be Subset of a1;
  redefine func a2 ** -> non empty Subset of (a1 **);
end;

theorem :: LTLAXIO3:4
for F, G being one-to-one FinSequence st rng F misses rng G
  holds F ^ G is one-to-one;

definition
  let X be set;
  let f,g be one-to-one FinSequence of X;
  assume
 rng f misses rng g;
  func f ^^ g -> one-to-one FinSequence of X equals
:: LTLAXIO3:def 3
f^g;
end;

begin

definition
  func tau1 -> Function of LTLB_WFF,bool LTLB_WFF means
:: LTLAXIO3:def 4
  it.TFALSUM={TFALSUM} & it.(prop n)={prop n} &
  it.(A=>B)={A => B} \/ it.A \/ it.B & it.(A 'U' B)={A 'U' B};
 end;

theorem :: LTLAXIO3:5
not A is conditional implies tau1.A = {A};

theorem :: LTLAXIO3:6
p in tau1.p;

registration
  let p;
  cluster tau1.p -> non empty finite;
end;

theorem :: LTLAXIO3:7
p => q in tau1.r implies p in tau1.r & q in tau1.r;

theorem :: LTLAXIO3:8
p in tau1.q implies tau1.p c= tau1.q;

theorem :: LTLAXIO3:9
p 'U' q in tau1.('not' A) implies p 'U' q in tau1.A;

theorem :: LTLAXIO3:10
  p 'U' q in tau1.(A '&&' B)implies(p 'U' q in tau1.A or p 'U' q in tau1.B);

theorem :: LTLAXIO3:11
p in tau1.q & p <> q implies len p < len q;

theorem :: LTLAXIO3:12
tau1.p c= tau1.('not' p);

theorem :: LTLAXIO3:13
tau1.q c= tau1.(p '&&' q);

theorem :: LTLAXIO3:14
tau1.q c= tau1.(p 'or' q);

definition
  let X;
  func tau X -> Subset of LTLB_WFF means
:: LTLAXIO3:def 5
  x in it iff ex A st A in X & x in tau1.A;
end;

theorem :: LTLAXIO3:15
tau X = union {tau1.p where p is Element of LTLB_WFF: p in X};

theorem :: LTLAXIO3:16
X c= tau X;

registration
  let X be empty Subset of LTLB_WFF;
  cluster tau X -> empty;
end;

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

registration
  let X be non empty Subset of LTLB_WFF;
  cluster tau X -> non empty;
end;

theorem :: LTLAXIO3:17
tau tau X = tau X;

theorem :: LTLAXIO3:18
X is without_implication implies tau X = X;

theorem :: LTLAXIO3:19
p => q in tau X implies p in tau X & q in tau X;

theorem :: LTLAXIO3:20
p '&&' q in tau X implies p in tau X & q in tau X;

theorem :: LTLAXIO3:21
p 'or' q in tau X implies p in tau X & q in tau X;

theorem :: LTLAXIO3:22
untn(p,q) in tau X implies p in tau X & q in tau X & p 'U' q in tau X;

theorem :: LTLAXIO3:23
p in tau X implies tau1.p c= tau X;

begin

definition
  func Sub -> Function of LTLB_WFF,bool LTLB_WFF means
:: LTLAXIO3:def 6
  it.TFALSUM={TFALSUM} & it.(prop n)={prop n} &
  it.(A=>B)={A => B} \/ it.A \/ it.B &
  it.(A 'U' B)= tau1.untn (A,B) \/ it.A \/ it.B;
 end;

theorem :: LTLAXIO3:24
p 'U' q in Sub.(p 'U' q);

theorem :: LTLAXIO3:25
tau1.p c= Sub.p;

registration
  let p;
  cluster Sub.p -> non empty finite;
end;

theorem :: LTLAXIO3:26
p in Sub.(A 'U' B) implies (A 'U' B in Sub.q implies p in Sub.q);

definition
  let X;
  func Subt X -> Subset of bool LTLB_WFF equals
:: LTLAXIO3:def 7
  {Sub.A where A is Element of LTLB_WFF: A in X};
end;

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

begin

definition
  mode PNPair is Element of [:LTLB_WFF**,LTLB_WFF**:];
end;

reserve P,Q,P1,R for PNPair;

definition
  let P;
  redefine func P`1 -> one-to-one FinSequence of LTLB_WFF;
  redefine func P`2 -> one-to-one FinSequence of LTLB_WFF;
end;

definition
  let P;
  func rng P -> finite Subset of LTLB_WFF equals
:: LTLAXIO3:def 8
rng P`1 \/ rng P`2;
end;

definition
  let fp,fm be one-to-one FinSequence of LTLB_WFF;
  redefine func [fp,fm] -> PNPair;
end;

definition
  let P;
  func P^ -> Element of LTLB_WFF equals
:: LTLAXIO3:def 9
  (con (P`1))/.len (con (P`1)) '&&' (con nega (P`2))/.len (con nega (P`2));
end;

theorem :: LTLAXIO3:27
[<*>LTLB_WFF,<*>LTLB_WFF]^ = TVERUM '&&' TVERUM;

theorem :: LTLAXIO3:28
A in rng P`1 implies {} LTLB_WFF |- (P^) => A;

theorem :: LTLAXIO3:29
A in rng P`2 implies {} LTLB_WFF |- (P^) => 'not' A;

definition
  let P;
  attr P is Inconsistent means
:: LTLAXIO3:def 10
{} LTLB_WFF |- 'not' (P^);
end;

notation
  let P;
  antonym P is consistent for P is Inconsistent;
end;

definition
  let P;
  attr P is complete means
:: LTLAXIO3:def 11
tau rng P = rng P;
end;

registration
  cluster [<*> LTLB_WFF,<*> LTLB_WFF] -> consistent for PNPair;
end;

registration
  cluster [<*> LTLB_WFF,<*> LTLB_WFF] -> complete for PNPair;
end;

registration
  cluster consistent complete for PNPair;
end;

registration
  let P be consistent PNPair;
  cluster [P`1,P`2] -> consistent for PNPair;
end;

begin

theorem :: LTLAXIO3:30
for P be consistent PNPair holds rng P`1 misses rng P`2;

theorem :: LTLAXIO3:31
for P be consistent PNPair st not A in rng P holds
  ([(P`1)^^<*A*>,P`2] is consistent or [P`1,(P`2)^^<*A*>] is consistent);

theorem :: LTLAXIO3:32
for P be consistent PNPair holds not TFALSUM in rng P`1;

theorem :: LTLAXIO3:33
  for P be consistent PNPair st A in rng P & B in rng P & A => B in rng P
  holds (A => B in rng P`1 iff (A in rng P`2 or B in rng P`1));

theorem :: LTLAXIO3:34
for P be consistent PNPair ex P1 be consistent PNPair st
  rng (P`1) c= rng (P1`1) & rng (P`2) c= rng (P1`2) & tau rng P = rng P1;