:: Weak Completeness Theorem for Propositional Linear Time Temporal Logic
:: by Mariusz Giero
::
:: Copyright (c) 2012-2017 Association of Mizar Users

set l = LTLB_WFF ;

set pairs = [:(),():];

deffunc H1( FinSequence of LTLB_WFF ) -> Element of LTLB_WFF = 'not' ((con (nega \$1)) /. (len (con (nega \$1))));

deffunc H2( FinSequence of LTLB_WFF ) -> Element of LTLB_WFF = (con \$1) /. (len (con \$1));

definition
let X be finite set ;
:: original: Enumeration
redefine mode Enumeration of X -> one-to-one FinSequence of X;
coherence
for b1 being Enumeration of X holds b1 is one-to-one FinSequence of X
proof end;
end;

definition
let E be set ;
let F be finite Subset of E;
:: original: Enumeration
redefine mode Enumeration of F -> one-to-one FinSequence of E;
coherence
for b1 being Enumeration of F holds b1 is one-to-one FinSequence of E
proof end;
end;

registration
let D be set ;
existence
ex b1 being FinSequenceSet of D st
( not b1 is empty & b1 is finite )
proof end;
end;

theorem Th1: :: LTLAXIO4:1
for X being set
for G being non empty finite FinSequenceSet of X ex A being FinSequence st
( A in G & ( for B being FinSequence st B in G holds
len B <= len A ) )
proof end;

definition
let T be DecoratedTree;
let n be Element of NAT ;
let t be Node of T;
:: original: |
redefine func t | n -> Node of T;
correctness
coherence
t | n is Node of T
;
proof end;
end;

theorem Th2: :: LTLAXIO4:2
for p being Element of LTLB_WFF holds p is FinSequence of NAT
proof end;

notation
let A be Element of LTLB_WFF ;
synonym s-until A for conjunctive ;
end;

definition
let A be Element of LTLB_WFF ;
assume A1: A is s-until ;
func rarg A -> Element of LTLB_WFF means :Def1: :: LTLAXIO4:def 1
ex p being Element of LTLB_WFF st p 'U' it = A;
existence
ex b1, p being Element of LTLB_WFF st p 'U' b1 = A
proof end;
uniqueness
for b1, b2 being Element of LTLB_WFF st ex p being Element of LTLB_WFF st p 'U' b1 = A & ex p being Element of LTLB_WFF st p 'U' b2 = A holds
b1 = b2
by HILBERT2:19;
end;

:: deftheorem Def1 defines rarg LTLAXIO4:def 1 :
for A being Element of LTLB_WFF st A is s-until holds
for b2 being Element of LTLB_WFF holds
( b2 = rarg A iff ex p being Element of LTLB_WFF st p 'U' b2 = A );

definition
let A be Element of LTLB_WFF ;
attr A is satisfiable means :: LTLAXIO4:def 2
ex M being LTLModel ex n being Element of NAT st (SAT M) . [n,A] = 1;
end;

:: deftheorem defines satisfiable LTLAXIO4:def 2 :
for A being Element of LTLB_WFF holds
( A is satisfiable iff ex M being LTLModel ex n being Element of NAT st (SAT M) . [n,A] = 1 );

theorem Th3: :: LTLAXIO4:3
for A being Element of LTLB_WFF holds
( {} LTLB_WFF |= A iff not 'not' A is satisfiable )
proof end;

theorem Th4: :: LTLAXIO4:4
for A being Element of LTLB_WFF st TVERUM '&&' A is satisfiable holds
A is satisfiable
proof end;

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

theorem Th6: :: LTLAXIO4:6
for M being LTLModel
for n being Element of NAT
for f being FinSequence of LTLB_WFF holds
( (SAT M) . [n,((con f) /. (len (con f)))] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 )
proof end;

theorem Th7: :: LTLAXIO4:7
for A being Element of LTLB_WFF holds [(),<*A*>] ^ = TVERUM '&&' ()
proof end;

theorem Th8: :: LTLAXIO4:8
for A, B being Element of LTLB_WFF
for P being complete PNPair st untn (A,B) in rng P holds
( A in rng P & B in rng P & A 'U' B in rng P )
proof end;

theorem Th9: :: LTLAXIO4:9
for P being PNPair holds rng P c= union (Subt (rng P))
proof end;

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

:: deftheorem defines ^ LTLAXIO4:def 3 :
for F being Subset of [:(),():] holds F ^ = { (P ^) where P is Element of [:(),():] : P in F } ;

registration
let F be non empty Subset of [:(),():];
cluster F ^ -> non empty ;
coherence
not F ^ is empty
proof end;
end;

registration
let F be finite Subset of [:(),():];
cluster F ^ -> finite ;
coherence
F ^ is finite
proof end;
end;

theorem Th10: :: LTLAXIO4:10
for F, G being Subset of [:(),():] holds (F \/ G) ^ = (F ^) \/ (G ^)
proof end;

theorem Th11: :: LTLAXIO4:11
proof end;

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

:: deftheorem defines comp LTLAXIO4:def 4 :
for F being finite Subset of LTLB_WFF holds comp F = { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } ;

registration
let F be finite Subset of LTLB_WFF;
cluster -> complete for Element of comp F;
coherence
for b1 being Element of comp F holds b1 is complete
proof end;
end;

theorem Th12: :: LTLAXIO4:12
proof end;

definition
let P, Q be PNPair;
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;

:: deftheorem defines is_completion_of LTLAXIO4:def 5 :
for P, Q being PNPair holds
( Q is_completion_of P iff ( rng (P `1) c= rng (Q `1) & rng (P `2) c= rng (Q `2) & tau (rng P) = rng Q ) );

theorem Th13: :: LTLAXIO4:13
for P, Q being PNPair st Q is_completion_of P holds
Q is complete by LTLAXIO3:17;

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

:: deftheorem defines comp LTLAXIO4:def 6 :
for P being PNPair holds comp P = { Q where Q is consistent PNPair : Q is_completion_of P } ;

registration
let P be consistent PNPair;
cluster comp P -> non empty finite ;
coherence
not comp P is empty
proof end;
end;

registration
let P be consistent PNPair;
cluster -> consistent for Element of comp P;
coherence
for b1 being Element of comp P holds b1 is consistent
proof end;
end;

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

:: deftheorem defines comp LTLAXIO4:def 7 :
for X being Subset of [:(),():] holds comp X = union { (comp P) where P is Element of [:(),():] : P in X } ;

registration
let X be finite Subset of [:(),():];
coherence
comp X is finite
proof end;
end;

theorem Th14: :: LTLAXIO4:14
for Q being PNPair
for X being non empty Subset of [:(),():] st Q in X holds
comp Q c= comp X
proof end;

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

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

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

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

:: deftheorem defines untn LTLAXIO4:def 8 :
for X being Subset of LTLB_WFF holds untn X = { (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } ;

registration
let X be finite Subset of LTLB_WFF;
coherence
untn X is finite
proof end;
end;

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

:: deftheorem defines untn LTLAXIO4:def 9 :
for P being PNPair holds untn P = { Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } ;

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

registration
let P be consistent PNPair;
cluster -> consistent for Element of untn P;
coherence
for b1 being Element of untn P holds b1 is consistent
proof end;
end;

definition
let P be PNPair;
func compn P -> finite Subset of [:(),():] equals :: LTLAXIO4:def 10
{ Q where Q is Element of [:(),():] : Q in comp (untn P) } ;
coherence
{ Q where Q is Element of [:(),():] : Q in comp (untn P) } is finite Subset of [:(),():]
proof end;
end;

:: deftheorem defines compn LTLAXIO4:def 10 :
for P being PNPair holds compn P = { Q where Q is Element of [:(),():] : Q in comp (untn P) } ;

registration
let P be consistent PNPair;
cluster compn P -> non empty finite ;
coherence
not compn P is empty
proof end;
end;

registration
let P be consistent PNPair;
cluster -> consistent for Element of compn P;
coherence
for b1 being Element of compn P holds b1 is consistent
proof end;
end;

theorem Th19: :: LTLAXIO4:19
for P, Q, R being PNPair st Q in compn P & R in untn P holds
Q is_completion_of R
proof end;

theorem Th20: :: LTLAXIO4:20
for P, Q being PNPair st Q in compn P holds
Q is complete
proof end;

registration
let P be consistent PNPair;
cluster -> complete for Element of compn P;
coherence
for b1 being Element of compn P holds b1 is complete
by Th20;
end;

theorem Th21: :: LTLAXIO4:21
for A, B being Element of LTLB_WFF
for P, Q being PNPair st A 'U' B in rng (P `2) & Q in compn P holds
untn (A,B) in rng (Q `2)
proof end;

theorem Th22: :: LTLAXIO4:22
for A, B being Element of LTLB_WFF
for P, Q being PNPair st A 'U' B in rng (P `1) & Q in compn P holds
untn (A,B) in rng (Q `1)
proof end;

theorem Th23: :: LTLAXIO4:23
for P, Q, R being PNPair st R in compn Q & rng Q c= union (Subt (rng P)) holds
rng R c= union (Subt (rng P))
proof end;

theorem Th24: :: LTLAXIO4:24
for A, B being Element of LTLB_WFF
for P being consistent complete PNPair
for Q being 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) ) )
proof end;

theorem Th25: :: LTLAXIO4:25
for A, B being Element of LTLB_WFF
for P being consistent complete PNPair
for Q being Element of compn P holds
( not A 'U' B in rng (P `1) or B in rng (Q `1) or ( A in rng (Q `1) & A 'U' B in rng (Q `1) ) )
proof end;

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

:: deftheorem Def11 defines pnptree LTLAXIO4:def 11 :
for P being PNPair
for b2 being finite-branching DecoratedTree of [:(),():] holds
( b2 is pnptree of P iff ( b2 . {} = P & ( for t being Element of dom b2
for w being Element of [:(),():] st w = b2 . t holds
succ (b2,t) = the Enumeration of compn w ) ) );

definition
let P be PNPair;
let T be pnptree of P;
let t be Node of T;
:: original: |
redefine func T | t -> pnptree of T . t;
correctness
coherence
T | t is pnptree of T . t
;
proof end;
end;

theorem Th26: :: LTLAXIO4:26
for P being PNPair
for T being pnptree of P
for t being Node of T
for n being Nat st t ^ <*n*> in dom T holds
T . (t ^ <*n*>) in compn (T . t)
proof end;

theorem Th27: :: LTLAXIO4:27
for P, Q being PNPair
for T being pnptree of P st Q in rng T holds
rng Q c= union (Subt (rng P))
proof end;

registration
let P be PNPair;
let T be pnptree of P;
cluster rng T -> non empty finite ;
coherence
( not rng T is empty & rng T is finite )
proof end;
end;

registration
let P be consistent PNPair;
let T be pnptree of P;
cluster -> consistent for Element of rng T;
coherence
for b1 being Element of rng T holds b1 is consistent
proof end;
end;

registration
let P be consistent complete PNPair;
let T be pnptree of P;
cluster -> complete for Element of rng T;
coherence
for b1 being Element of rng T holds b1 is complete
proof end;
end;

registration
let P be consistent complete PNPair;
let T be pnptree of P;
let t be Node of T;
cluster T . t -> consistent complete for PNPair;
coherence
for b1 being PNPair st b1 = T . t holds
( not b1 is Inconsistent & b1 is complete )
proof end;
end;

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

definition
let P be PNPair;
let T be pnptree of P;
func rngr T -> finite Subset of [:(),():] equals :: LTLAXIO4:def 12
{ (T . t) where t is Node of T : t <> {} } ;
correctness
coherence
{ (T . t) where t is Node of T : t <> {} } is finite Subset of [:(),():]
;
proof end;
end;

:: deftheorem defines rngr LTLAXIO4:def 12 :
for P being PNPair
for T being pnptree of P holds rngr T = { (T . t) where t is Node of T : t <> {} } ;

registration
let P be consistent PNPair;
let T be pnptree of P;
cluster rngr T -> non empty finite ;
coherence
not rngr T is empty
proof end;
end;

theorem Th28: :: LTLAXIO4:28
for P, Q, R being PNPair
for T being pnptree of P st R in rng T & Q in untn R holds
comp Q c= rngr T
proof end;

theorem Th29: :: LTLAXIO4:29
for P being consistent complete PNPair
for T being pnptree of P
for f being 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))))))
proof end;

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

:: deftheorem Def13 defines path LTLAXIO4:def 13 :
for P being consistent PNPair
for T being pnptree of P
for b3 being sequence of (dom T) holds
( b3 is path of T iff ( b3 . 0 = {} & ( for k being Nat holds b3 . (k + 1) in succ (b3 . k) ) ) );

definition
let P be consistent complete PNPair;
let T be pnptree of P;
let t be path of T;
let i be Nat;
:: original: .
redefine func t . i -> Node of T;
coherence
t . i is Node of T
proof end;
end;

theorem Th30: :: LTLAXIO4:30
for A, B being Element of LTLB_WFF
for i being Nat
for P being consistent complete PNPair
for T being pnptree of P
for t being path of T st A 'U' B in rng ((T . (t . i)) `2) holds
for j being Element of NAT holds
( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st
( i < k & k < j & A in rng ((T . (t . k)) `2) ) )
proof end;

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

theorem Th32: :: LTLAXIO4:32
for A, B being Element of LTLB_WFF
for P being consistent complete PNPair
for T being pnptree of P st A 'U' B in rng (P `1) holds
ex R being Element of rngr T st B in rng (R `1)
proof end;

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

:: deftheorem Def14 defines complete LTLAXIO4:def 14 :
for P being consistent PNPair
for T being pnptree of P
for t being path of T holds
( t is complete iff for A, B being Element of LTLB_WFF
for i being Nat st A 'U' B in rng ((T . (t . i)) `1) holds
ex j being Element of NAT st
( j > i & B in rng ((T . (t . j)) `1) & ( for k being Element of NAT st i < k & k < j holds
A in rng ((T . (t . k)) `1) ) ) );

registration
let P be consistent complete PNPair;
let T be pnptree of P;
existence
ex b1 being path of T st b1 is complete
proof end;
end;

registration
let P be consistent PNPair;
coherence
P ^ is satisfiable
proof end;
end;

:: Completeness theorem for Propositional Linear Temporal Logic
theorem :: LTLAXIO4:33
for A being Element of LTLB_WFF
for F being finite Subset of LTLB_WFF st F |= A holds
F |- A
proof end;