:: Model Checking, Part II
:: by Kazuhisa Ishida
::
:: Received April 21, 2008
:: Copyright (c) 2008-2026 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 NUMBERS, NAT_1, CARD_1, ARYTM_3, XXREAL_0, XBOOLE_0, FINSEQ_1,
MODELC_1, XBOOLEAN, ORDINAL4, TARSKI, RELAT_1, SUBSET_1, ZF_LANG,
FUNCT_1, ARYTM_1, BINOP_1, ZFMISC_1, FUNCOP_1, FUNCT_2, VALUED_1,
MARGREL1, ZF_MODEL, MODELC_2, STRUCT_0, FUNCT_5, LATTICES, ROBBINS1,
EQREL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, RELAT_1, FUNCT_1, BINOP_1, FUNCT_2, NAT_1, FINSEQ_1, FUNCOP_1,
MARGREL1, FUNCT_5, MODELC_1, STRUCT_0, LATTICES, ROBBINS1;
constructors BINOP_1, VALUED_1, MODELC_1, RELSET_1, FUNCT_5;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, NAT_1, XBOOLEAN,
MARGREL1, FINSEQ_1, CARD_1, STRUCT_0, MODELC_1, RELSET_1, FUNCT_2;
requirements REAL, NUMERALS, ARITHM, SUBSET, BOOLE;
definitions TARSKI;
equalities BINOP_1, XBOOLEAN, ROBBINS1, LATTICES;
expansions TARSKI;
theorems XBOOLE_0, ZFMISC_1, XBOOLE_1, TARSKI, FUNCT_1, FUNCT_2, NAT_1,
XREAL_1, FINSEQ_1, FUNCOP_1, XXREAL_0, FINSEQ_5, XBOOLEAN, MODELC_1,
ORDINAL1;
schemes NAT_1, FUNCT_2, XBOOLE_0, BINOP_1, BINOP_2, MODELC_1, XFAMILY;
begin
definition
let x be object;
func CastNat(x) -> Nat equals
:Def1:
x if x is Nat otherwise 0;
correctness;
end;
::************
:: definition of LTL(Linear Temporal Logic) language.
:: refer to (reuse) construction & proof of ZF_LANG
::************
Lm1: for m,n,k be Nat st m < n & n <= k+1 holds m <= k
proof
let m,n,k be Nat;
assume that
A1: m < n and
A2: n <= k+1;
m+1 <= n by A1,NAT_1:13;
then m+1<=k+1 by A2,XXREAL_0:2;
hence thesis by XREAL_1:6;
end;
reserve k,n,m for Nat,
a,x,X,Y for set,
D,D1,D2,S for non empty set,
p,q for FinSequence of NAT;
:: The operations to make LTL-formulae
definition
let n;
func atom.n -> FinSequence of NAT equals
<* (6 + n) *>;
coherence
proof
reconsider 6n=6+n as Element of NAT by ORDINAL1:def 12;
<*6n*> is FinSequence of NAT;
hence thesis;
end;
end;
definition
let p;
func 'not' p -> FinSequence of NAT equals
<*0*>^p;
coherence;
let q;
func p '&' q -> FinSequence of NAT equals
<*1*>^p^q;
coherence;
func p 'or' q -> FinSequence of NAT equals
<*2*>^p^q;
coherence;
end;
definition
let p;
func 'X' p -> FinSequence of NAT equals
<*3*>^p;
coherence;
let q;
func p 'U' q -> FinSequence of NAT equals
<*4*>^p^q;
coherence;
func p 'R' q -> FinSequence of NAT equals
<*5*>^p^q;
coherence;
end;
Lm2: len(<*n*>^p^q) = 1+len(p)+len(q)
proof
len(p^q) = len(p)+len(q) by FINSEQ_1:22;
then
A1: len(<*n*>)+len(p^q) = len(<*n*>)+len(p)+len(q);
len(<*n*>^p^q) = len(<*n*>^(p^q)) by FINSEQ_1:32
.= len(<*n*>)+len(p^q) by FINSEQ_1:22;
hence thesis by A1,FINSEQ_1:40;
end;
:: The set of all well formed formulae of LTL-language
definition
func LTL_WFF -> non empty set means
:Def9:
(for a st a in it holds a is
FinSequence of NAT ) & (for n holds atom.n in it ) & (for p st p in it holds
'not' p in it ) & (for p,q st p in it & q in it holds p '&' q in it ) & (for p,
q st p in it & q in it holds p 'or' q in it ) & (for p st p in it holds 'X' p
in it ) & (for p,q st p in it & q in it holds p 'U' q in it ) & (for p,q st p
in it & q in it holds p 'R' q in it ) & for D st (for a st a in D holds a is
FinSequence of NAT ) & (for n holds atom.n in D ) & (for p st p in D holds
'not' p in D ) & (for p,q st p in D & q in D holds p '&' q in D ) & (for p,q st
p in D & q in D holds p 'or' q in D ) & (for p st p in D holds 'X' p in D ) & (
for p,q st p in D & q in D holds p 'U' q in D ) & (for p,q st p in D & q in D
holds p 'R' q in D ) holds it c= D;
existence
proof
defpred P[set] means (for a st a in $1 holds a is FinSequence of NAT ) & (
for n holds atom.n in $1 ) & (for p st p in $1 holds 'not' p in $1 ) & (for p,q
st p in $1 & q in $1 holds p '&' q in $1 ) & (for p,q st p in $1 & q in $1
holds p 'or' q in $1 ) & (for p st p in $1 holds 'X' p in $1 ) & (for p,q st p
in $1 & q in $1 holds p 'U' q in $1 ) & (for p,q st p in $1 & q in $1 holds p
'R' q in $1 );
defpred Q[object] means for D st P[D] holds $1 in D;
consider Y such that
A1: for a being object holds a in Y iff a in NAT* & Q[a] from XBOOLE_0:sch 1;
now
set a = atom.0;
take b = a;
a in NAT* & for D st P[D] holds a in D by FINSEQ_1:def 11;
hence b in Y by A1;
end;
then reconsider Y as non empty set;
take Y;
thus a in Y implies a is FinSequence of NAT
proof
assume a in Y;
then a in NAT* by A1;
hence thesis by FINSEQ_1:def 11;
end;
thus atom.n in Y
proof
atom.n in NAT* & for D st P[D] holds atom.n in D by FINSEQ_1:def 11;
hence thesis by A1;
end;
thus p in Y implies 'not' p in Y
proof
assume
A2: p in Y;
A3: for D st P[D] holds 'not' p in D
proof
let D;
assume
A4: P[D];
then p in D by A1,A2;
hence thesis by A4;
end;
'not' p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A3;
end;
thus for q,p holds q in Y & p in Y implies q '&' p in Y
proof
let q,p;
assume
A5: q in Y & p in Y;
A6: for D st P[D] holds q '&' p in D
proof
let D;
assume
A7: P[D];
then p in D & q in D by A1,A5;
hence thesis by A7;
end;
q '&' p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A6;
end;
thus for q,p holds q in Y & p in Y implies q 'or' p in Y
proof
let q,p;
assume
A8: q in Y & p in Y;
A9: for D st P[D] holds q 'or' p in D
proof
let D;
assume
A10: P[D];
then p in D & q in D by A1,A8;
hence thesis by A10;
end;
q 'or' p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A9;
end;
thus p in Y implies 'X' p in Y
proof
assume
A11: p in Y;
A12: for D st P[D] holds 'X' p in D
proof
let D;
assume
A13: P[D];
then p in D by A1,A11;
hence thesis by A13;
end;
'X' p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A12;
end;
thus for q,p holds q in Y & p in Y implies q 'U' p in Y
proof
let q,p;
assume
A14: q in Y & p in Y;
A15: for D st P[D] holds q 'U' p in D
proof
let D;
assume
A16: P[D];
then p in D & q in D by A1,A14;
hence thesis by A16;
end;
q 'U' p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A15;
end;
thus for q,p holds q in Y & p in Y implies q 'R' p in Y
proof
let q,p;
assume
A17: q in Y & p in Y;
A18: for D st P[D] holds q 'R' p in D
proof
let D;
assume
A19: P[D];
then p in D & q in D by A1,A17;
hence thesis by A19;
end;
q 'R' p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A18;
end;
let D such that
A20: P[D];
let a be object;
assume a in Y;
hence thesis by A1,A20;
end;
uniqueness
proof
let D1,D2;
assume ( ( for a st a in D1 holds a is FinSequence of NAT)& for n holds
atom.n in D1 )&( ( for p st p in D1 holds 'not' p in D1)& for p,q st p in D1 &
q in D1 holds p '&' q in D1 ) & ( ( for p,q st p in D1 & q in D1 holds p 'or' q
in D1) & for p st p in D1 holds 'X' p in D1 )&( ( for p,q st p in D1 & q in D1
holds p 'U' q in D1)& for p,q st p in D1 & q in D1 holds p 'R' q in D1 ) & ( (
for D st (for a st a in D holds a is FinSequence of NAT ) & (for n holds atom.n
in D ) & (for p st p in D holds 'not' p in D ) & (for p,q st p in D & q in D
holds p '&' q in D ) & (for p,q st p in D & q in D holds p 'or' q in D ) & (for
p st p in D holds 'X' p in D ) & (for p,q st p in D & q in D holds p 'U' q in D
) & ( for p,q st p in D & q in D holds p 'R' q in D ) holds D1 c= D)& for a st
a in D2 holds a is FinSequence of NAT )&( ( for n holds atom.n in D2)& for p st
p in D2 holds 'not' p in D2 ) & ( ( for p,q st p in D2 & q in D2 holds p '&' q
in D2 )& for p,q st p in D2 & q in D2 holds p 'or' q in D2 )&( ( for p st p in
D2 holds 'X' p in D2)& for p,q st p in D2 & q in D2 holds p 'U' q in D2 ) &( (
for p,q st p in D2 & q in D2 holds p 'R' q in D2)& for D st (for a st a in D
holds a is FinSequence of NAT ) & (for n holds atom.n in D ) & (for p st p in D
holds 'not' p in D ) & (for p,q st p in D & q in D holds p '&' q in D ) & (for
p,q st p in D & q in D holds p 'or' q in D ) & (for p st p in D holds 'X' p in
D ) & (for p,q st p in D & q in D holds p 'U' q in D ) & (for p,q st p in D & q
in D holds p 'R' q in D ) holds D2 c= D);
then D1 c= D2 & D2 c= D1;
hence thesis by XBOOLE_0:def 10;
end;
end;
definition
let IT be FinSequence of NAT;
attr IT is LTL-formula-like means
:Def10:
IT is Element of LTL_WFF;
end;
registration
cluster LTL-formula-like for FinSequence of NAT;
existence
proof
set x = the Element of LTL_WFF;
reconsider x as FinSequence of NAT by Def9;
take x;
thus x is Element of LTL_WFF;
end;
end;
definition
mode LTL-formula is LTL-formula-like FinSequence of NAT;
end;
theorem Th1:
a is LTL-formula iff a in LTL_WFF
proof
thus a is LTL-formula implies a in LTL_WFF
proof
assume a is LTL-formula;
then a is Element of LTL_WFF by Def10;
hence thesis;
end;
assume a in LTL_WFF;
hence thesis by Def9,Def10;
end;
reserve F,F1,G,G1,H,H1,H2 for LTL-formula;
registration
let n;
cluster atom.n -> LTL-formula-like;
coherence
by Def9;
end;
registration
let H;
cluster 'not' H -> LTL-formula-like;
coherence
proof
H is Element of LTL_WFF by Def10;
then 'not' H is Element of LTL_WFF by Def9;
hence thesis;
end;
cluster 'X' H -> LTL-formula-like;
coherence
proof
H is Element of LTL_WFF by Def10;
then 'X' H is Element of LTL_WFF by Def9;
hence thesis;
end;
let G;
cluster H '&' G -> LTL-formula-like;
coherence
proof
H is Element of LTL_WFF & G is Element of LTL_WFF by Def10;
then H '&' G is Element of LTL_WFF by Def9;
hence thesis;
end;
cluster H 'or' G -> LTL-formula-like;
coherence
proof
H is Element of LTL_WFF & G is Element of LTL_WFF by Def10;
then H 'or' G is Element of LTL_WFF by Def9;
hence thesis;
end;
cluster H 'U' G -> LTL-formula-like;
coherence
proof
H is Element of LTL_WFF & G is Element of LTL_WFF by Def10;
then H 'U' G is Element of LTL_WFF by Def9;
hence thesis;
end;
cluster H 'R' G -> LTL-formula-like;
coherence
proof
H is Element of LTL_WFF & G is Element of LTL_WFF by Def10;
then H 'R' G is Element of LTL_WFF by Def9;
hence thesis;
end;
end;
definition
let H;
attr H is atomic means
ex n st H = atom.n;
attr H is negative means
ex H1 st H = 'not' H1;
attr H is conjunctive means
ex F,G st H = F '&' G;
attr H is disjunctive means
ex F,G st H = F 'or' G;
attr H is next means
ex H1 st H = 'X' H1;
attr H is Until means
ex F,G st H = F 'U' G;
attr H is Release means
ex F,G st H = F 'R' G;
end;
theorem Th2:
H is atomic or H is negative or H is conjunctive or H is
disjunctive or H is next or H is Until or H is Release
proof
A1: H is Element of LTL_WFF by Def10;
assume
A2: not thesis;
then atom.0 <> H;
then
A3: not atom.0 in { H } by TARSKI:def 1;
A4: now
let p,q;
assume
A5: p in LTL_WFF \ { H } & q in LTL_WFF \ { H };
then reconsider F = p, G = q as LTL-formula by Def10;
F 'R' G <> H by A2;
then
A6: not p 'R' q in { H } by TARSKI:def 1;
p 'R' q in LTL_WFF by A5,Def9;
hence p 'R' q in LTL_WFF \ { H } by A6,XBOOLE_0:def 5;
end;
A7: now
let p,q;
assume
A8: p in LTL_WFF \ { H } & q in LTL_WFF \ { H };
then reconsider F = p, G = q as LTL-formula by Def10;
F 'U' G <> H by A2;
then
A9: not p 'U' q in { H } by TARSKI:def 1;
p 'U' q in LTL_WFF by A8,Def9;
hence p 'U' q in LTL_WFF \ { H } by A9,XBOOLE_0:def 5;
end;
A10: now
let p;
assume
A11: p in LTL_WFF \ { H };
then reconsider H1 = p as LTL-formula by Def10;
'X' H1 <> H by A2;
then
A12: not 'X' p in { H } by TARSKI:def 1;
'X' p in LTL_WFF by A11,Def9;
hence 'X' p in LTL_WFF \ { H } by A12,XBOOLE_0:def 5;
end;
A13: now
let p,q;
assume
A14: p in LTL_WFF \ { H } & q in LTL_WFF \ { H };
then reconsider F = p, G = q as LTL-formula by Def10;
F 'or' G <> H by A2;
then
A15: not p 'or' q in { H } by TARSKI:def 1;
p 'or' q in LTL_WFF by A14,Def9;
hence p 'or' q in LTL_WFF \ { H } by A15,XBOOLE_0:def 5;
end;
A16: now
let p,q;
assume
A17: p in LTL_WFF \ { H } & q in LTL_WFF \ { H };
then reconsider F = p, G = q as LTL-formula by Def10;
F '&' G <> H by A2;
then
A18: not p '&' q in { H } by TARSKI:def 1;
p '&' q in LTL_WFF by A17,Def9;
hence p '&' q in LTL_WFF \ { H } by A18,XBOOLE_0:def 5;
end;
A19: now
let p;
assume
A20: p in LTL_WFF \ { H };
then reconsider H1 = p as LTL-formula by Def10;
'not' H1 <> H by A2;
then
A21: not 'not' p in { H } by TARSKI:def 1;
'not' p in LTL_WFF by A20,Def9;
hence 'not' p in LTL_WFF \ { H } by A21,XBOOLE_0:def 5;
end;
A22: now
let n;
atom.n <> H by A2;
then
A23: not atom.n in { H } by TARSKI:def 1;
atom.n in LTL_WFF by Def9;
hence atom.n in LTL_WFF \ { H } by A23,XBOOLE_0:def 5;
end;
atom.0 in LTL_WFF by Def9;
then
A24: LTL_WFF \ { H } is non empty by A3,XBOOLE_0:def 5;
for a st a in LTL_WFF \ { H } holds a is FinSequence of NAT by Def9;
then LTL_WFF c= LTL_WFF \ { H } by A24,A22,A19,A16,A13,A10,A7,A4,Def9;
then H in LTL_WFF \ { H } by A1;
then not H in { H } by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
Lm3: H is negative implies H.1 = 0
by FINSEQ_1:41;
Lm4: H is conjunctive implies H.1 = 1
proof
assume H is conjunctive;
then consider F,G such that
A1: H = F '&' G;
<*1*>^F^G = <*1*>^(F^G) by FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
Lm5: H is disjunctive implies H.1 = 2
proof
assume H is disjunctive;
then consider F,G such that
A1: H = F 'or' G;
<*2*>^F^G = <*2*>^(F^G) by FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
Lm6: H is next implies H.1 = 3
by FINSEQ_1:41;
Lm7: H is Until implies H.1 = 4
proof
assume H is Until;
then consider F,G such that
A1: H = F 'U' G;
<*4*>^F^G = <*4*>^(F^G) by FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
Lm8: H is Release implies H.1 = 5
proof
assume H is Release;
then consider F,G such that
A1: H = F 'R' G;
<*5*>^F^G = <*5*>^(F^G) by FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
Lm9: H is atomic implies not H.1 = 0 & not H.1 = 1 & not H.1 = 2 & not H.1 = 3
& not H.1 = 4 & not H.1 = 5
proof
assume H is atomic;
then consider n such that
A1: H = atom.n;
A3: 5+0<5+(1+n) by XREAL_1:8;
thus thesis by A1,A3;
end;
Lm10: H is atomic & H.1 <> 0 & H.1 <> 1 & H.1 <> 2 & H.1 <> 3 & H.1 <> 4 & H.1
<> 5 or H is negative & H.1 = 0 or H is conjunctive & H.1 = 1 or H is
disjunctive & H.1 = 2 or H is next & H.1 = 3 or H is Until & H.1 = 4 or H is
Release & H.1 = 5
proof
per cases by Th2;
case
H is atomic;
hence thesis by Lm9;
end;
case
H is negative;
hence thesis by Lm3;
end;
case
H is conjunctive;
hence thesis by Lm4;
end;
case
H is disjunctive;
hence thesis by Lm5;
end;
case
H is next;
hence thesis by Lm6;
end;
case
H is Until;
hence thesis by Lm7;
end;
case
H is Release;
hence thesis by Lm8;
end;
end;
theorem Th3:
1<= len H
proof
per cases by Th2;
suppose
H is atomic;
then ex n st H = atom.n;
hence thesis by FINSEQ_1:40;
end;
suppose
H is negative;
then consider H1 such that
A1: H = 'not' H1;
len(H) = 1+len(H1) by A1,FINSEQ_5:8;
hence thesis by NAT_1:11;
end;
suppose
H is conjunctive;
then consider F,G such that
A2: H = F '&' G;
A3: 1 <= 1+len(F) & 1+len(F) <= 1+len(F)+len(G) by NAT_1:11;
len(H) = 1+len(F)+len(G) by A2,Lm2;
hence thesis by A3,XXREAL_0:2;
end;
suppose
H is disjunctive;
then consider F,G such that
A4: H = F 'or' G;
A5: 1 <= 1+len(F) & 1+len(F) <= 1+len(F)+len(G) by NAT_1:11;
len(H) = 1+len(F)+len(G) by A4,Lm2;
hence thesis by A5,XXREAL_0:2;
end;
suppose
H is next;
then consider H1 such that
A6: H = 'X' H1;
len(H) = 1+len(H1) by A6,FINSEQ_5:8;
hence thesis by NAT_1:11;
end;
suppose
H is Until;
then consider F,G such that
A7: H = F 'U' G;
A8: 1 <= 1+len(F) & 1+len(F) <= 1+len(F)+len(G) by NAT_1:11;
len(H) = 1+len(F)+len(G) by A7,Lm2;
hence thesis by A8,XXREAL_0:2;
end;
suppose
H is Release;
then consider F,G such that
A9: H = F 'R' G;
A10: 1 <= 1+len(F) & 1+len(F) <= 1+len(F)+len(G) by NAT_1:11;
len(H) = 1+len(F)+len(G) by A9,Lm2;
hence thesis by A10,XXREAL_0:2;
end;
end;
reserve sq,sq9 for FinSequence;
Lm11: H = F^sq implies H = F
proof
defpred P[Nat] means for H,F,sq st len H = $1 & H = F^sq holds H = F;
for n being Nat st (for k being Nat st k < n for H,F,sq st len H = k & H
= F^sq holds H = F) for H,F,sq st len H = n & H = F^sq holds H = F
proof
let n being Nat such that
A1: for k being Nat st k < n for H,F,sq st len H = k & H = F^sq holds H = F;
let H,F,sq such that
A2: len H = n and
A3: H = F^sq;
dom F = Seg len F & 1 <= len F by Th3,FINSEQ_1:def 3;
then
A4: 1 in dom F by FINSEQ_1:1;
A5: now
A6: len <*0*>= 1 by FINSEQ_1:40;
assume
A7: H is negative;
then consider H1 such that
A8: H = 'not' H1;
(F^sq).1 = 0 by A3,A7,Lm3;
then F.1 = 0 by A4,FINSEQ_1:def 7;
then F is negative by Lm10;
then consider F1 such that
A9: F = 'not' F1;
len <*0*> + len H1 = len H by A8,FINSEQ_1:22;
then
A10: len H1 < len H by A6,NAT_1:13;
<*0*>^F1^sq = <*0*>^(F1^sq) by FINSEQ_1:32;
then H1 = F1^sq by A3,A8,A9,FINSEQ_1:33;
hence thesis by A1,A2,A8,A9,A10;
end;
A11: now
assume
A12: H is Release;
then consider G1,G such that
A13: H = G1 'R' G;
A14: len G + (1 + len G1) = len G + 1 + len G1;
A15: len(<*5*>^G1) = len <*5*> + len G1 & len <*5*> = 1 by FINSEQ_1:22,40;
len(<*5*>^G1) + len G = len H by A13,FINSEQ_1:22;
then len G + 1 <= len H by A15,A14,NAT_1:11;
then
A16: len G < len H by NAT_1:13;
(F^sq).1 = 5 by A3,A12,Lm8;
then F.1 = 5 by A4,FINSEQ_1:def 7;
then F is Release by Lm10;
then consider F1,H1 such that
A17: F = F1 'R' H1;
A18: now
A19: len F1 + 1 + len H1 + len sq = len F1 + 1 + (len H1 + len sq);
given sq9 such that
A20: F1 = G1^sq9;
A21: len(F^sq) = len F + len sq & len <*5*> = 1 by FINSEQ_1:22,40;
len(<*5*>^F1) = len <*5*> + len F1 & len F = len(<*5*>^F1) + len
H1 by A17,FINSEQ_1:22;
then len F1 + 1 <= len H by A3,A21,A19,NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1,A2,A20;
end;
A22: <*5*>^F1^H1 = <*5*>^(F1^H1) & <*5*>^(F1^H1)^sq = <*5*>^(F1^H1^sq)
by FINSEQ_1:32;
A23: now
given sq9 such that
A24: G1 = F1^sq9;
A25: len <*5*> = 1 by FINSEQ_1:40;
len(<*5*>^G1) + len G = len H & len(<*5*>^G1) = len <*5*> + len
G1 by A13,FINSEQ_1:22;
then len G1 + 1 <= len H by A25,NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1,A2,A24;
end;
A26: F1^H1^sq = F1^(H1^sq) by FINSEQ_1:32;
<*5*>^G1^G = <*5*>^(G1^G) by FINSEQ_1:32;
then
A27: G1^G = F1^(H1^sq) by A3,A13,A17,A22,A26,FINSEQ_1:33;
then len F1 <= len G1 implies ex sq9 st G1 = F1^sq9 by FINSEQ_1:47;
then G = H1^sq by A27,A23,A18,FINSEQ_1:33,47;
hence thesis by A1,A2,A3,A17,A22,A26,A16;
end;
A28: now
assume
A29: H is Until;
then consider G1,G such that
A30: H = G1 'U' G;
A31: len G + (1 + len G1) = len G + 1 + len G1;
A32: len(<*4*>^G1) = len <*4*> + len G1 & len <*4*> = 1 by FINSEQ_1:22,40;
len(<*4*>^G1) + len G = len H by A30,FINSEQ_1:22;
then len G + 1 <= len H by A32,A31,NAT_1:11;
then
A33: len G < len H by NAT_1:13;
(F^sq).1 = 4 by A3,A29,Lm7;
then F.1 = 4 by A4,FINSEQ_1:def 7;
then F is Until by Lm10;
then consider F1,H1 such that
A34: F = F1 'U' H1;
A35: now
A36: len F1 + 1 + len H1 + len sq = len F1 + 1 + (len H1 + len sq);
given sq9 such that
A37: F1 = G1^sq9;
A38: len(F^sq) = len F + len sq & len <*4*> = 1 by FINSEQ_1:22,40;
len(<*4*>^F1) = len <*4*> + len F1 & len F = len(<*4*>^F1) + len
H1 by A34,FINSEQ_1:22;
then len F1 + 1 <= len H by A3,A38,A36,NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1,A2,A37;
end;
A39: <*4*>^F1^H1 = <*4*>^(F1^H1) & <*4*>^(F1^H1)^sq = <*4*>^(F1^H1^sq)
by FINSEQ_1:32;
A40: now
given sq9 such that
A41: G1 = F1^sq9;
A42: len <*4*> = 1 by FINSEQ_1:40;
len(<*4*>^G1) + len G = len H & len(<*4*>^G1) = len <*4*> + len
G1 by A30,FINSEQ_1:22;
then len G1 + 1 <= len H by A42,NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1,A2,A41;
end;
A43: F1^H1^sq = F1^(H1^sq) by FINSEQ_1:32;
<*4*>^G1^G = <*4*>^(G1^G) by FINSEQ_1:32;
then
A44: G1^G = F1^(H1^sq) by A3,A30,A34,A39,A43,FINSEQ_1:33;
then len F1 <= len G1 implies ex sq9 st G1 = F1^sq9 by FINSEQ_1:47;
then G = H1^sq by A44,A40,A35,FINSEQ_1:33,47;
hence thesis by A1,A2,A3,A34,A39,A43,A33;
end;
A45: now
assume
A46: H is disjunctive;
then consider G1,G such that
A47: H = G1 'or' G;
A48: len G + (1 + len G1) = len G + 1 + len G1;
A49: len(<*2*>^G1) = len <*2*> + len G1 & len <*2*> = 1 by FINSEQ_1:22,40;
len(<*2*>^G1) + len G = len H by A47,FINSEQ_1:22;
then len G + 1 <= len H by A49,A48,NAT_1:11;
then
A50: len G < len H by NAT_1:13;
(F^sq).1 = 2 by A3,A46,Lm5;
then F.1 = 2 by A4,FINSEQ_1:def 7;
then F is disjunctive by Lm10;
then consider F1,H1 such that
A51: F = F1 'or' H1;
A52: now
A53: len F1 + 1 + len H1 + len sq = len F1 + 1 + (len H1 + len sq);
given sq9 such that
A54: F1 = G1^sq9;
A55: len(F^sq) = len F + len sq & len <*2*> = 1 by FINSEQ_1:22,40;
len(<*2*>^F1) = len <*2*> + len F1 & len F = len(<*2*>^F1) + len
H1 by A51,FINSEQ_1:22;
then len F1 + 1 <= len H by A3,A55,A53,NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1,A2,A54;
end;
A56: <*2*>^F1^H1 = <*2*>^(F1^H1) & <*2*>^(F1^H1)^sq = <*2*>^(F1^H1^sq)
by FINSEQ_1:32;
A57: now
given sq9 such that
A58: G1 = F1^sq9;
A59: len <*2*> = 1 by FINSEQ_1:40;
len(<*2*>^G1) + len G = len H & len(<*2*>^G1) = len <*2*> + len
G1 by A47,FINSEQ_1:22;
then len G1 + 1 <= len H by A59,NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1,A2,A58;
end;
A60: F1^H1^sq = F1^(H1^sq) by FINSEQ_1:32;
<*2*>^G1^G = <*2*>^(G1^G) by FINSEQ_1:32;
then
A61: G1^G = F1^(H1^sq) by A3,A47,A51,A56,A60,FINSEQ_1:33;
then len F1 <= len G1 implies ex sq9 st G1 = F1^sq9 by FINSEQ_1:47;
then G = H1^sq by A61,A57,A52,FINSEQ_1:33,47;
hence thesis by A1,A2,A3,A51,A56,A60,A50;
end;
A62: now
assume
A63: H is conjunctive;
then consider G1,G such that
A64: H = G1 '&' G;
A65: len G + (1 + len G1) = len G + 1 + len G1;
A66: len(<*1*>^G1) = len <*1*> + len G1 & len <*1*> = 1 by FINSEQ_1:22,40;
len(<*1*>^G1) + len G = len H by A64,FINSEQ_1:22;
then len G + 1 <= len H by A66,A65,NAT_1:11;
then
A67: len G < len H by NAT_1:13;
(F^sq).1 = 1 by A3,A63,Lm4;
then F.1 = 1 by A4,FINSEQ_1:def 7;
then F is conjunctive by Lm10;
then consider F1,H1 such that
A68: F = F1 '&' H1;
A69: now
A70: len F1 + 1 + len H1 + len sq = len F1 + 1 + (len H1 + len sq);
given sq9 such that
A71: F1 = G1^sq9;
A72: len(F^sq) = len F + len sq & len <*1*> = 1 by FINSEQ_1:22,40;
len(<*1*>^F1) = len <*1*> + len F1 & len F = len(<*1*>^F1) + len
H1 by A68,FINSEQ_1:22;
then len F1 + 1 <= len H by A3,A72,A70,NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1,A2,A71;
end;
A73: <*1*>^F1^H1 = <*1*>^(F1^H1) & <*1*>^(F1^H1)^sq = <*1*>^(F1^H1^sq)
by FINSEQ_1:32;
A74: now
given sq9 such that
A75: G1 = F1^sq9;
A76: len <*1*> = 1 by FINSEQ_1:40;
len(<*1*>^G1) + len G = len H & len(<*1*>^G1) = len <*1*> + len
G1 by A64,FINSEQ_1:22;
then len G1 + 1 <= len H by A76,NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1,A2,A75;
end;
A77: F1^H1^sq = F1^(H1^sq) by FINSEQ_1:32;
<*1*>^G1^G = <*1*>^(G1^G) by FINSEQ_1:32;
then
A78: G1^G = F1^(H1^sq) by A3,A64,A68,A73,A77,FINSEQ_1:33;
then len F1 <= len G1 implies ex sq9 st G1 = F1^sq9 by FINSEQ_1:47;
then G = H1^sq by A78,A74,A69,FINSEQ_1:33,47;
hence thesis by A1,A2,A3,A68,A73,A77,A67;
end;
A79: now
A80: len <*3*>= 1 by FINSEQ_1:40;
assume
A81: H is next;
then consider H1 such that
A82: H = 'X' H1;
(F^sq).1 = 3 by A3,A81,Lm6;
then F.1 = 3 by A4,FINSEQ_1:def 7;
then F is next by Lm10;
then consider F1 such that
A83: F = 'X' F1;
len <*3*> + len H1 = len H by A82,FINSEQ_1:22;
then
A84: len H1 < len H by A80,NAT_1:13;
<*3*>^F1^sq = <*3*>^(F1^sq) by FINSEQ_1:32;
then H1 = F1^sq by A3,A82,A83,FINSEQ_1:33;
hence thesis by A1,A2,A82,A83,A84;
end;
A85: len F + len sq = len(F^sq) by FINSEQ_1:22;
now
A86: 1 <= len F by Th3;
assume H is atomic;
then ex k st H = atom.k;
then
A87: len(H) = 1 by FINSEQ_1:40;
then len F <= 1 by A3,A85,NAT_1:11;
then 1 + len sq = 1 + 0 by A3,A85,A87,A86,XXREAL_0:1;
then sq = {};
hence thesis by A3,FINSEQ_1:34;
end;
hence thesis by A5,A62,A45,A79,A28,A11,Th2;
end;
then
A88: for k being Nat st for n being Nat st n < k holds P[n] holds P[k];
A89: for n being Nat holds P[n] from NAT_1:sch 4(A88);
len H = len H;
hence thesis by A89;
end;
Lm12: H '&' G = H1 '&' G1 implies H = H1 & G = G1
proof
assume
A1: H '&' G = H1 '&' G1;
<*1*>^H^G = <*1*>^(H^G) & <*1*>^H1^G1 = <*1*>^(H1^G1) by FINSEQ_1:32;
then
A2: H^G = H1^G1 by A1,FINSEQ_1:33;
then
A3: len H1 <= len H implies ex sq st H = H1^sq by FINSEQ_1:47;
A4: len H <= len H1 implies ex sq st H1 = H^sq by A2,FINSEQ_1:47;
hence H = H1 by A3,Lm11;
(ex sq st H1 = H^sq) implies H1 = H by Lm11;
hence thesis by A1,A3,A4,Lm11,FINSEQ_1:33;
end;
Lm13: H 'or' G = H1 'or' G1 implies H = H1 & G = G1
proof
assume
A1: H 'or' G = H1 'or' G1;
<*2*>^H^G = <*2*>^(H^G) & <*2*>^H1^G1 = <*2*>^(H1^G1) by FINSEQ_1:32;
then
A2: H^G = H1^G1 by A1,FINSEQ_1:33;
then
A3: len H1 <= len H implies ex sq st H = H1^sq by FINSEQ_1:47;
A4: len H <= len H1 implies ex sq st H1 = H^sq by A2,FINSEQ_1:47;
hence H = H1 by A3,Lm11;
(ex sq st H1 = H^sq) implies H1 = H by Lm11;
hence thesis by A1,A3,A4,Lm11,FINSEQ_1:33;
end;
Lm14: H 'U' G = H1 'U' G1 implies H = H1 & G = G1
proof
assume
A1: H 'U' G = H1 'U' G1;
<*4*>^H^G = <*4*>^(H^G) & <*4*>^H1^G1 = <*4*>^(H1^G1) by FINSEQ_1:32;
then
A2: H^G = H1^G1 by A1,FINSEQ_1:33;
then
A3: len H1 <= len H implies ex sq st H = H1^sq by FINSEQ_1:47;
A4: len H <= len H1 implies ex sq st H1 = H^sq by A2,FINSEQ_1:47;
hence H = H1 by A3,Lm11;
(ex sq st H1 = H^sq) implies H1 = H by Lm11;
hence thesis by A1,A3,A4,Lm11,FINSEQ_1:33;
end;
Lm15: H 'R' G = H1 'R' G1 implies H = H1 & G = G1
proof
assume
A1: H 'R' G = H1 'R' G1;
<*5*>^H^G = <*5*>^(H^G) & <*5*>^H1^G1 = <*5*>^(H1^G1) by FINSEQ_1:32;
then
A2: H^G = H1^G1 by A1,FINSEQ_1:33;
then
A3: len H1 <= len H implies ex sq st H = H1^sq by FINSEQ_1:47;
A4: len H <= len H1 implies ex sq st H1 = H^sq by A2,FINSEQ_1:47;
hence H = H1 by A3,Lm11;
(ex sq st H1 = H^sq) implies H1 = H by Lm11;
hence thesis by A1,A3,A4,Lm11,FINSEQ_1:33;
end;
Lm16: H is negative implies (not H is atomic) & (not H is conjunctive) & (not
H is disjunctive) & (not H is next) & (not H is Until) & not H is Release
proof
assume H is negative;
then H.1=0 by Lm3;
hence thesis by Lm4,Lm5,Lm6,Lm7,Lm8;
end;
Lm17: H is conjunctive implies (not H is atomic) & (not H is negative) & (not
H is disjunctive) & (not H is next) & (not H is Until) & not H is Release
proof
assume H is conjunctive;
then H.1=1 by Lm4;
hence thesis by Lm3,Lm5,Lm6,Lm7,Lm8,Lm9;
end;
Lm18: H is disjunctive implies (not H is atomic) & (not H is negative) & (not
H is conjunctive) & (not H is next) & (not H is Until) & not H is Release
proof
assume H is disjunctive;
then H.1=2 by Lm5;
hence thesis by Lm3,Lm4,Lm6,Lm7,Lm8,Lm9;
end;
Lm19: H is next implies (not H is atomic) & (not H is negative) & (not H is
conjunctive) & (not H is disjunctive) & (not H is Until) & not H is Release
proof
assume H is next;
then H.1=3 by Lm6;
hence thesis by Lm3,Lm4,Lm5,Lm7,Lm8,Lm9;
end;
Lm20: H is Until implies (not H is atomic) & (not H is negative) & (not H is
conjunctive) & (not H is disjunctive) & (not H is next) & not H is Release
proof
assume H is Until;
then H.1=4 by Lm7;
hence thesis by Lm3,Lm4,Lm5,Lm6,Lm8,Lm9;
end;
Lm21: H is Release implies (not H is atomic) & (not H is negative) & (not H is
conjunctive) & (not H is disjunctive) & (not H is next) & not H is Until
proof
assume H is Release;
then H.1=5 by Lm8;
hence thesis by Lm3,Lm4,Lm5,Lm6,Lm7,Lm9;
end;
definition
let H;
assume
A1: H is negative or H is next;
func the_argument_of H -> LTL-formula means
:Def18:
'not' it = H if H is negative otherwise 'X' it = H;
existence by A1;
uniqueness by FINSEQ_1:33;
consistency;
end;
definition
let H;
assume
A1: H is conjunctive or H is disjunctive or H is Until or H is Release;
func the_left_argument_of H -> LTL-formula means
:Def19:
ex H1 st it '&' H1
= H if H is conjunctive, ex H1 st it 'or' H1 = H if H is disjunctive, ex H1 st
it 'U' H1 = H if H is Until otherwise ex H1 st it 'R' H1 = H;
existence by A1;
uniqueness by Lm12,Lm13,Lm14,Lm15;
consistency by Lm17,Lm18;
func the_right_argument_of H -> LTL-formula means
:Def20:
ex H1 st H1 '&' it
= H if H is conjunctive, ex H1 st H1 'or' it = H if H is disjunctive, ex H1 st
H1 'U' it = H if H is Until otherwise ex H1 st H1 'R' it = H;
existence
by A1;
uniqueness by Lm12,Lm13,Lm14,Lm15;
consistency by Lm18,Lm20;
end;
theorem
H is negative implies H = 'not' the_argument_of H by Def18;
theorem Th5:
H is next implies H = 'X' the_argument_of H
proof
assume
A1: H is next;
then not H is negative by Lm19;
hence thesis by A1,Def18;
end;
theorem Th6:
H is conjunctive implies H =(the_left_argument_of H) '&' (
the_right_argument_of H)
proof
assume
A1: H is conjunctive;
then ex H1 st H = H1 '&' the_right_argument_of H by Def20;
hence thesis by A1,Def19;
end;
theorem Th7:
H is disjunctive implies H =(the_left_argument_of H) 'or' (
the_right_argument_of H)
proof
assume
A1: H is disjunctive;
then ex H1 st H = H1 'or' the_right_argument_of H by Def20;
hence thesis by A1,Def19;
end;
theorem Th8:
H is Until implies H = (the_left_argument_of H) 'U' (
the_right_argument_of H)
proof
assume
A1: H is Until;
then ex H1 st H = H1 'U' the_right_argument_of H by Def20;
hence thesis by A1,Def19;
end;
theorem Th9:
H is Release implies H = (the_left_argument_of H) 'R' (
the_right_argument_of H)
proof
assume
A1: H is Release;
then
A2: not H is Until by Lm21;
A3: ( not H is conjunctive)& not H is disjunctive by A1,Lm21;
then ex H1 st H = H1 'R' the_right_argument_of H by A1,A2,Def20;
hence thesis by A1,A3,A2,Def19;
end;
theorem Th10:
H is negative or H is next implies len(H) = 1+len(
the_argument_of H) & len(the_argument_of H) < len(H)
proof
assume
A1: H is negative or H is next;
per cases by A1;
suppose
H is negative;
then H = 'not' the_argument_of H by Def18;
then len(H) = 1+len(the_argument_of H) by FINSEQ_5:8;
hence thesis by NAT_1:19;
end;
suppose
H is next;
then H = 'X' the_argument_of H by Th5;
then len(H) = 1+len(the_argument_of H) by FINSEQ_5:8;
hence thesis by NAT_1:19;
end;
end;
theorem Th11:
H is conjunctive or H is disjunctive or H is Until or H is
Release implies len(H) =1+ len(the_left_argument_of H)+len(
the_right_argument_of H) & len(the_left_argument_of H) < len(H) & len(
the_right_argument_of H) < len(H)
proof
set iL=len(the_left_argument_of H);
set iR=len(the_right_argument_of H);
set iR1=iR+1;
assume
A1: H is conjunctive or H is disjunctive or H is Until or H is Release;
per cases by A1;
suppose
H is conjunctive;
then H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th6;
then
A2: len(H) = 1+iL+iR by Lm2;
1<=iR1 by NAT_1:11;
then
A3: iL < iL +iR1 by NAT_1:19;
1<=1+iL by NAT_1:11;
hence thesis by A2,A3,NAT_1:19;
end;
suppose
H is disjunctive;
then H = (the_left_argument_of H) 'or' (the_right_argument_of H) by Th7;
then
A4: len(H) = 1+iL+iR by Lm2;
1<=iR1 by NAT_1:11;
then
A5: iL < iL +iR1 by NAT_1:19;
1<=1+iL by NAT_1:11;
hence thesis by A4,A5,NAT_1:19;
end;
suppose
H is Until;
then H = the_left_argument_of H 'U' the_right_argument_of H by Th8;
then
A6: len(H) = 1+iL+iR by Lm2;
1<=iR1 by NAT_1:11;
then
A7: iL < iL +iR1 by NAT_1:19;
1<=1+iL by NAT_1:11;
hence thesis by A6,A7,NAT_1:19;
end;
suppose
H is Release;
then H = the_left_argument_of H 'R' the_right_argument_of H by Th9;
then
A8: len(H) = 1+iL+iR by Lm2;
1<=iR1 by NAT_1:11;
then
A9: iL < iL +iR1 by NAT_1:19;
1<=1+iL by NAT_1:11;
hence thesis by A8,A9,NAT_1:19;
end;
end;
::
:: The Immediate Constituents of LTL-formulae
::
definition
let H,F;
pred H is_immediate_constituent_of F means
F = 'not' H or F = 'X' H
or ex H1 st F = H '&' H1 or F = H1 '&' H or F = H 'or' H1 or F = H1 'or' H or F
= H 'U' H1 or F = H1 'U' H or F = H 'R' H1 or F = H1 'R' H;
end;
theorem Th12:
for F,G holds ('not' F).1 = 0 & (F '&' G).1 = 1 & (F 'or' G).1 =
2 & ('X' F).1 = 3 & (F 'U' G).1 = 4 & (F 'R' G).1 = 5
proof
let F,G;
thus ('not' F).1 = 0 by FINSEQ_1:41;
thus (F '&' G).1 = (<*1*>^(F^G)).1 by FINSEQ_1:32
.= 1 by FINSEQ_1:41;
thus (F 'or' G).1 = (<*2*>^(F^G)).1 by FINSEQ_1:32
.= 2 by FINSEQ_1:41;
thus ('X' F).1 = 3 by FINSEQ_1:41;
thus (F 'U' G).1 = (<*4*>^(F^G)).1 by FINSEQ_1:32
.= 4 by FINSEQ_1:41;
thus (F 'R' G).1 = (<*5*>^(F^G)).1 by FINSEQ_1:32
.= 5 by FINSEQ_1:41;
end;
theorem Th13:
H is_immediate_constituent_of 'not' F iff H = F
proof
thus H is_immediate_constituent_of 'not' F implies H = F
proof
A1: now
given H1 such that
A2: 'not' F = H '&' H1 or 'not' F = H1 '&' H or 'not' F = H 'or' H1
or 'not' F = H1 'or' H or 'not' F = H 'U' H1 or 'not' F = H1 'U' H or 'not' F =
H 'R' H1 or 'not' F = H1 'R' H;
('not' F).1 = 0 by Th12;
hence contradiction by A2,Th12;
end;
A3: now
assume
A4: 'not' F = 'X' H;
('not' F).1 = 0 by Th12;
hence contradiction by A4,Th12;
end;
assume H is_immediate_constituent_of 'not' F;
then
'not' F = 'not' H or 'not' F = 'X' H or ex H1 st 'not' F = H '&' H1 or
'not' F = H1 '&' H or 'not' F = H 'or' H1 or 'not' F = H1 'or' H or 'not' F = H
'U' H1 or 'not' F = H1 'U' H or 'not' F = H 'R' H1 or 'not' F = H1 'R' H;
hence thesis by A3,A1,FINSEQ_1:33;
end;
thus thesis;
end;
theorem Th14:
H is_immediate_constituent_of 'X' F iff H = F
proof
thus H is_immediate_constituent_of 'X' F implies H = F
proof
A1: now
given H1 such that
A2: 'X' F = H '&' H1 or 'X' F = H1 '&' H or 'X' F = H 'or' H1 or 'X'
F = H1 'or' H or 'X' F = H 'U' H1 or 'X' F = H1 'U' H or 'X' F = H 'R' H1 or
'X' F = H1 'R' H;
('X' F).1 = 3 by Th12;
hence contradiction by A2,Th12;
end;
A3: now
assume
A4: 'X' F = 'not' H;
('X' F).1 = 3 by Th12;
hence contradiction by A4,Th12;
end;
assume H is_immediate_constituent_of 'X' F;
then
'X' F = 'not' H or 'X' F = 'X' H or ex H1 st 'X' F = H '&' H1 or 'X' F
= H1 '&' H or 'X' F = H 'or' H1 or 'X' F = H1 'or' H or 'X' F = H 'U' H1 or 'X'
F = H1 'U' H or 'X' F = H 'R' H1 or 'X' F = H1 'R' H;
hence thesis by A3,A1,FINSEQ_1:33;
end;
thus thesis;
end;
theorem Th15:
H is_immediate_constituent_of F '&' G iff H = F or H =G
proof
thus H is_immediate_constituent_of F '&' G implies H = F or H =G
proof
set Z= F '&' G;
A1: now
assume
A2: Z = 'not' H or Z = 'X' H;
Z.1 = 1 by Th12;
hence contradiction by A2,Th12;
end;
A3: now
given H1 such that
A4: Z = H 'or' H1 or Z = H1 'or' H or Z = H 'U' H1 or Z = H1 'U' H
or Z = H 'R' H1 or Z = H1 'R' H;
Z.1 = 1 by Th12;
hence contradiction by A4,Th12;
end;
assume H is_immediate_constituent_of F '&' G;
then
Z = 'not' H or Z = 'X' H or ex H1 st Z = H '&' H1 or Z = H1 '&' H or Z
= H 'or' H1 or Z = H1 'or' H or Z = H 'U' H1 or Z = H1 'U' H or Z = H 'R' H1 or
Z = H1 'R' H;
hence thesis by A1,A3,Lm12;
end;
thus thesis;
end;
theorem Th16:
H is_immediate_constituent_of F 'or' G iff H = F or H =G
proof
thus H is_immediate_constituent_of F 'or' G implies H = F or H =G
proof
set Z= F 'or' G;
A1: now
assume
A2: Z = 'not' H or Z = 'X' H;
Z.1 = 2 by Th12;
hence contradiction by A2,Th12;
end;
A3: now
given H1 such that
A4: Z = H '&' H1 or Z = H1 '&' H or Z = H 'U' H1 or Z = H1 'U' H or
Z = H 'R' H1 or Z = H1 'R' H;
Z.1 = 2 by Th12;
hence contradiction by A4,Th12;
end;
assume H is_immediate_constituent_of F 'or' G;
then
Z = 'not' H or Z = 'X' H or ex H1 st Z = H '&' H1 or Z = H1 '&' H or Z
= H 'or' H1 or Z = H1 'or' H or Z = H 'U' H1 or Z = H1 'U' H or Z = H 'R' H1 or
Z = H1 'R' H;
hence thesis by A1,A3,Lm13;
end;
thus thesis;
end;
theorem Th17:
H is_immediate_constituent_of F 'U' G iff H = F or H =G
proof
thus H is_immediate_constituent_of F 'U' G implies H = F or H =G
proof
set Z= F 'U' G;
A1: now
assume
A2: Z = 'not' H or Z = 'X' H;
Z.1 = 4 by Th12;
hence contradiction by A2,Th12;
end;
A3: now
given H1 such that
A4: Z = H '&' H1 or Z = H1 '&' H or Z = H 'or' H1 or Z = H1 'or' H
or Z = H 'R' H1 or Z = H1 'R' H;
Z.1 = 4 by Th12;
hence contradiction by A4,Th12;
end;
assume H is_immediate_constituent_of F 'U' G;
then
Z = 'not' H or Z = 'X' H or ex H1 st Z = H '&' H1 or Z = H1 '&' H or Z
= H 'or' H1 or Z = H1 'or' H or Z = H 'U' H1 or Z = H1 'U' H or Z = H 'R' H1 or
Z = H1 'R' H;
hence thesis by A1,A3,Lm14;
end;
thus thesis;
end;
theorem Th18:
H is_immediate_constituent_of F 'R' G iff H = F or H =G
proof
thus H is_immediate_constituent_of F 'R' G implies H = F or H =G
proof
set Z= F 'R' G;
A1: now
assume
A2: Z = 'not' H or Z = 'X' H;
Z.1 = 5 by Th12;
hence contradiction by A2,Th12;
end;
A3: now
given H1 such that
A4: Z = H '&' H1 or Z = H1 '&' H or Z = H 'or' H1 or Z = H1 'or' H
or Z = H 'U' H1 or Z = H1 'U' H;
Z.1 = 5 by Th12;
hence contradiction by A4,Th12;
end;
assume H is_immediate_constituent_of F 'R' G;
then
Z = 'not' H or Z = 'X' H or ex H1 st Z = H '&' H1 or Z = H1 '&' H or Z
= H 'or' H1 or Z = H1 'or' H or Z = H 'U' H1 or Z = H1 'U' H or Z = H 'R' H1 or
Z = H1 'R' H;
hence thesis by A1,A3,Lm15;
end;
thus thesis;
end;
theorem
F is atomic implies not H is_immediate_constituent_of F
proof
assume F is atomic;
then F.1 <> 2 & F.1 <> 3 & F.1 <> 4 & F.1 <> 5 & F.1 <> 0 & F.1 <> 1 by Lm9;
hence thesis by Th12;
end;
theorem Th20:
F is negative implies (H is_immediate_constituent_of F iff H =
the_argument_of F)
proof
assume F is negative;
then F = 'not' the_argument_of F by Def18;
hence thesis by Th13;
end;
theorem Th21:
F is next implies (H is_immediate_constituent_of F iff H = the_argument_of F)
proof
assume F is next;
then F = 'X' the_argument_of F by Th5;
hence thesis by Th14;
end;
theorem Th22:
F is conjunctive implies (H is_immediate_constituent_of F iff H
= the_left_argument_of F or H = the_right_argument_of F)
proof
assume F is conjunctive;
then F = (the_left_argument_of F) '&' (the_right_argument_of F) by Th6;
hence thesis by Th15;
end;
theorem Th23:
F is disjunctive implies (H is_immediate_constituent_of F iff H
= the_left_argument_of F or H = the_right_argument_of F)
proof
assume F is disjunctive;
then F = (the_left_argument_of F) 'or' (the_right_argument_of F) by Th7;
hence thesis by Th16;
end;
theorem Th24:
F is Until implies (H is_immediate_constituent_of F iff H =
the_left_argument_of F or H = the_right_argument_of F)
proof
assume F is Until;
then F = (the_left_argument_of F) 'U' (the_right_argument_of F) by Th8;
hence thesis by Th17;
end;
theorem Th25:
F is Release implies (H is_immediate_constituent_of F iff H =
the_left_argument_of F or H = the_right_argument_of F)
proof
assume F is Release;
then F = (the_left_argument_of F) 'R' (the_right_argument_of F) by Th9;
hence thesis by Th18;
end;
theorem
H is_immediate_constituent_of F implies F is negative or F is next or
F is conjunctive or F is disjunctive or F is Until or F is Release;
::
:: The Subformulae and The Proper Subformulae of LTL-formulae
::
reserve L,L9 for FinSequence;
definition
let H,F;
pred H is_subformula_of F means
ex n,L st 1 <= n & len L = n & L.1 = H & L.n = F &
for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 &
H1 is_immediate_constituent_of F1;
reflexivity
proof
let H be LTL-formula;
take 1 , <*H*>;
thus 1 <= 1;
thus len <*H*> = 1 by FINSEQ_1:40;
thus <*H*>.1 = H & <*H*>.1 = H;
thus thesis;
end;
end;
theorem
H is_subformula_of H;
definition
let H,F;
pred H is_proper_subformula_of F means
H is_subformula_of F & H <> F;
irreflexivity;
end;
theorem Th28:
H is_immediate_constituent_of F implies len H < len F
proof
assume
A1: H is_immediate_constituent_of F;
per cases by A1;
suppose
A2: F is negative or F is next;
then H = the_argument_of F by A1,Th20,Th21;
hence thesis by A2,Th10;
end;
suppose
A3: F is conjunctive or F is disjunctive or F is Until or F is Release;
then H = the_left_argument_of F or H = the_right_argument_of F by A1,Th22
,Th23,Th24,Th25;
hence thesis by A3,Th11;
end;
end;
theorem Th29:
H is_immediate_constituent_of F implies H is_proper_subformula_of F
proof
assume
A1: H is_immediate_constituent_of F;
thus H is_subformula_of F
proof
take n=2 , L=<* H,F *>;
thus 1 <= n;
thus len L = n by FINSEQ_1:44;
thus L.1 = H & L.n = F;
let k;
assume that
A2: 1 <= k and
A3: k < n;
take H,F;
k < 1 + 1 by A3;
then k <= 1 by NAT_1:13;
then k = 1 by A2,XXREAL_0:1;
hence L.k = H & L.(k + 1) = F;
thus thesis by A1;
end;
assume H = F;
then len H = len F;
hence contradiction by A1,Th28;
end;
theorem
(G is negative or G is next) implies the_argument_of G is_subformula_of G
proof
assume G is negative or G is next;
then the_argument_of G is_immediate_constituent_of G by Th20,Th21;
then the_argument_of G is_proper_subformula_of G by Th29;
hence thesis;
end;
theorem
(G is conjunctive or G is disjunctive or G is Until or G is Release )
implies the_left_argument_of G is_subformula_of G & the_right_argument_of G
is_subformula_of G
proof
assume
A1: G is conjunctive or G is disjunctive or G is Until or G is Release;
then the_right_argument_of G is_immediate_constituent_of G by Th22,Th23,Th24
,Th25;
then
A2: the_right_argument_of G is_proper_subformula_of G by Th29;
the_left_argument_of G is_immediate_constituent_of G by A1,Th22,Th23,Th24
,Th25;
then the_left_argument_of G is_proper_subformula_of G by Th29;
hence thesis by A2;
end;
theorem Th32:
H is_proper_subformula_of F implies len H < len F
proof
assume H is_subformula_of F;
then consider n,L such that
A1: 1 <= n and
len L = n and
A2: L.1 = H and
A3: L.n = F and
A4: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1;
defpred P[Nat] means 1 <= $1 & $1 < n implies for H1 st L.($1 + 1) = H1
holds len H < len H1;
A5: for k st P[k] holds P[k + 1]
proof
let k such that
A6: 1 <= k & k < n implies for H1 st L.(k + 1) = H1 holds len H < len H1 and
A7: 1 <= k + 1 and
A8: k + 1 < n;
consider F1,G such that
A9: L.(k + 1) = F1 and
A10: L.(k + 1 + 1) = G & F1 is_immediate_constituent_of G by A4,A7,A8;
let H1 such that
A11: L.(k + 1 + 1) = H1;
A12: now
given m be Nat such that
A13: k = m + 1;
len H < len F1 by A6,A8,A9,A13,NAT_1:11,13;
hence thesis by A11,A10,Th28,XXREAL_0:2;
end;
k = 0 implies len H < len H1 by A2,A11,A9,A10,Th28;
hence thesis by A12,NAT_1:6;
end;
assume H <> F;
then 1 < n by A1,A2,A3,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A14: n = 2 + k by NAT_1:10;
A15: P[0];
A16: for k holds P[k] from NAT_1:sch 2(A15,A5);
A17: 1 + 1 + k = (1 + k) + 1;
then 1 + k < n by A14,NAT_1:13;
hence thesis by A3,A16,A14,A17,NAT_1:11;
end;
theorem
H is_proper_subformula_of F implies ex G st G is_immediate_constituent_of F
proof
assume H is_subformula_of F;
then consider n,L such that
A1: 1 <= n and
len L = n and
A2: L.1 = H and
A3: L.n = F and
A4: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1;
assume H <> F;
then 1 < n by A1,A2,A3,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A5: n = 2 + k by NAT_1:10;
1 + 1 + k = (1 + k) + 1;
then 1 + k < n by A5,NAT_1:13;
then consider H1,F1 such that
L.(1 + k) = H1 and
A6: L.(1 + k + 1) = F1 & H1 is_immediate_constituent_of F1 by A4,NAT_1:11;
take H1;
thus thesis by A3,A5,A6;
end;
reserve j for Nat;
reserve j1 for Element of NAT;
theorem Th34:
F is_proper_subformula_of G & G is_proper_subformula_of H
implies F is_proper_subformula_of H
proof
assume that
A1: F is_subformula_of G and
A2: F <> G and
A3: G is_subformula_of H and
A4: G <> H;
consider m,L9 such that
A5: 1 <= m and
A6: len L9 = m and
A7: L9.1 = G and
A8: L9.m = H and
A9: for k st 1 <= k & k < m ex H1,F1 st L9.k = H1 & L9.(k + 1) = F1 &
H1 is_immediate_constituent_of F1 by A3;
consider n,L such that
A10: 1 <= n and
A11: len L = n and
A12: L.1 = F and
A13: L.n = G and
A14: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1 by A1;
1 < n by A2,A10,A12,A13,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A15: n = 2 + k by NAT_1:10;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
thus F is_subformula_of H
proof
take l = 1 + k + m, K = L1^L9;
A16: 1 + k + m - (1 + k) = m;
m <= m + (1 + k) by NAT_1:11;
hence 1 <= l by A5,XXREAL_0:2;
1 + 1 + k = 1 + k + 1;
then
A17: 1 + k <= n by A15,NAT_1:11;
then
A18: len L1 = 1 + k by A11,FINSEQ_1:17;
hence
A19: len K = l by A6,FINSEQ_1:22;
A20: now
let j;
assume 1 <= j & j <= 1 + k;
then
A21: j in Seg(1 + k) by FINSEQ_1:1;
then j in dom L1 by A11,A17,FINSEQ_1:17;
then K.j = L1.j by FINSEQ_1:def 7;
hence K.j = L.j by A21,FUNCT_1:49;
end;
1 <= 1 + k by NAT_1:11;
hence K.1 = F by A12,A20;
len L1 + 1 <= len L1 + m by A5,XREAL_1:7;
then len L1 < l by A18,NAT_1:13;
then K.l = L9.(l - len L1) by A19,FINSEQ_1:24;
hence K.l = H by A11,A8,A17,A16,FINSEQ_1:17;
let j such that
A22: 1 <= j and
A23: j < l;
j + 0 <= j + 1 by XREAL_1:7;
then
A24: 1 <= j + 1 by A22,XXREAL_0:2;
A25: now
assume
A26: j < 1 + k;
then
A27: j + 1 <= 1 + k by NAT_1:13;
then j + 1 <= n by A17,XXREAL_0:2;
then j < n by NAT_1:13;
then consider F1,G1 such that
A28: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A14,A22;
take F1, G1;
thus K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A20
,A22,A24,A26,A27,A28;
end;
A29: now
A30: j + 1 <= l by A23,NAT_1:13;
assume
A31: 1 + k < j;
then
A32: 1 + k < j + 1 by NAT_1:13;
1 + k + 1 <= j by A31,NAT_1:13;
then consider j1 be Nat such that
A33: j = 1 + k + 1 + j1 by NAT_1:10;
j - (1 + k) < l - (1 + k) by A23,XREAL_1:9;
then consider F1,G1 such that
A34: L9.(1 + j1) = F1 & L9.(1 + j1 + 1) = G1 & F1
is_immediate_constituent_of G1 by A9,A33,NAT_1:11;
take F1, G1;
A35: 1 + j1 + (1 + k) - (1 + k) = 1 + j1 + (1 + k) + -(1 + k);
j + 1 - len L1 = 1 + (j + -len L1)
.= 1 + j1 + 1 by A11,A17,A33,A35,FINSEQ_1:17;
hence K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by
A18,A19,A23,A31,A32,A30,A35,A34,FINSEQ_1:24;
end;
now
A36: j + 1 <= l & j + 1 - j = j + 1 + -j by A23,NAT_1:13;
assume
A37: j = 1 + k;
then j < 1 + k + 1 by NAT_1:13;
then consider F1,G1 such that
A38: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1
by A14,A15,A22;
take F1, G1;
1 + k < j + 1 by A37,NAT_1:13;
hence
K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A13,A7
,A15,A18,A19,A20,A22,A37,A36,A38,FINSEQ_1:24;
end;
hence thesis by A25,A29,XXREAL_0:1;
end;
assume
A39: F = H;
F is_proper_subformula_of G by A1,A2;
then
A40: len F < len G by Th32;
G is_proper_subformula_of H by A3,A4;
hence contradiction by A39,A40,Th32;
end;
theorem Th35:
F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H
proof
assume that
A1: F is_subformula_of G and
A2: G is_subformula_of H;
now
assume F <> G;
then
A3: F is_proper_subformula_of G by A1;
now
assume G <> H;
then G is_proper_subformula_of H by A2;
then F is_proper_subformula_of H by A3,Th34;
hence thesis;
end;
hence thesis by A1;
end;
hence thesis by A2;
end;
theorem
G is_subformula_of H & H is_subformula_of G implies G = H
proof
assume that
A1: G is_subformula_of H and
A2: H is_subformula_of G;
assume
A3: G <> H;
then G is_proper_subformula_of H by A1;
then
A4: len G < len H by Th32;
H is_proper_subformula_of G by A2,A3;
hence contradiction by A4,Th32;
end;
theorem Th37:
(G is negative or G is next) & F is_proper_subformula_of G
implies F is_subformula_of (the_argument_of G)
proof
assume that
A1: G is negative or G is next and
A2: F is_subformula_of G and
A3: F <> G;
consider n,L such that
A4: 1 <= n and
A5: len L = n and
A6: L.1 = F and
A7: L.n = G and
A8: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1 by A2;
1 < n by A3,A4,A6,A7,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A9: n = 2 + k by NAT_1:10;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
take m = 1 + k, L1;
thus
A10: 1 <= m by NAT_1:11;
1 + k <= 1 + k + 1 by NAT_1:11;
hence len L1 = m by A5,A9,FINSEQ_1:17;
A11: now
let j;
assume 1 <= j & j <= m;
then j in { j1 where j1 is Nat : 1 <= j1 & j1 <= 1 + k };
then j in Seg(1 + k) by FINSEQ_1:def 1;
hence L1.j = L.j by FUNCT_1:49;
end;
hence L1.1 = F by A6,A10;
m < m + 1 by NAT_1:13;
then consider F1,G1 such that
A12: L.m = F1 and
A13: L.(m + 1) = G1 & F1 is_immediate_constituent_of G1 by A8,A9,NAT_1:11;
F1 = (the_argument_of G) by A1,A7,A9,A13,Th20,Th21;
hence L1.m = (the_argument_of G) by A10,A11,A12;
let j;
assume that
A14: 1 <= j and
A15: j < m;
m <= m + 1 by NAT_1:11;
then j < n by A9,A15,XXREAL_0:2;
then consider F1,G1 such that
A16: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A8,A14;
take F1,G1;
1 <= 1 + j & j + 1 <= m by A14,A15,NAT_1:13;
hence thesis by A11,A14,A15,A16;
end;
theorem Th38:
(G is conjunctive or G is disjunctive or G is Until or G is
Release ) & F is_proper_subformula_of G implies F is_subformula_of (
the_left_argument_of G) or F is_subformula_of (the_right_argument_of G)
proof
assume that
A1: G is conjunctive or G is disjunctive or G is Until or G is Release and
A2: F is_subformula_of G and
A3: F <> G;
consider n,L such that
A4: 1 <= n and
A5: len L = n and
A6: L.1 = F and
A7: L.n = G and
A8: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1 by A2;
1 < n by A3,A4,A6,A7,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A9: n = 2 + k by NAT_1:10;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
1 + 1 + k = 1 + k + 1;
then 1 + k < n by A9,NAT_1:13;
then consider H1,G1 such that
A10: L.(1 + k) = H1 and
A11: L.(1 + k + 1) = G1 & H1 is_immediate_constituent_of G1 by A8,NAT_1:11;
F is_subformula_of H1
proof
take m = 1 + k, L1;
thus
A12: 1 <= m by NAT_1:11;
1 + k <= 1 + k + 1 by NAT_1:11;
hence len L1 = m by A5,A9,FINSEQ_1:17;
A13: now
let j;
assume 1 <= j & j <= m;
then j in { j1 where j1 is Nat : 1 <= j1 & j1 <= 1 + k };
then j in Seg(1 + k) by FINSEQ_1:def 1;
hence L1.j = L.j by FUNCT_1:49;
end;
hence L1.1 = F by A6,A12;
thus L1.m = H1 by A10,A12,A13;
let j;
assume that
A14: 1 <= j and
A15: j < m;
m <= m + 1 by NAT_1:11;
then j < n by A9,A15,XXREAL_0:2;
then consider F1,G1 such that
A16: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A8,A14;
take F1,G1;
1 <= 1 + j & j + 1 <= m by A14,A15,NAT_1:13;
hence thesis by A13,A14,A15,A16;
end;
hence thesis by A1,A7,A9,A11,Th22,Th23,Th24,Th25;
end;
theorem
F is_proper_subformula_of 'not' H implies F is_subformula_of H
proof
assume
A1: F is_proper_subformula_of 'not' H;
A2: 'not' H is negative;
then the_argument_of ('not' H) = H by Def18;
hence thesis by A1,A2,Th37;
end;
theorem
F is_proper_subformula_of 'X' H implies F is_subformula_of H
proof
assume
A1: F is_proper_subformula_of 'X' H;
A2: 'X' H is next;
then not 'X' H is negative by Lm19;
then the_argument_of ('X' H) = H by A2,Def18;
hence thesis by A1,A2,Th37;
end;
theorem
F is_proper_subformula_of G '&' H implies F is_subformula_of G or F
is_subformula_of H
proof
assume
A1: F is_proper_subformula_of G '&' H;
A2: G '&' H is conjunctive;
then
the_left_argument_of (G '&' H) = G & the_right_argument_of (G '&' H) =H
by Def19,Def20;
hence thesis by A1,A2,Th38;
end;
theorem
F is_proper_subformula_of G 'or' H implies F is_subformula_of G or F
is_subformula_of H
proof
assume
A1: F is_proper_subformula_of G 'or' H;
A2: G 'or' H is disjunctive;
then
the_left_argument_of (G 'or' H) = G & the_right_argument_of (G 'or' H) =
H by Def19,Def20;
hence thesis by A1,A2,Th38;
end;
theorem
F is_proper_subformula_of G 'U' H implies F is_subformula_of G or F
is_subformula_of H
proof
assume
A1: F is_proper_subformula_of G 'U' H;
A2: G 'U' H is Until;
then
the_left_argument_of (G 'U' H) = G & the_right_argument_of (G 'U' H) =H
by Def19,Def20;
hence thesis by A1,A2,Th38;
end;
theorem
F is_proper_subformula_of G 'R' H implies F is_subformula_of G or F
is_subformula_of H
proof
assume
A1: F is_proper_subformula_of G 'R' H;
set G1 = G 'R' H;
A2: G1 is Release;
then
A3: not G1 is Until by Lm21;
( not G1 is conjunctive)& not G1 is disjunctive by A2,Lm21;
then the_left_argument_of G1 = G & the_right_argument_of G1 =H by A2,A3,Def19
,Def20;
hence thesis by A1,A2,Th38;
end;
::
:: The Set of Subformulae of LTL-formulae
::
definition
let H;
func Subformulae H -> set means
:Def24:
a in it iff ex F st F = a & F is_subformula_of H;
existence
proof
defpred X[object] means ex F st F = $1 & F is_subformula_of H;
consider X such that
A1: for a being object holds a in X iff a in NAT* & X[a] from XBOOLE_0:sch 1;
take X;
let a;
thus a in X implies ex F st F = a & F is_subformula_of H by A1;
given F such that
A2: F = a & F is_subformula_of H;
F in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A2;
end;
uniqueness
proof
let X,Y such that
A3: a in X iff ex F st F = a & F is_subformula_of H and
A4: a in Y iff ex F st F = a & F is_subformula_of H;
now
let a be object;
thus a in X implies a in Y
proof
assume a in X;
then ex F st F = a & F is_subformula_of H by A3;
hence thesis by A4;
end;
assume a in Y;
then ex F st F = a & F is_subformula_of H by A4;
hence a in X by A3;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th45:
G in Subformulae H iff G is_subformula_of H
proof
G in Subformulae H implies G is_subformula_of H
proof
assume G in Subformulae H;
then ex F st F = G & F is_subformula_of H by Def24;
hence thesis;
end;
hence thesis by Def24;
end;
registration
let H;
cluster Subformulae H -> non empty;
coherence by Th45;
end;
theorem
F is_subformula_of H implies Subformulae F c= Subformulae H
proof
assume
A1: F is_subformula_of H;
let a be object;
assume a in Subformulae F;
then consider F1 such that
A2: F1 = a and
A3: F1 is_subformula_of F by Def24;
F1 is_subformula_of H by A1,A3,Th35;
hence thesis by A2,Def24;
end;
theorem
a is Subset of Subformulae H implies a is Subset of LTL_WFF
proof
assume
A1: a is Subset of Subformulae H;
for x being object holds x in a implies x in LTL_WFF
proof let x be object;
assume x in a;
then ex F st F = x & F is_subformula_of H by A1,Def24;
hence thesis by Th1;
end;
hence thesis by TARSKI:def 3;
end;
scheme
LTLInd { P[LTL-formula] } : for H holds P[H]
provided
A1: for H st H is atomic holds P[H] and
A2: for H st (H is negative or H is next) & P[the_argument_of H] holds P
[H] and
A3: for H st (H is conjunctive or H is disjunctive or H is Until or H is
Release )& P[the_left_argument_of H] & P[the_right_argument_of H] holds P[H]
proof
defpred Q[Nat] means for H st len H = $1 holds P[H];
A4: for n being Nat st for k being Nat st k < n holds Q[k] holds Q[n]
proof
let n being Nat such that
A5: for k being Nat st k < n for H st len H = k holds P[H];
let H such that
A6: len H = n;
A7: now
assume
A8: H is conjunctive or H is disjunctive or H is Until or H is Release;
then len the_right_argument_of H < len H by Th11;
then
A9: P[the_right_argument_of H] by A5,A6;
len the_left_argument_of H < len H by A8,Th11;
then P[the_left_argument_of H] by A5,A6;
hence thesis by A3,A8,A9;
end;
now
assume
A10: H is negative or H is next;
then len the_argument_of H < len H by Th10;
then P[the_argument_of H] by A5,A6;
hence thesis by A2,A10;
end;
hence thesis by A1,A7,Th2;
end;
A11: for n being Nat holds Q[n] from NAT_1:sch 4(A4);
let H;
len H = len H;
hence thesis by A11;
end;
scheme
LTLCompInd { P[LTL-formula] } : for H holds P[H]
provided
A1: for H st for F st F is_proper_subformula_of H holds P[F] holds P[H]
proof
defpred Q[Nat] means for H st len H = $1 holds P[H];
A2: for n being Nat st for k being Nat st k < n holds Q[k] holds Q[n]
proof
let n being Nat such that
A3: for k being Nat st k < n for H st len H = k holds P[H];
let H such that
A4: len H = n;
now
let F;
assume F is_proper_subformula_of H;
then len F < len H by Th32;
hence P[F] by A3,A4;
end;
hence thesis by A1;
end;
A5: for n being Nat holds Q[n] from NAT_1:sch 4 (A2);
let H;
len H = len H;
hence thesis by A5;
end;
::***************************************************
::**
::** definition of LTL model structure.
::**
::****************************************************
definition
let x be object;
func CastLTL(x) -> LTL-formula equals
:Def25:
x if x in LTL_WFF otherwise
atom.0;
correctness by Th1;
end;
definition
struct(OrthoLattStr) LTLModelStr (# carrier -> set, BasicAssign ->
Subset of the carrier, L_meet -> BinOp of the carrier,
L_join -> BinOp of the carrier,
Compl -> UnOp of the carrier, NEXT-> UnOp of the
carrier, UNTIL -> BinOp of the carrier, RELEASE -> BinOp of the
carrier #);
end;
definition
let V be LTLModelStr;
mode Assign of V is Element of the carrier of V;
end;
:: Preparation to define semantics for LTL-language
:: definition of evaluate function of LTL
definition
func atomic_LTL -> Subset of LTL_WFF equals
{x where x is LTL-formula:x is
atomic};
correctness
proof
set X = {x where x is LTL-formula:x is atomic};
X c= LTL_WFF
proof
let y be object;
assume y in X;
then ex x being LTL-formula st y=x & x is atomic;
hence thesis by Th1;
end;
hence thesis;
end;
end;
definition
let V be LTLModelStr;
let Kai be Function of atomic_LTL,the BasicAssign of V;
let f be Function of LTL_WFF,the carrier of V;
pred f is-Evaluation-for Kai means
for H being LTL-formula holds (H is atomic implies f.H = Kai.H) &
(H is negative implies f.H = (the Compl of V).(f
.(the_argument_of H))) &
(H is conjunctive implies f.H = (the L_meet of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))) & (H is disjunctive
implies f.H = (the L_join of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H))) & (H is next implies f.H = (the NEXT of V).(f.(
the_argument_of H))) & (H is Until implies f.H = (the UNTIL of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))) & (H is Release implies
f.H = (the RELEASE of V).(f.(the_left_argument_of H), f.(the_right_argument_of
H)));
end;
definition
let V be LTLModelStr;
let Kai be Function of atomic_LTL,the BasicAssign of V;
let f be Function of LTL_WFF,the carrier of V;
let n be Nat;
pred f is-PreEvaluation-for n,Kai means
:Def28:
for H being LTL-formula st
len(H) <= n holds (H is atomic implies f.H = Kai.H) & (H is negative implies f.
H = (the Compl of V).(f.(the_argument_of H))) &
(H is conjunctive implies f.H = (
the L_meet of V).(f.(the_left_argument_of H), f.(the_right_argument_of H)))
& (H
is disjunctive implies f.H = (the L_join of V).(f.(the_left_argument_of H),
f.(
the_right_argument_of H))) & (H is next implies f.H = (the NEXT of V).(f.(
the_argument_of H))) & (H is Until implies f.H = (the UNTIL of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))) & (H is Release implies
f.H = (the RELEASE of V).(f.(the_left_argument_of H), f.(the_right_argument_of
H)));
end;
definition
let V be LTLModelStr;
let Kai be Function of atomic_LTL,the BasicAssign of V;
let f,h be Function of LTL_WFF,the carrier of V;
let n be Nat;
let H be LTL-formula;
func GraftEval(V,Kai,f,h,n,H) -> set equals
:Def29:
f.H if len(H) > n+1, Kai
.H if len(H)=n+1 & H is atomic, (the Compl of V).(h.(the_argument_of H))
if len(H
)=n+1 & H is negative, (the L_meet of V).(h.(the_left_argument_of H), h.(
the_right_argument_of H)) if len(H)=n+1 & H is conjunctive,
(the L_join of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) if len(H)=n+1 & H is
disjunctive, (the NEXT of V).(h.(the_argument_of H)) if len(H)=n+1 & H is next
, (the UNTIL of V).(h.(the_left_argument_of H), h.(the_right_argument_of H)) if
len(H)=n+1 & H is Until, (the RELEASE of V).(h.(the_left_argument_of H), h.(
the_right_argument_of H)) if len(H)=n+1 & H is Release, h.H if len(H)<n+1
otherwise {};
coherence;
consistency by Lm16,Lm17,Lm18,Lm19,Lm20,Lm21;
end;
definition let C be LTLModelStr;
attr C is with_basic means
:Def30: the BasicAssign of C is non empty;
end;
definition
func TrivialLTLModel -> LTLModelStr equals
LTLModelStr(# {0}, [#]{0}, op2, op2, op1, op1, op2, op2#);
coherence;
end;
registration
cluster TrivialLTLModel -> with_basic strict non empty;
coherence;
end;
registration
cluster non empty for LTLModelStr;
existence
proof
take TrivialLTLModel;
thus thesis;
end;
end;
registration
cluster with_basic for non empty LTLModelStr;
existence
proof
take TrivialLTLModel;
thus thesis;
end;
end;
definition
mode LTLModel is with_basic non empty LTLModelStr;
end;
registration let C be LTLModel;
cluster the BasicAssign of C -> non empty;
coherence by Def30;
end;
reserve V for LTLModel;
reserve Kai for Function of atomic_LTL,the BasicAssign of V;
reserve f,f1,f2 for Function of LTL_WFF,the carrier of V;
Lm22: f is-PreEvaluation-for 0,Kai
by Th3;
Lm23: f is-PreEvaluation-for n+1,Kai implies f is-PreEvaluation-for n,Kai
proof
assume
A1: f is-PreEvaluation-for n+1,Kai;
for H being LTL-formula st len(H) <= n holds (H is atomic implies f.H =
Kai.H) & (H is negative implies f.H = (the Compl of V).(f.(the_argument_of H)))
&
(H is conjunctive implies f.H = (the L_meet of V).(f.(the_left_argument_of H),
f.(
the_right_argument_of H))) &
(H is disjunctive implies f.H = (the L_join of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))) & (H is next implies f.H
= (the NEXT of V).(f.(the_argument_of H))) & (H is Until implies f.H = (the
UNTIL of V).(f.(the_left_argument_of H), f.(the_right_argument_of H))) & (H is
Release implies f.H = (the RELEASE of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)))
proof
let H be LTL-formula;
assume len(H) <= n;
then len(H) < n+1 by NAT_1:13;
hence thesis by A1;
end;
hence thesis;
end;
Lm24: f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai implies
for H being LTL-formula st len(H) <= n holds f1.H = f2.H
proof
defpred P[Nat] means (f1 is-PreEvaluation-for $1,Kai) & (f2
is-PreEvaluation-for $1,Kai) implies (for H being LTL-formula st len(H) <= $1
holds f1.H = f2.H);
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A2: P[k];
assume that
A3: f1 is-PreEvaluation-for k+1,Kai and
A4: f2 is-PreEvaluation-for k+1,Kai;
let H be LTL-formula such that
A5: len(H)<= k+1;
per cases by Th2;
suppose
A6: H is atomic;
then f1.H = Kai.H by A3,A5;
hence thesis by A4,A5,A6;
end;
suppose
A7: H is negative;
then len the_argument_of H < len(H) by Th10;
then
A8: len the_argument_of H <= k by A5,Lm1;
f2.H = (the Compl of V).(f2.(the_argument_of H)) by A4,A5,A7
.= (the Compl of V).(f1.(the_argument_of H)) by A2,A3,A4,A8,Lm23;
hence thesis by A3,A5,A7;
end;
suppose
A9: H is next;
then len(the_argument_of H) < len(H) by Th10;
then
A10: len(the_argument_of H) <= k by A5,Lm1;
f2.H = (the NEXT of V).(f2.(the_argument_of H)) by A4,A5,A9
.= (the NEXT of V).(f1.(the_argument_of H)) by A2,A3,A4,A10,Lm23;
hence thesis by A3,A5,A9;
end;
suppose
A11: H is conjunctive;
then len(the_left_argument_of H) < len(H) by Th11;
then len(the_left_argument_of H) <= k by A5,Lm1;
then
A12: f1.(the_left_argument_of H) = f2.(the_left_argument_of H) by A2,A3,A4
,Lm23;
len(the_right_argument_of H) < len(H) by A11,Th11;
then
A13: len(the_right_argument_of H) <= k by A5,Lm1;
f2.H = (the L_meet of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A4,A5,A11
.= (the L_meet of V).(f1.(the_left_argument_of H), f1.(
the_right_argument_of H)) by A2,A3,A4,A12,A13,Lm23;
hence thesis by A3,A5,A11;
end;
suppose
A14: H is disjunctive;
then len(the_left_argument_of H) < len(H) by Th11;
then len(the_left_argument_of H) <= k by A5,Lm1;
then
A15: f1.(the_left_argument_of H) = f2.(the_left_argument_of H) by A2,A3,A4
,Lm23;
len(the_right_argument_of H) < len(H) by A14,Th11;
then
A16: len(the_right_argument_of H) <= k by A5,Lm1;
f2.H = (the L_join of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A4,A5,A14
.= (the L_join of V).(f1.(the_left_argument_of H), f1.(
the_right_argument_of H)) by A2,A3,A4,A15,A16,Lm23;
hence thesis by A3,A5,A14;
end;
suppose
A17: H is Until;
then len(the_left_argument_of H) < len(H) by Th11;
then len(the_left_argument_of H) <= k by A5,Lm1;
then
A18: f1.(the_left_argument_of H) = f2.(the_left_argument_of H) by A2,A3,A4
,Lm23;
len(the_right_argument_of H) < len(H) by A17,Th11;
then
A19: len(the_right_argument_of H) <= k by A5,Lm1;
f2.H = (the UNTIL of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A4,A5,A17
.= (the UNTIL of V).(f1.(the_left_argument_of H), f1.(
the_right_argument_of H)) by A2,A3,A4,A18,A19,Lm23;
hence thesis by A3,A5,A17;
end;
suppose
A20: H is Release;
then len(the_left_argument_of H) < len(H) by Th11;
then len(the_left_argument_of H) <= k by A5,Lm1;
then
A21: f1.(the_left_argument_of H) = f2.(the_left_argument_of H) by A2,A3,A4
,Lm23;
len(the_right_argument_of H) < len(H) by A20,Th11;
then
A22: len(the_right_argument_of H) <= k by A5,Lm1;
f2.H = (the RELEASE of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A4,A5,A20
.= (the RELEASE of V).(f1.(the_left_argument_of H), f1.(
the_right_argument_of H)) by A2,A3,A4,A21,A22,Lm23;
hence thesis by A3,A5,A20;
end;
end;
A23: P[0] by Th3;
for n being Nat holds P[n] from NAT_1:sch 2(A23,A1);
hence thesis;
end;
Lm25: for n holds ex f st f is-PreEvaluation-for n,Kai
proof
defpred P[Nat] means ex f being Function of LTL_WFF,the carrier of V st
f is-PreEvaluation-for $1,Kai;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume P[k];
then consider h being Function of LTL_WFF,the carrier of V such that
A2: h is-PreEvaluation-for k,Kai;
P[k+1]
proof
deffunc F(object) =GraftEval(V,Kai,h,h,k,CastLTL($1));
A3: for H being object st H in LTL_WFF holds F(H) in the carrier of V
proof
let H be object such that
A4: H in LTL_WFF;
reconsider H as LTL-formula by A4,Th1;
A5: F(H)=GraftEval(V,Kai,h,h,k,H) by A4,Def25;
per cases by Th2,XXREAL_0:1;
suppose
len(H) > k+1;
then GraftEval(V,Kai,h,h,k,H)=h.H by Def29;
hence thesis by A4,A5,FUNCT_2:5;
end;
suppose
A6: len(H)=k+1 & H is atomic;
then H in atomic_LTL;
then Kai.H in the BasicAssign of V by FUNCT_2:5;
then Kai.H in the carrier of V;
hence thesis by A5,A6,Def29;
end;
suppose
A7: len(H)=k+1 & H is negative;
the_argument_of H in LTL_WFF by Th1;
then
A8: h.(the_argument_of H) in the carrier of V by FUNCT_2:5;
GraftEval(V,Kai,h,h,k,H) = (the Compl of V).(h.(the_argument_of H
)) by A7,Def29;
hence thesis by A5,A8,FUNCT_2:5;
end;
suppose
len(H)=k+1 & H is conjunctive;
then
A9: GraftEval(V,Kai,h,h,k,H) = (the L_meet of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by Def29;
the_right_argument_of H in LTL_WFF by Th1;
then
A10: h.(the_right_argument_of H) in the carrier of V by FUNCT_2:5;
the_left_argument_of H in LTL_WFF by Th1;
then h.(the_left_argument_of H) in the carrier of V by FUNCT_2:5;
then [h.(the_left_argument_of H),h.(the_right_argument_of H)] in [:
the carrier of V,the carrier of V:] by A10,ZFMISC_1:def 2;
hence thesis by A5,A9,FUNCT_2:5;
end;
suppose
len(H)=k+1 & H is disjunctive;
then
A11: GraftEval(V,Kai,h,h,k,H) = (the L_join of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by Def29;
the_right_argument_of H in LTL_WFF by Th1;
then
A12: h.(the_right_argument_of H) in the carrier of V by FUNCT_2:5;
the_left_argument_of H in LTL_WFF by Th1;
then h.(the_left_argument_of H) in the carrier of V by FUNCT_2:5;
then [h.(the_left_argument_of H),h.(the_right_argument_of H)] in [:
the carrier of V,the carrier of V:] by A12,ZFMISC_1:def 2;
hence thesis by A5,A11,FUNCT_2:5;
end;
suppose
A13: len(H)=k+1 & H is next;
the_argument_of H in LTL_WFF by Th1;
then
A14: h.(the_argument_of H) in the carrier of V by FUNCT_2:5;
GraftEval(V,Kai,h,h,k,H) = (the NEXT of V).(h.(the_argument_of
H)) by A13,Def29;
hence thesis by A5,A14,FUNCT_2:5;
end;
suppose
len(H)=k+1 & H is Until;
then
A15: GraftEval(V,Kai,h,h,k,H) = (the UNTIL of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by Def29;
the_right_argument_of H in LTL_WFF by Th1;
then
A16: h.(the_right_argument_of H) in the carrier of V by FUNCT_2:5;
the_left_argument_of H in LTL_WFF by Th1;
then h.(the_left_argument_of H) in the carrier of V by FUNCT_2:5;
then [h.(the_left_argument_of H),h.(the_right_argument_of H)] in [:
the carrier of V,the carrier of V:] by A16,ZFMISC_1:def 2;
hence thesis by A5,A15,FUNCT_2:5;
end;
suppose
len(H)=k+1 & H is Release;
then
A17: GraftEval(V,Kai,h,h,k,H) = (the RELEASE of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by Def29;
the_right_argument_of H in LTL_WFF by Th1;
then
A18: h.(the_right_argument_of H) in the carrier of V by FUNCT_2:5;
the_left_argument_of H in LTL_WFF by Th1;
then h.(the_left_argument_of H) in the carrier of V by FUNCT_2:5;
then [h.(the_left_argument_of H),h.(the_right_argument_of H)] in [:
the carrier of V,the carrier of V:] by A18,ZFMISC_1:def 2;
hence thesis by A5,A17,FUNCT_2:5;
end;
suppose
len(H) < k+1;
then GraftEval(V,Kai,h,h,k,H)=h.H by Def29;
hence thesis by A4,A5,FUNCT_2:5;
end;
end;
consider f be Function of LTL_WFF,the carrier of V such that
A19: for H being object st H in LTL_WFF holds f.H =F(H) from FUNCT_2:sch
2(A3);
take f;
A20: for H being LTL-formula st len(H) <k+1 holds f.H =h.H
proof
let H be LTL-formula such that
A21: len(H) < k+1;
A22: H in LTL_WFF by Th1;
then f.H = F(H) by A19
.=GraftEval(V,Kai,h,h,k,H) by A22,Def25;
hence thesis by A21,Def29;
end;
for H being LTL-formula st len(H) <= k+1 holds (H is atomic implies
f.H = Kai.H) & (H is negative implies
f.H = (the Compl of V).(f.(the_argument_of
H))) & (H is conjunctive implies
f.H = (the L_meet of V).(f.(the_left_argument_of
H), f.(the_right_argument_of H))) &
(H is disjunctive implies f.H = (the L_join of
V).(f.(the_left_argument_of H), f.(the_right_argument_of H))) & (H is next
implies f.H = (the NEXT of V).(f.(the_argument_of H))) & (H is Until implies f.
H = (the UNTIL of V).(f.(the_left_argument_of H), f.(the_right_argument_of H)))
& (H is Release implies f.H = (the RELEASE of V).(f.(the_left_argument_of H), f
.(the_right_argument_of H)))
proof
let H be LTL-formula such that
A23: len(H) <= k+1;
A24: H in LTL_WFF by Th1;
then
A25: f.H = F(H) by A19
.=GraftEval(V,Kai,h,h,k,H) by A24,Def25;
A26: H is negative implies f.H = (the Compl of V).(f.(the_argument_of H))
proof
assume
A27: H is negative;
then len(the_argument_of H) < len(H) by Th10;
then len(the_argument_of H) <=k by A23,Lm1;
then
A28: len(the_argument_of H) < k+1 by NAT_1:13;
per cases by A23,NAT_1:8;
suppose
A29: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A20
.= (the Compl of V).(h.(the_argument_of H)) by A2,A27,A29;
hence thesis by A20,A28;
end;
suppose
len(H) = k+1;
then
GraftEval(V,Kai,h,h,k,H) = (the Compl of V).(h.(the_argument_of
H)) by A27,Def29
.= (the Compl of V).(f.(the_argument_of H)) by A20,A28;
hence thesis by A25;
end;
end;
A30: H is Release implies f.H = (the RELEASE of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))
proof
assume
A31: H is Release;
then len(the_right_argument_of H) < len(H) by Th11;
then len(the_right_argument_of H) <=k by A23,Lm1;
then
A32: len(the_right_argument_of H) < k+1 by NAT_1:13;
len(the_left_argument_of H) < len(H) by A31,Th11;
then len(the_left_argument_of H) <=k by A23,Lm1;
then len(the_left_argument_of H) < k+1 by NAT_1:13;
then
A33: h.(the_left_argument_of H) =f.(the_left_argument_of H) by A20;
per cases by A23,NAT_1:8;
suppose
A34: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A20
.= (the RELEASE of V).(h.(the_left_argument_of H), h.(
the_right_argument_of H)) by A2,A31,A34;
hence thesis by A20,A33,A32;
end;
suppose
len(H) = k+1;
then GraftEval(V,Kai,h,h,k,H) = (the RELEASE of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by A31,Def29
.= (the RELEASE of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A20,A33,A32;
hence thesis by A25;
end;
end;
A35: H is Until implies f.H = (the UNTIL of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))
proof
assume
A36: H is Until;
then len(the_right_argument_of H) < len(H) by Th11;
then len(the_right_argument_of H) <=k by A23,Lm1;
then
A37: len(the_right_argument_of H) < k+1 by NAT_1:13;
len(the_left_argument_of H) < len(H) by A36,Th11;
then len(the_left_argument_of H) <=k by A23,Lm1;
then len(the_left_argument_of H) < k+1 by NAT_1:13;
then
A38: h.(the_left_argument_of H) =f.(the_left_argument_of H) by A20;
per cases by A23,NAT_1:8;
suppose
A39: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A20
.= (the UNTIL of V).(h.(the_left_argument_of H), h.(
the_right_argument_of H)) by A2,A36,A39;
hence thesis by A20,A38,A37;
end;
suppose
len(H) = k+1;
then GraftEval(V,Kai,h,h,k,H) = (the UNTIL of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by A36,Def29
.= (the UNTIL of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A20,A38,A37;
hence thesis by A25;
end;
end;
A40: H is disjunctive implies f.H = (the L_join of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))
proof
assume
A41: H is disjunctive;
then len(the_right_argument_of H) < len(H) by Th11;
then len(the_right_argument_of H) <=k by A23,Lm1;
then
A42: len(the_right_argument_of H) < k+1 by NAT_1:13;
len(the_left_argument_of H) < len(H) by A41,Th11;
then len(the_left_argument_of H) <=k by A23,Lm1;
then len(the_left_argument_of H) < k+1 by NAT_1:13;
then
A43: h.(the_left_argument_of H) =f.(the_left_argument_of H) by A20;
per cases by A23,NAT_1:8;
suppose
A44: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A20
.= (the L_join of V).(h.(the_left_argument_of H), h.(
the_right_argument_of H)) by A2,A41,A44;
hence thesis by A20,A43,A42;
end;
suppose
len(H) = k+1;
then GraftEval(V,Kai,h,h,k,H) = (the L_join of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by A41,Def29
.= (the L_join of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A20,A43,A42;
hence thesis by A25;
end;
end;
A45: H is conjunctive implies f.H = (the L_meet of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))
proof
assume
A46: H is conjunctive;
then len(the_right_argument_of H) < len(H) by Th11;
then len(the_right_argument_of H) <=k by A23,Lm1;
then
A47: len(the_right_argument_of H) < k+1 by NAT_1:13;
len(the_left_argument_of H) < len(H) by A46,Th11;
then len(the_left_argument_of H) <=k by A23,Lm1;
then len(the_left_argument_of H) < k+1 by NAT_1:13;
then
A48: h.(the_left_argument_of H) =f.(the_left_argument_of H) by A20;
per cases by A23,NAT_1:8;
suppose
A49: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A20
.= (the L_meet of V).(h.(the_left_argument_of H), h.(
the_right_argument_of H)) by A2,A46,A49;
hence thesis by A20,A48,A47;
end;
suppose
len(H) = k+1;
then GraftEval(V,Kai,h,h,k,H) = (the L_meet of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by A46,Def29
.= (the L_meet of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A20,A48,A47;
hence thesis by A25;
end;
end;
A50: H is next implies f.H = (the NEXT of V).(f.(the_argument_of H))
proof
assume
A51: H is next;
then len(the_argument_of H) < len(H) by Th10;
then len(the_argument_of H) <=k by A23,Lm1;
then
A52: len(the_argument_of H) < k+1 by NAT_1:13;
per cases by A23,NAT_1:8;
suppose
A53: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A20
.= (the NEXT of V).(h.(the_argument_of H)) by A2,A51,A53;
hence thesis by A20,A52;
end;
suppose
len(H) = k+1;
then GraftEval(V,Kai,h,h,k,H) = (the NEXT of V).(h.(
the_argument_of H)) by A51,Def29
.= (the NEXT of V).(f.(the_argument_of H)) by A20,A52;
hence thesis by A25;
end;
end;
H is atomic implies f.H = Kai.H
proof
assume
A54: H is atomic;
per cases by A23,NAT_1:8;
suppose
A55: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A20
.= Kai.H by A2,A54,A55;
hence thesis;
end;
suppose
len(H) = k+1;
hence thesis by A25,A54,Def29;
end;
end;
hence thesis by A26,A45,A40,A50,A35,A30;
end;
hence thesis;
end;
hence thesis;
end;
A56: P[0]
proof
consider v0 be object such that
A57: v0 in the carrier of V by XBOOLE_0:def 1;
set f = LTL_WFF --> v0;
A58: dom f = LTL_WFF & rng f c= {v0} by FUNCOP_1:13;
{v0} c= the carrier of V by A57,ZFMISC_1:31;
then reconsider f as Function of LTL_WFF,the carrier of V by A58,FUNCT_2:2
,XBOOLE_1:1;
take f;
thus thesis by Lm22;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A56,A1);
hence thesis;
end;
Lm26: (for n holds f is-PreEvaluation-for n,Kai) implies f is-Evaluation-for
Kai
proof
assume
A1: for n holds f is-PreEvaluation-for n,Kai;
let H be LTL-formula;
set n = len(H);
f is-PreEvaluation-for n,Kai by A1;
hence thesis;
end;
definition
let V be LTLModel;
let Kai be Function of atomic_LTL,the BasicAssign of V;
let n be Nat;
func EvalSet(V,Kai,n) ->non empty set equals
{h where h is Function of
LTL_WFF,the carrier of V : h is-PreEvaluation-for n,Kai};
correctness
proof
set X = {h where h is Function of LTL_WFF,the carrier of V : h
is-PreEvaluation-for n,Kai};
consider h being Function of LTL_WFF,the carrier of V such that
A1: h is-PreEvaluation-for n,Kai by Lm25;
h in X by A1;
hence thesis;
end;
end;
definition
let V be LTLModel;
let v0 be Element of the carrier of V;
let x be set;
func CastEval(V,x,v0) ->Function of LTL_WFF,the carrier of V equals
:
Def33: x
if x in Funcs(LTL_WFF,the carrier of V) otherwise LTL_WFF --> v0;
correctness by FUNCT_2:66;
end;
definition
let V be LTLModel;
let Kai be Function of atomic_LTL,the BasicAssign of V;
func EvalFamily(V,Kai) -> non empty set means
:Def34:
for p being set holds
p in it iff p in bool Funcs(LTL_WFF,the carrier of V) & ex n being Nat st
p=EvalSet(V,Kai,n);
existence
proof
defpred Q[set] means ex n being Nat st $1=EvalSet(V,Kai,n);
set X = bool Funcs(LTL_WFF,the carrier of V);
consider IT be set such that
A1: for p being set holds p in IT iff p in X & Q[p] from XFAMILY:sch 1;
IT is non empty
proof
set p = EvalSet(V,Kai,0);
p c= Funcs(LTL_WFF,the carrier of V)
proof
let x be object;
assume x in p;
then ex h being Function of LTL_WFF,the carrier of V st x= h & h
is-PreEvaluation-for 0,Kai;
hence thesis by FUNCT_2:8;
end;
hence thesis by A1;
end;
then reconsider IT as non empty set;
take IT;
thus thesis by A1;
end;
uniqueness
proof
defpred P[set] means $1 in bool Funcs(LTL_WFF,the carrier of V) & ex
n being Nat st $1=EvalSet(V,Kai,n);
for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for
x being set holds x in X2 iff P[x]) holds X1 = X2 from XFAMILY:sch 3;
hence thesis;
end;
end;
Lm27: EvalSet(V,Kai,n) in EvalFamily(V,Kai)
proof
set p1 = EvalSet(V,Kai,n);
p1 c= Funcs(LTL_WFF,the carrier of V)
proof
let x be object;
assume x in p1;
then ex h being Function of LTL_WFF,the carrier of V st x = h & h
is-PreEvaluation-for n,Kai;
hence thesis by FUNCT_2:8;
end;
hence thesis by Def34;
end;
theorem Th48:
ex f st f is-Evaluation-for Kai
proof
set M = EvalFamily(V,Kai);
set v0 = the Element of the carrier of V;
for X being set st X in M holds X <> {}
proof
let X being set;
assume X in M;
then ex n being Nat st X = EvalSet(V,Kai,n) by Def34;
hence thesis;
end;
then consider Choice being Function such that
dom Choice = M and
A1: for X being set st X in M holds Choice.X in X by FUNCT_1:111;
deffunc F(object) = Choice.EvalSet(V,Kai,CastNat($1));
A2: for n being set st n in NAT holds F(n) is Function of LTL_WFF,the
carrier of V
proof
let n be set such that
A3: n in NAT;
set Y = F(n);
reconsider n as Nat by A3;
CastNat(n) = n by Def1;
then Y in EvalSet(V,Kai,n) by A1,Lm27;
then ex h being Function of LTL_WFF,the carrier of V st Y= h & h
is-PreEvaluation-for n,Kai;
hence thesis;
end;
A4: for n being object st n in NAT
holds F(n) in Funcs(LTL_WFF,the carrier of V)
proof
let n be object;
assume n in NAT;
then F(n) is Function of LTL_WFF,the carrier of V by A2;
hence thesis by FUNCT_2:8;
end;
consider f1 being sequence of Funcs(LTL_WFF,the carrier of V) such
that
A5: for n being object st n in NAT holds f1.n = F(n) from FUNCT_2:sch 2(
A4);
deffunc G(object) = CastEval(V,f1.len(CastLTL($1)),v0).$1;
A6: for H being object st H in LTL_WFF holds G(H) in the carrier of V
by FUNCT_2:5;
consider f being Function of LTL_WFF,the carrier of V such that
A7: for H being object st H in LTL_WFF holds f.H = G(H) from FUNCT_2:sch 2
(A6);
take f;
for n being Nat holds f is-PreEvaluation-for n,Kai
proof
defpred P[Nat] means f is-PreEvaluation-for $1,Kai;
A8: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A9: P[k];
for H being LTL-formula st len(H) <= k+1 holds (H is atomic implies
f.H = Kai.H) & (H is negative implies
f.H = (the Compl of V).(f.(the_argument_of
H))) & (H is conjunctive implies
f.H = (the L_meet of V).(f.(the_left_argument_of
H), f.(the_right_argument_of H))) &
(H is disjunctive implies f.H = (the L_join of
V).(f.(the_left_argument_of H), f.(the_right_argument_of H))) & (H is next
implies f.H = (the NEXT of V).(f.(the_argument_of H))) & (H is Until implies f.
H = (the UNTIL of V).(f.(the_left_argument_of H), f.(the_right_argument_of H)))
& (H is Release implies f.H = (the RELEASE of V).(f.(the_left_argument_of H), f
.(the_right_argument_of H)))
proof
let H be LTL-formula such that
A10: len(H) <= k+1;
now
per cases by A10,NAT_1:8;
case
len(H) <= k;
hence thesis by A9,Def28;
end;
case
A11: len(H) = k+1;
set f2 = F(len H);
A12: H in LTL_WFF by Th1;
then f1.len(CastLTL(H)) = f1.len(H) by Def25
.= F(len(H)) by A5;
then
A13: CastEval(V,f1.len(CastLTL(H)),v0) = F(len H) by Def33;
then reconsider f2 as Function of LTL_WFF,the carrier of V;
f2 = Choice.EvalSet(V,Kai,len(H)) & Choice.EvalSet(V,Kai,len(
H)) in EvalSet(V,Kai,len(H)) by A1,Def1,Lm27;
then
A14: ex h being Function of LTL_WFF,the carrier of V st f2 =h
& h is-PreEvaluation-for len(H),Kai;
then
A15: f2 is-PreEvaluation-for k,Kai by A11,Lm23;
A16: f.H = f2.H by A7,A12,A13;
A17: H is next implies f.H = (the NEXT of V).(f.(the_argument_of H ))
proof
assume
A18: H is next;
then len(the_argument_of H) < len(H) by Th10;
then
A19: len(the_argument_of H) <= k by A11,NAT_1:13;
f.H = (the NEXT of V).(f2.(the_argument_of H)) by A16,A14,A18
.= (the NEXT of V).(f.(the_argument_of H)) by A9,A15,A19,Lm24;
hence thesis;
end;
A20: H is Release implies f.H = (the RELEASE of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))
proof
assume
A21: H is Release;
then len(the_right_argument_of H) < len(H) by Th11;
then
A22: len(the_right_argument_of H) <= k by A11,NAT_1:13;
len(the_left_argument_of H) < len(H) by A21,Th11;
then len(the_left_argument_of H) <= k by A11,NAT_1:13;
then
A23: f.(the_left_argument_of H) = f2.(the_left_argument_of H) by A9
,A15,Lm24;
f.H = (the RELEASE of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A16,A14,A21
.= (the RELEASE of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A9,A15,A23,A22,Lm24;
hence thesis;
end;
A24: H is Until implies f.H = (the UNTIL of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))
proof
assume
A25: H is Until;
then len(the_right_argument_of H) < len(H) by Th11;
then
A26: len(the_right_argument_of H) <= k by A11,NAT_1:13;
len(the_left_argument_of H) < len(H) by A25,Th11;
then len(the_left_argument_of H) <= k by A11,NAT_1:13;
then
A27: f.(the_left_argument_of H) = f2.(the_left_argument_of H) by A9
,A15,Lm24;
f.H = (the UNTIL of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A16,A14,A25
.= (the UNTIL of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A9,A15,A27,A26,Lm24;
hence thesis;
end;
A28: H is disjunctive implies f.H = (the L_join of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))
proof
assume
A29: H is disjunctive;
then len(the_right_argument_of H) < len(H) by Th11;
then
A30: len(the_right_argument_of H) <= k by A11,NAT_1:13;
len(the_left_argument_of H) < len(H) by A29,Th11;
then len(the_left_argument_of H) <= k by A11,NAT_1:13;
then
A31: f.(the_left_argument_of H) = f2.(the_left_argument_of H) by A9
,A15,Lm24;
f.H = (the L_join of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A16,A14,A29
.= (the L_join of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A9,A15,A31,A30,Lm24;
hence thesis;
end;
A32: H is conjunctive implies f.H = (the L_meet of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))
proof
assume
A33: H is conjunctive;
then len(the_right_argument_of H) < len(H) by Th11;
then
A34: len(the_right_argument_of H) <= k by A11,NAT_1:13;
len(the_left_argument_of H) < len(H) by A33,Th11;
then len(the_left_argument_of H) <= k by A11,NAT_1:13;
then
A35: f.(the_left_argument_of H) = f2.(the_left_argument_of H) by A9
,A15,Lm24;
f.H = (the L_meet of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A16,A14,A33
.= (the L_meet of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A9,A15,A35,A34,Lm24;
hence thesis;
end;
H is negative implies f.H = (the Compl of V).(f.(
the_argument_of H))
proof
assume
A36: H is negative;
then len(the_argument_of H) < len(H) by Th10;
then
A37: len(the_argument_of H) <= k by A11,NAT_1:13;
f.H = (the Compl of V).(f2.(the_argument_of H)) by A16,A14,A36
.= (the Compl of V).(f.(the_argument_of H)) by A9,A15,A37,Lm24;
hence thesis;
end;
hence thesis by A16,A14,A17,A32,A28,A24,A20;
end;
end;
hence thesis;
end;
hence thesis by Def28;
end;
for H being LTL-formula st len(H) <= 0 holds (H is atomic implies f.H
= Kai.H) & (H is negative implies
f.H = (the Compl of V).(f.(the_argument_of H)))
& (H is conjunctive implies f.H =
(the L_meet of V).(f.(the_left_argument_of H), f
.(the_right_argument_of H))) &
(H is disjunctive implies f.H = (the L_join of V).(f
.(the_left_argument_of H), f.(the_right_argument_of H))) & (H is next implies f
.H = (the NEXT of V).(f.(the_argument_of H))) & (H is Until implies f.H = (the
UNTIL of V).(f.(the_left_argument_of H), f.(the_right_argument_of H))) & (H is
Release implies f.H = (the RELEASE of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)))by Th3;
then
A38: P[0] by Def28;
for n being Nat holds P[n] from NAT_1:sch 2(A38,A8);
hence thesis;
end;
hence thesis by Lm26;
end;
theorem Th49:
f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai implies f1 = f2
proof
assume
A1: f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai;
for H being object st H in LTL_WFF holds f1.H=f2.H
proof
let H be object;
assume H in LTL_WFF;
then reconsider H as LTL-formula by Th1;
set n=len(H);
f1 is-PreEvaluation-for n, Kai & f2 is-PreEvaluation-for n, Kai by A1;
hence thesis by Lm24;
end;
hence thesis by FUNCT_2:12;
end;
definition
let V be LTLModel;
let Kai be Function of atomic_LTL,the BasicAssign of V;
let H be LTL-formula;
func Evaluate(H,Kai) -> Assign of V means
:Def35:
ex f being Function of
LTL_WFF,the carrier of V st f is-Evaluation-for Kai & it = f.H;
existence
proof
consider f be Function of LTL_WFF,the carrier of V such that
A1: f is-Evaluation-for Kai by Th48;
set IT=f.H;
H in LTL_WFF by Th1;
then reconsider IT as Assign of V by FUNCT_2:5;
take IT;
thus thesis by A1;
end;
uniqueness by Th49;
end;
notation
let V be LTLModel;
let f be Assign of V;
synonym 'not' f for f`;
let g be Assign of V;
synonym f '&' g for f "/\" g;
synonym f 'or' g for f "\/" g;
end;
definition
let V be LTLModel;
let f be Assign of V;
func 'X' f -> Assign of V equals
(the NEXT of V).f;
correctness;
end;
definition
let V be LTLModel;
let f,g be Assign of V;
func f 'U' g -> Assign of V equals
(the UNTIL of V).(f,g);
correctness;
func f 'R' g -> Assign of V equals
(the RELEASE of V).(f,g);
correctness;
end;
::Some properties of evaluate function of LTL
theorem Th50:
Evaluate('not' H,Kai) = 'not' Evaluate(H,Kai)
proof
consider f1 be Function of LTL_WFF,the carrier of V such that
A1: f1 is-Evaluation-for Kai and
A2: Evaluate('not' H,Kai) = f1.('not' H) by Def35;
A3: ex f2 be Function of LTL_WFF,the carrier of V st f2
is-Evaluation-for Kai & Evaluate(H,Kai) = f2.H by Def35;
A4: 'not' H is negative;
then
Evaluate('not' H,Kai) = (the Compl of V).(f1.(the_argument_of('not' H)) )
by A1,A2
.= (the Compl of V).(f1.H ) by A4,Def18
.= 'not' Evaluate(H,Kai) by A1,A3,Th49;
hence thesis;
end;
theorem Th51:
Evaluate(H1 '&' H2,Kai) = Evaluate(H1,Kai) '&' Evaluate(H2,Kai)
proof
consider f0 be Function of LTL_WFF,the carrier of V such that
A1: f0 is-Evaluation-for Kai and
A2: Evaluate(H1 '&' H2,Kai) = f0.(H1 '&' H2) by Def35;
consider f1 be Function of LTL_WFF,the carrier of V such that
A3: f1 is-Evaluation-for Kai and
A4: Evaluate(H1,Kai) = f1.H1 by Def35;
consider f2 be Function of LTL_WFF,the carrier of V such that
A5: f2 is-Evaluation-for Kai and
A6: Evaluate(H2,Kai) = f2.H2 by Def35;
A7: f0=f2 by A1,A5,Th49;
A8: H1 '&' H2 is conjunctive;
then
A9: the_left_argument_of(H1 '&' H2) = H1 & the_right_argument_of(H1 '&' H2)
= H2 by Def19,Def20;
f0=f1 by A1,A3,Th49;
hence thesis by A1,A2,A4,A6,A7,A8,A9;
end;
theorem Th52:
Evaluate(H1 'or' H2,Kai) = Evaluate(H1,Kai) 'or' Evaluate(H2,Kai )
proof
consider f0 be Function of LTL_WFF,the carrier of V such that
A1: f0 is-Evaluation-for Kai and
A2: Evaluate(H1 'or' H2,Kai) = f0.(H1 'or' H2) by Def35;
consider f1 be Function of LTL_WFF,the carrier of V such that
A3: f1 is-Evaluation-for Kai and
A4: Evaluate(H1,Kai) = f1.H1 by Def35;
consider f2 be Function of LTL_WFF,the carrier of V such that
A5: f2 is-Evaluation-for Kai and
A6: Evaluate(H2,Kai) = f2.H2 by Def35;
A7: f0=f2 by A1,A5,Th49;
A8: H1 'or' H2 is disjunctive;
then
A9: the_left_argument_of(H1 'or' H2) = H1 & the_right_argument_of(H1 'or'
H2)= H2 by Def19,Def20;
f0=f1 by A1,A3,Th49;
hence thesis by A1,A2,A4,A6,A7,A8,A9;
end;
theorem Th53:
Evaluate('X' H,Kai) = 'X' Evaluate(H,Kai)
proof
consider f1 be Function of LTL_WFF,the carrier of V such that
A1: f1 is-Evaluation-for Kai and
A2: Evaluate('X' H,Kai) = f1.('X' H) by Def35;
A3: ex f2 be Function of LTL_WFF,the carrier of V st f2
is-Evaluation-for Kai & Evaluate(H,Kai) = f2.H by Def35;
A4: 'X' H is next;
then
A5: not 'X' H is negative by Lm19;
Evaluate('X' H,Kai) = (the NEXT of V).(f1.(the_argument_of('X' H)) ) by A1,A2
,A4
.= (the NEXT of V).(f1.H ) by A4,A5,Def18
.= 'X' Evaluate(H,Kai) by A1,A3,Th49;
hence thesis;
end;
theorem Th54:
Evaluate(H1 'U' H2,Kai) = Evaluate(H1,Kai) 'U' Evaluate(H2,Kai)
proof
consider f0 be Function of LTL_WFF,the carrier of V such that
A1: f0 is-Evaluation-for Kai and
A2: Evaluate(H1 'U' H2,Kai) = f0.(H1 'U' H2) by Def35;
consider f1 be Function of LTL_WFF,the carrier of V such that
A3: f1 is-Evaluation-for Kai and
A4: Evaluate(H1,Kai) = f1.H1 by Def35;
consider f2 be Function of LTL_WFF,the carrier of V such that
A5: f2 is-Evaluation-for Kai and
A6: Evaluate(H2,Kai) = f2.H2 by Def35;
A7: f0=f2 by A1,A5,Th49;
A8: H1 'U' H2 is Until;
then
A9: the_left_argument_of(H1 'U' H2) = H1 & the_right_argument_of(H1 'U' H2)
= H2 by Def19,Def20;
f0=f1 by A1,A3,Th49;
hence thesis by A1,A2,A4,A6,A7,A8,A9;
end;
theorem Th55:
Evaluate(H1 'R' H2,Kai) = Evaluate(H1,Kai) 'R' Evaluate(H2,Kai)
proof
consider f0 be Function of LTL_WFF,the carrier of V such that
A1: f0 is-Evaluation-for Kai and
A2: Evaluate(H1 'R' H2,Kai) = f0.(H1 'R' H2) by Def35;
consider f1 be Function of LTL_WFF,the carrier of V such that
A3: f1 is-Evaluation-for Kai and
A4: Evaluate(H1,Kai) = f1.H1 by Def35;
consider f2 be Function of LTL_WFF,the carrier of V such that
A5: f2 is-Evaluation-for Kai and
A6: Evaluate(H2,Kai) = f2.H2 by Def35;
A7: f0=f2 by A1,A5,Th49;
A8: H1 'R' H2 is Release;
then
A9: not H1 'R' H2 is Until by Lm21;
( not H1 'R' H2 is conjunctive)& not H1 'R' H2 is disjunctive by A8,Lm21;
then
A10: the_left_argument_of(H1 'R' H2) = H1 & the_right_argument_of(H1 'R' H2)
= H2 by A8,A9,Def19,Def20;
f0=f1 by A1,A3,Th49;
hence thesis by A1,A2,A4,A6,A7,A8,A10;
end;
::definition of concrete object of LTL model
definition
let S be non empty set;
func Inf_seq(S) -> non empty set equals
Funcs(NAT,S);
correctness;
end;
definition
let S be non empty set;
let t be sequence of S;
func CastSeq(t) -> Element of Inf_seq(S) equals
t;
correctness by FUNCT_2:8;
end;
definition
let S be non empty set;
let t be object;
assume
A1: t is Element of Inf_seq(S);
func CastSeq(t,S) -> sequence of S equals
:Def41:
t;
correctness by A1,FUNCT_2:66;
end;
definition
let S be non empty set;
let t be set;
let k be Nat;
func Shift(t,k,S) -> Element of Inf_seq(S) equals
CastSeq(CastSeq(t,S)^\k);
correctness;
end;
definition
let S be non empty set;
let t be Element of Inf_seq(S);
let k be Nat;
func Shift(t,k) -> Element of Inf_seq(S) equals
Shift(t,k,S);
correctness;
end;
Lm28: for seq being Element of Inf_seq(S) holds Shift(seq,0) = seq
proof
let seq be Element of Inf_seq(S);
set cseq = CastSeq(seq,S);
for x being object st x in NAT holds (cseq^\0).x = cseq.x
proof
let x be object;
assume x in NAT;
then reconsider x as Element of NAT;
(cseq^\0).x = cseq.(x+0) by NAT_1:def 3;
hence thesis;
end;
then Shift(seq,0) = CastSeq(cseq) by FUNCT_2:12;
hence thesis by Def41;
end;
Lm29: for seq being Element of Inf_seq(S) holds Shift(Shift(seq,k),n) = Shift(
seq,n+k)
proof
let seq be Element of Inf_seq(S);
set nk=n+k;
set t1=Shift(seq,k);
set cseq = CastSeq(seq,S);
set ct1 = CastSeq(t1,S);
A1: for m holds ct1.m = cseq.(m+k)
by Def41,NAT_1:def 3;
for m holds (ct1^\n).m = (cseq^\nk).m
proof
let m;
(ct1^\n).m = ct1.(m+n) by NAT_1:def 3
.= cseq.(m+n+k) by A1
.= cseq.(m+nk);
hence thesis by NAT_1:def 3;
end;
then for x being object st x in NAT holds (ct1^\n).x =(cseq^\nk).x;
hence thesis by FUNCT_2:12;
end;
:: definition of Not_ unary operation of Model Space.
definition
let S be non empty set;
let f be object;
func Not_0(f,S) -> Element of ModelSP(Inf_seq(S)) means
:Def44:
for t being
set st t in Inf_seq(S) holds 'not' (Castboolean (Fid(f,Inf_seq(S))).t) = TRUE
iff (Fid(it,Inf_seq(S))).t = TRUE;
existence
proof
set SEQ=Inf_seq(S);
deffunc F(set,Function of SEQ,BOOLEAN) ='not' Castboolean($2.$1);
consider IT being set such that
A1: IT in ModelSP(SEQ) & for t being set st t in SEQ holds F(t,Fid(f,
SEQ)) = TRUE iff (Fid(IT,SEQ)).t=TRUE from MODELC_1:sch 2;
take IT;
thus thesis by A1;
end;
uniqueness
proof
set SEQ=Inf_seq(S);
deffunc F(set,Function of SEQ,BOOLEAN) ='not' Castboolean($2.$1);
for g1,g2 being set st g1 in ModelSP(SEQ) & (for t being set st t in
SEQ holds F(t,Fid(f,SEQ)) =TRUE iff (Fid(g1,SEQ)).t=TRUE) & g2 in ModelSP(SEQ)
& (for t being set st t in SEQ holds F(t,Fid(f,SEQ)) =TRUE iff (Fid(g2,SEQ)).t=
TRUE) holds g1 = g2 from MODELC_1:sch 3;
hence thesis;
end;
end;
Lm30: for o1,o2 being UnOp of ModelSP(Inf_seq(S)) st
(for f being object st f in
ModelSP(Inf_seq(S)) holds o1.f = Not_0(f,S)) &
(for f being object st f in ModelSP
(Inf_seq(S)) holds o2.f = Not_0(f,S)) holds o1=o2
proof
set M = ModelSP(Inf_seq(S));
deffunc F(object) = Not_0($1,S);
for o1,o2 being UnOp of M st
(for f being object st f in M holds o1.f = F(f
)) & (for f being object st f in M holds o2.f = F(f)) holds o1=o2
from MODELC_1:
sch 5;
hence thesis;
end;
definition
let S be non empty set;
func Not_(S) -> UnOp of ModelSP(Inf_seq(S)) means
:Def45:
for f being object st f in ModelSP(Inf_seq(S)) holds it.f = Not_0(f,S);
existence
proof
set M = ModelSP(Inf_seq(S));
deffunc F(object) = Not_0($1,S);
ex o being UnOp of M st for f being object st f in M holds o.(f) = F(f)
from MODELC_1:sch 4;
hence thesis;
end;
uniqueness by Lm30;
end;
:: definition of next_ unary operation of Model Space.
definition
let S be non empty set;
let f be Function of Inf_seq(S),BOOLEAN;
let t be set;
func Next_univ(t,f) -> Element of BOOLEAN equals
:Def46:
TRUE if t is
Element of Inf_seq(S) & f.Shift(t,1,S) =TRUE otherwise FALSE;
correctness;
end;
definition
let S be non empty set;
let f be object;
func Next_0(f,S) -> Element of ModelSP(Inf_seq(S)) means
:Def47:
for t being
set st t in Inf_seq(S) holds Next_univ(t,Fid(f,Inf_seq(S)))=TRUE iff (Fid(it,
Inf_seq(S))).t=TRUE;
existence
proof
deffunc F(set,Function of Inf_seq(S),BOOLEAN) =Next_univ($1,$2);
consider IT being set such that
A1: IT in ModelSP(Inf_seq(S)) & for t being set st t in Inf_seq(S)
holds F(t,Fid (f,Inf_seq(S))) =TRUE iff (Fid(IT,Inf_seq(S))).t=TRUE from
MODELC_1:sch 2;
take IT;
thus thesis by A1;
end;
uniqueness
proof
deffunc F(set,Function of Inf_seq(S),BOOLEAN) =Next_univ($1,$2);
for g1,g2 being set st g1 in ModelSP(Inf_seq(S)) & (for t being set st
t in Inf_seq(S) holds F(t,Fid(f,Inf_seq(S))) =TRUE iff (Fid(g1,Inf_seq(S))).t=
TRUE) & g2 in ModelSP(Inf_seq(S)) & (for t being set st t in Inf_seq(S) holds F
(t,Fid(f,Inf_seq(S))) =TRUE iff (Fid(g2,Inf_seq(S))).t=TRUE) holds g1 = g2 from
MODELC_1:sch 3;
hence thesis;
end;
end;
Lm31: for o1,o2 being UnOp of ModelSP(Inf_seq(S)) st
(for f being object st f in
ModelSP(Inf_seq(S)) holds o1.f = Next_0(f,S)) &
(for f being object st f in
ModelSP(Inf_seq(S)) holds o2.f = Next_0(f,S)) holds o1=o2
proof
set M = ModelSP(Inf_seq(S));
deffunc F(object) = Next_0($1,S);
for o1,o2 being UnOp of M st
(for f being object st f in M holds o1.f = F(f
)) & (for f being object st f in M holds o2.f = F(f))
holds o1 = o2 from MODELC_1:
sch 5;
hence thesis;
end;
definition
let S be non empty set;
func Next_(S) -> UnOp of ModelSP(Inf_seq(S)) means
:Def48:
for f being object st f in ModelSP(Inf_seq(S)) holds it.f = Next_0(f,S);
existence
proof
set M = ModelSP(Inf_seq(S));
deffunc F(object) = Next_0($1,S);
ex o being UnOp of M st for f being object st f in M holds o.(f) = F(f)
from MODELC_1:sch 4;
hence thesis;
end;
uniqueness by Lm31;
end;
:: definition of And_ Binary Operation of Model Space.
definition
let S be non empty set;
let f,g be set;
func And_0(f,g,S) -> Element of ModelSP(Inf_seq(S)) means
:Def49:
for t
being set st t in Inf_seq(S) holds (Castboolean (Fid(f,Inf_seq(S))).t ) '&' (
Castboolean (Fid(g,Inf_seq(S))).t ) =TRUE iff (Fid(it,Inf_seq(S))).t=TRUE;
existence
proof
deffunc F(set,Function of Inf_seq(S),BOOLEAN,Function of Inf_seq(S),
BOOLEAN) = (Castboolean $2.$1 ) '&' (Castboolean $3.$1 );
consider IT being set such that
A1: IT in ModelSP(Inf_seq(S)) & for t being set st t in Inf_seq(S)
holds F(t,Fid( f,Inf_seq(S)),Fid(g,Inf_seq(S))) =TRUE iff (Fid(IT,Inf_seq(S))).
t=TRUE from MODELC_1:sch 6;
take IT;
thus thesis by A1;
end;
uniqueness
proof
deffunc F(set,Function of Inf_seq(S),BOOLEAN,Function of Inf_seq(S),
BOOLEAN) =(Castboolean $2.$1 ) '&' (Castboolean $3.$1 );
for h1,h2 being set st h1 in ModelSP(Inf_seq(S)) & (for t being set st
t in Inf_seq(S) holds F(t,Fid(f,Inf_seq(S)),Fid(g,Inf_seq(S))) =TRUE iff (Fid(
h1,Inf_seq(S))).t=TRUE) & h2 in ModelSP(Inf_seq(S)) & (for t being set st t in
Inf_seq(S) holds F(t,Fid(f,Inf_seq(S)),Fid(g,Inf_seq(S))) =TRUE iff (Fid(h2,
Inf_seq(S))).t=TRUE) holds h1 = h2 from MODELC_1:sch 7;
hence thesis;
end;
end;
Lm32: for o1,o2 being BinOp of ModelSP(Inf_seq(S)) st (for f,g being set st (f
in ModelSP(Inf_seq(S))) & (g in ModelSP(Inf_seq(S))) holds o1.(f,g) = And_0(f,g
,S)) & (for f,g being set st (f in ModelSP(Inf_seq(S))) & (g in ModelSP(Inf_seq
(S))) holds o2.(f,g) = And_0(f,g,S)) holds o1=o2
proof
set M = ModelSP(Inf_seq(S));
deffunc O(Element of M,Element of M) = And_0($1,$2,S);
A1: for o1,o2 being BinOp of M st (for f,g being Element of M holds o1.(f,g)
= O(f,g)) & (for f,g being Element of M holds o2.(f,g) = O(f,g)) holds o1=o2
from BINOP_2:sch 2;
for o1,o2 being BinOp of M st (for f,g being set st (f in M ) & (g in M
) holds o1.(f,g) = And_0(f,g,S)) & (for f,g being set st (f in M) & (g in M)
holds o2.(f,g) = And_0(f,g,S)) holds o1=o2
proof
let o1,o2 be BinOp of M;
assume ( for f,g being set st f in M & g in M holds o1.(f,g) = And_0(f,g,
S))& for f,g being set st f in M & g in M holds o2.(f,g) = And_0(f,g,S);
then (for f,g being Element of M holds o1.(f,g) = O(f,g))& for f,g being
Element of M holds o2.(f,g) = O(f,g);
hence thesis by A1;
end;
hence thesis;
end;
definition
let S be non empty set;
func And_(S) -> BinOp of ModelSP(Inf_seq(S)) means
:Def50:
for f,g being set
st f in ModelSP(Inf_seq(S)) & g in ModelSP(Inf_seq(S)) holds it.(f,g) = And_0(f
,g,S);
existence
proof
set M = ModelSP(Inf_seq(S));
deffunc O(Element of M,Element of M) = And_0($1,$2,S);
consider o being BinOp of M such that
A1: for f,g being Element of M holds o.(f,g) = O(f,g) from BINOP_1:sch 4;
for f,g being set st f in M & g in M holds o.(f,g) = And_0(f,g,S) by A1;
hence thesis;
end;
uniqueness by Lm32;
end;
:: definition of Until_ Binary Operation of Model Space.
definition
let S be non empty set;
let f,g be Function of Inf_seq(S),BOOLEAN;
let t be set;
func Until_univ(t,f,g,S) -> Element of BOOLEAN equals
:Def51:
TRUE if t is
Element of Inf_seq(S) & ex m being Nat st (for j being Nat st j<m holds f.Shift
(t,j,S) =TRUE ) & g.Shift(t,m,S) = TRUE otherwise FALSE;
correctness;
end;
definition
let S be non empty set;
let f,g be set;
func Until_0(f,g,S) -> Element of ModelSP(Inf_seq(S)) means
:Def52:
for t
being set st t in Inf_seq(S) holds Until_univ(t,Fid(f,Inf_seq(S)),Fid(g,Inf_seq
(S)),S)=TRUE iff (Fid(it,Inf_seq(S))).t=TRUE;
existence
proof
deffunc F(set,Function of Inf_seq(S),BOOLEAN, Function of Inf_seq(S),
BOOLEAN) =Until_univ($1,$2,$3,S);
consider IT being set such that
A1: IT in ModelSP(Inf_seq(S)) & for t being set st t in Inf_seq(S)
holds F(t,Fid (f,Inf_seq(S)),Fid(g,Inf_seq(S))) =TRUE iff (Fid(IT,Inf_seq(S))).
t=TRUE from MODELC_1:sch 6;
take IT;
thus thesis by A1;
end;
uniqueness
proof
deffunc F(set,Function of Inf_seq(S),BOOLEAN, Function of Inf_seq(S),
BOOLEAN) =Until_univ($1,$2,$3,S);
for h1,h2 being set st h1 in ModelSP(Inf_seq(S)) & (for t being set st
t in Inf_seq(S) holds F(t,Fid(f,Inf_seq(S)),Fid(g,Inf_seq(S))) = TRUE iff (Fid(
h1,Inf_seq(S))).t=TRUE) & h2 in ModelSP(Inf_seq(S)) & (for t being set st t in
Inf_seq(S) holds F(t,Fid(f,Inf_seq(S)),Fid(g,Inf_seq(S))) = TRUE iff (Fid(h2,
Inf_seq(S))).t=TRUE) holds h1 = h2 from MODELC_1:sch 7;
hence thesis;
end;
end;
Lm33: for o1,o2 being BinOp of ModelSP(Inf_seq(S)) st (for f,g being set st (f
in ModelSP(Inf_seq(S))) & (g in ModelSP(Inf_seq(S))) holds o1.(f,g) = Until_0(f
,g,S)) & (for f,g being set st (f in ModelSP(Inf_seq(S))) & (g in ModelSP(
Inf_seq(S))) holds o2.(f,g) = Until_0(f,g,S)) holds o1=o2
proof
set M = ModelSP(Inf_seq(S));
deffunc O(Element of M,Element of M) = Until_0($1,$2,S);
A1: for o1,o2 being BinOp of M st (for f,g being Element of M holds o1.(f,g)
= O(f,g)) & (for f,g being Element of M holds o2.(f,g) = O(f,g)) holds o1=o2
from BINOP_2:sch 2;
for o1,o2 being BinOp of M st (for f,g being set st f in M & g in M
holds o1.(f,g) = Until_0(f,g,S)) & (for f,g being set st f in M & g in M holds
o2.(f,g) = Until_0(f,g,S)) holds o1=o2
proof
let o1,o2 be BinOp of M;
assume ( for f,g being set st f in M & g in M holds o1.(f,g) = Until_0(f,
g,S))& for f,g being set st f in M & g in M holds o2.(f,g) = Until_0(f,g,S);
then (for f,g being Element of M holds o1.(f,g) = O(f,g))& for f,g being
Element of M holds o2.(f,g) = O(f,g);
hence thesis by A1;
end;
hence thesis;
end;
definition
let S be non empty set;
func Until_(S) -> BinOp of ModelSP(Inf_seq(S)) means
:Def53:
for f,g being
set st f in ModelSP(Inf_seq(S)) & g in ModelSP(Inf_seq(S)) holds it.(f,g) =
Until_0(f,g,S);
existence
proof
set M = ModelSP(Inf_seq(S));
deffunc O(Element of M,Element of M) = Until_0($1,$2,S);
consider o being BinOp of M such that
A1: for f,g being Element of M holds o.(f,g) = O(f,g) from BINOP_1:sch 4;
for f,g being set st f in M & g in M holds o.(f,g) = Until_0(f,g,S) by A1;
hence thesis;
end;
uniqueness by Lm33;
end;
Lm34: for o1,o2 being BinOp of ModelSP(Inf_seq(S)) st (for f,g being set st (f
in ModelSP(Inf_seq(S))) & (g in ModelSP(Inf_seq(S))) holds o1.(f,g) = (Not_(S))
.((And_(S)).((Not_(S)).f,(Not_(S)).g))) & (for f,g being set st (f in ModelSP(
Inf_seq(S))) & (g in ModelSP(Inf_seq(S))) holds o2.(f,g) = (Not_(S)).((And_(S))
.((Not_(S)).f,(Not_(S)).g))) holds o1=o2
proof
set M = ModelSP(Inf_seq(S));
deffunc O(Element of M,Element of M) = (Not_(S)).((And_(S)).((Not_(S)).$1,(
Not_(S)).$2));
A1: for o1,o2 being BinOp of M st (for f,g being Element of M holds o1.(f,g)
= O(f,g)) & (for f,g being Element of M holds o2.(f,g) = O(f,g)) holds o1=o2
from BINOP_2:sch 2;
for o1,o2 being BinOp of M st (for f,g being set st f in M & g in M
holds o1.(f,g) = (Not_(S)).((And_(S)).((Not_(S)).f,(Not_(S)).g))) & (for f,g
being set st f in M & g in M holds o2.(f,g) = (Not_(S)).((And_(S)).((Not_(S)).f
,(Not_(S)).g))) holds o1=o2
proof
let o1,o2 be BinOp of M;
assume ( for f,g being set st f in M & g in M holds o1.(f,g) = (Not_(S)).
((And_(S)).(( Not_(S)).f,(Not_(S)).g)))& for f,g being set st f in M & g in M
holds o2.(f,g) = (Not_(S)).((And_(S)).((Not_(S)).f,(Not_(S)).g));
then (for f,g being Element of M holds o1.(f,g) = O(f,g))& for f,g being
Element of M holds o2.(f,g) = O(f,g);
hence thesis by A1;
end;
hence thesis;
end;
Lm35: for o1,o2 being BinOp of ModelSP(Inf_seq(S)) st (for f,g being set st (f
in ModelSP(Inf_seq(S))) & (g in ModelSP(Inf_seq(S))) holds o1.(f,g) = (Not_(S))
.((Until_(S)).((Not_(S)).f,(Not_(S)).g))) & (for f,g being set st (f in ModelSP
(Inf_seq(S))) & (g in ModelSP(Inf_seq(S))) holds o2.(f,g) = (Not_(S)).((Until_(
S)).((Not_(S)).f,(Not_(S)).g))) holds o1=o2
proof
set M = ModelSP(Inf_seq(S));
deffunc O(Element of M,Element of M) = (Not_(S)).((Until_(S)).((Not_(S)).$1,
(Not_(S)).$2));
A1: for o1,o2 being BinOp of M st (for f,g being Element of M holds o1.(f,g)
= O(f,g)) & (for f,g being Element of M holds o2.(f,g) = O(f,g)) holds o1=o2
from BINOP_2:sch 2;
for o1,o2 being BinOp of M st (for f,g being set st f in M & g in M
holds o1.(f,g) = (Not_(S)).((Until_(S)).((Not_(S)).f,(Not_(S)).g))) & (for f,g
being set st f in M & g in M holds o2.(f,g) = (Not_(S)).((Until_(S)).((Not_(S))
.f,(Not_(S)).g))) holds o1=o2
proof
let o1,o2 be BinOp of M;
assume ( for f,g being set st f in M & g in M holds o1.(f,g) = (Not_(S)).
((Until_(S)). ((Not_(S)).f,(Not_(S)).g)))& for f,g being set st f in M & g in M
holds o2.(f, g) = (Not_(S)).((Until_(S)).((Not_(S)).f,(Not_(S)).g));
then (for f,g being Element of M holds o1.(f,g) = O(f,g))& for f,g being
Element of M holds o2.(f,g) = O(f,g);
hence thesis by A1;
end;
hence thesis;
end;
definition
let S be non empty set;
func Or_(S) -> BinOp of ModelSP(Inf_seq(S)) means
:Def54:
for f,g being set
st f in ModelSP(Inf_seq(S)) & g in ModelSP(Inf_seq(S)) holds it.(f,g) = (Not_(S
)).((And_(S)).((Not_(S)).f,(Not_(S)).g));
existence
proof
set M = ModelSP(Inf_seq(S));
deffunc O(Element of M,Element of M) = (Not_(S)).((And_(S)).((Not_(S)).$1,(
Not_(S)).$2));
consider o being BinOp of M such that
A1: for f,g being Element of M holds o.(f,g) = O(f,g) from BINOP_1:sch 4;
for f,g being set st f in M & g in M holds o.(f,g) = (Not_(S)).((And_(S)
).((Not_(S)).f,(Not_(S)).g)) by A1;
hence thesis;
end;
uniqueness by Lm34;
func Release_(S) -> BinOp of ModelSP(Inf_seq(S)) means
:Def55:
for f,g being
set st f in ModelSP(Inf_seq(S)) & g in ModelSP(Inf_seq(S)) holds it.(f,g) = (
Not_(S)).((Until_(S)).((Not_(S)).f,(Not_(S)).g));
existence
proof
set M = ModelSP(Inf_seq(S));
deffunc O(Element of M,Element of M) = (Not_(S)).((Until_(S)).((Not_(S)).$1,
(Not_(S)).$2));
consider o being BinOp of M such that
A2: for f,g being Element of M holds o.(f,g) = O(f,g) from BINOP_1:sch 4;
for f,g being set st f in M & g in M holds o.(f,g) = (Not_(S)).((Until_(
S)).((Not_(S)).f,(Not_(S)).g)) by A2;
hence thesis;
end;
uniqueness by Lm35;
end;
:: definition of concrete object of LTL model by ModelSP
definition
let S be non empty set;
let BASSIGN be non empty Subset of ModelSP(Inf_seq(S));
func Inf_seqModel(S,BASSIGN) -> LTLModelStr equals
LTLModelStr(# ModelSP(Inf_seq
(S)), BASSIGN, And_(S), Or_(S), Not_(S), Next_(S), Until_(S), Release_(S) #);
coherence;
end;
registration
let S be non empty set;
let BASSIGN be non empty Subset of ModelSP(Inf_seq(S));
cluster Inf_seqModel(S,BASSIGN) -> with_basic strict non empty;
coherence;
end;
reserve BASSIGN for non empty Subset of ModelSP(Inf_seq(S));
reserve t for Element of Inf_seq(S);
reserve f,g for Assign of Inf_seqModel(S,BASSIGN);
:: definition of correctness of Assign of Inf_seqModel(S,BASSIGN)
definition
let S be non empty set;
let BASSIGN be non empty Subset of ModelSP(Inf_seq(S));
let t be Element of Inf_seq(S);
let f be Assign of Inf_seqModel(S,BASSIGN);
pred t |= f means
(Fid(f,Inf_seq(S))).t=TRUE;
end;
notation
let S be non empty set;
let BASSIGN be non empty Subset of ModelSP(Inf_seq(S));
let t be Element of Inf_seq(S);
let f be Assign of Inf_seqModel(S,BASSIGN);
antonym t |/= f for t |= f;
end;
theorem
f 'or' g = 'not' (('not' f) '&' ('not' g)) & f 'R' g = 'not' (('not' f
) 'U' ('not' g)) by Def54,Def55;
theorem Th57:
t |= 'not' f iff t |/= f
proof
set S1 = Inf_seq(S);
A1: 'not' f = Not_0(f,S) by Def45;
thus t |= 'not'(f) implies t |/= f
proof
assume t |= ('not' f);
then (Fid('not' f,S1)).t=TRUE;
then 'not' (Castboolean (Fid(f,S1)).t) = TRUE by A1,Def44;
then (Fid(f,S1)).t = FALSE by MODELC_1:def 4;
hence thesis;
end;
assume t |/= f;
then not (Fid(f,S1)).t =TRUE;
then not Castboolean (Fid(f,S1)).t = TRUE by MODELC_1:def 4;
then Castboolean (Fid(f,S1)).t = FALSE by XBOOLEAN:def 3;
then 'not' (Castboolean (Fid(f,S1)).t) =TRUE;
then (Fid('not'(f),S1)).t =TRUE by A1,Def44;
hence thesis;
end;
theorem Th58:
t |= f '&' g iff t|=f & t|=g
proof
set S1 = Inf_seq(S);
A1: f '&' g = And_0(f,g,S) by Def50;
thus t |= f '&' g implies t|= f & t|= g
proof
assume t|= f '&' g;
then (Fid(And_0(f,g,S),S1)).t=TRUE by A1;
then
A2: (Castboolean (Fid(f,S1)).t) '&' (Castboolean (Fid(g,S1)).t) =TRUE by Def49;
then Castboolean (Fid(g,S1)).t =TRUE by XBOOLEAN:101;
then
A3: (Fid(g,S1)).t=TRUE by MODELC_1:def 4;
Castboolean (Fid(f,S1)).t =TRUE by A2,XBOOLEAN:101;
then (Fid(f,S1)).t =TRUE by MODELC_1:def 4;
hence thesis by A3;
end;
assume t|= f & t|= g;
then (Fid(f,S1)).t=TRUE & (Fid(g,S1)).t=TRUE;
then (Castboolean (Fid(f,S1)).t) '&' (Castboolean (Fid(g,S1)).t) =TRUE by
MODELC_1:def 4;
then (Fid(f '&' g,S1)).t=TRUE by A1,Def49;
hence thesis;
end;
theorem Th59:
t |= 'X' f iff Shift(t,1) |=f
proof
set S1 = Inf_seq(S);
set t1 = Shift(t,1);
set t1p = Shift(t,1,S);
A1: 'X' f = Next_0(f,S) by Def48;
thus t |= 'X' f implies t1 |=f
proof
assume t|= 'X' f;
then (Fid(Next_0(f,S),S1)).t=TRUE by A1;
then Next_univ(t,Fid(f,S1))=TRUE by Def47;
then Fid(f,S1).t1p =TRUE by Def46;
hence thesis;
end;
assume t1 |=f;
then Fid(f,S1).t1 = TRUE;
then Next_univ(t,Fid(f,S1))=TRUE by Def46;
then (Fid('X' f,S1)).t=TRUE by A1,Def47;
hence thesis;
end;
theorem Th60:
t |= f 'U' g iff ex m being Nat st (for j being Nat st j<m holds
Shift(t,j) |= f) & Shift(t,m) |= g
proof
set S1 = Inf_seq(S);
A1: f 'U' g = Until_0(f,g,S) by Def53;
A2: (ex m being Nat st (for j being Nat st j<m holds Shift(t,j) |= f) & (
Shift(t,m) |= g )) implies t |= f 'U' g
proof
assume
A3: ex m being Nat st (for j being Nat st j<m holds Shift(t,j) |= f) &
Shift(t,m) |= g;
ex m being Nat st (for j being Nat st j<m holds Fid(f,S1).Shift(t,j,S
)=TRUE) & Fid(g,S1).Shift(t,m,S) = TRUE
proof
consider m being Nat such that
A4: for j being Nat st j<m holds Shift(t,j) |= f and
A5: Shift(t,m) |= g by A3;
take m;
for j being Nat st j<m holds Fid(f,S1).Shift(t,j,S)=TRUE
proof
let j be Nat;
assume j<m;
then Shift(t,j) |= f by A4;
hence thesis;
end;
hence thesis by A5;
end;
then Until_univ(t,Fid(f,S1),Fid(g,S1),S)=TRUE by Def51;
then (Fid(f 'U' g,S1)).t=TRUE by A1,Def52;
hence thesis;
end;
t |= f 'U' g implies ex m being Nat st (for j being Nat st j<m holds
Shift(t,j) |= f) & Shift(t,m) |= g
proof
assume t|= f 'U' g;
then (Fid(Until_0(f,g,S),S1)).t=TRUE by A1;
then Until_univ(t,Fid(f,S1),Fid(g,S1),S)=TRUE by Def52;
then consider m being Nat such that
A6: for j being Nat st j<m holds Fid(f,S1).Shift(t,j,S) =TRUE and
A7: Fid(g,S1).Shift(t,m,S) = TRUE by Def51;
take m;
for j being Nat st j<m holds Shift(t,j) |= f
by A6;
hence thesis by A7;
end;
hence thesis by A2;
end;
theorem Th61:
t |= f 'or' g iff (t|= f or t|= g)
proof
t |= f 'or' g iff t|= 'not' ('not'(f) '&' 'not'(g)) by Def54;
then t |= f 'or' g iff not t|= 'not'(f) '&' 'not'(g) by Th57;
then t |= f 'or' g iff not t|= 'not'(f) or not t|= 'not'(g) by Th58;
hence thesis by Th57;
end;
theorem Th62:
t |= f 'R' g iff for m being Nat holds ((for j being Nat st j<m
holds Shift(t,j) |= 'not'(f)) implies Shift(t,m) |= g)
proof
A1: (for m being Nat holds ((for j being Nat st j<m holds Shift(t,j) |=
'not'(f)) implies Shift(t,m) |/= 'not'(g))) implies for m being Nat holds ((for
j being Nat st j<m holds Shift(t,j) |= 'not'(f)) implies Shift(t,m) |= g)
proof
assume
A2: for m being Nat holds ((for j being Nat st j<m holds Shift(t,j) |=
'not'(f)) implies Shift(t,m) |/= 'not'(g));
for m being Nat holds ((for j being Nat st j<m holds Shift(t,j) |=
'not'(f)) implies Shift(t,m) |= g)
proof
let m be Nat;
(for j being Nat st j<m holds Shift(t,j) |= 'not'(f)) implies Shift(
t,m) |/= 'not'(g) by A2;
hence thesis by Th57;
end;
hence thesis;
end;
A3: (for m being Nat holds ((for j being Nat st j<m holds Shift(t,j) |= 'not'
(f)) implies Shift(t,m) |= g)) implies for m being Nat holds ((for j being Nat
st j<m holds Shift(t,j) |= 'not'(f)) implies Shift(t,m) |/= 'not'(g))
by Th57;
t |= f 'R' g iff t|= 'not' ('not'(f) 'U' 'not'(g)) by Def55;
then t |= f 'R' g iff not t|= 'not'(f) 'U' 'not'(g) by Th57;
hence thesis by A1,A3,Th60;
end;
:: definition of correctness of LTL-formula & its basic properties.
definition
func AtomicFamily -> non empty set equals
bool atomic_LTL;
correctness;
end;
definition
let a, t be object;
func AtomicFunc(a,t) -> Element of BOOLEAN equals
:Def59:
TRUE if t in
Inf_seq(AtomicFamily) & a in (CastSeq(t,AtomicFamily)).0 otherwise FALSE;
correctness;
end;
Lm36: for f1,f2 being set st f1 in ModelSP(S) & f2 in ModelSP(S) holds Fid(f1,
S)=Fid(f2,S) implies f1=f2
proof
let f1,f2 be set such that
A1: f1 in ModelSP(S) and
A2: f2 in ModelSP(S);
assume
A3: Fid(f1,S)=Fid(f2,S);
Fid(f1,S) = f1 by A1,MODELC_1:def 41;
hence thesis by A2,A3,MODELC_1:def 41;
end;
definition
let a be object;
func AtomicAsgn(a) -> Element of ModelSP(Inf_seq(AtomicFamily)) means
:Def60:
for t being set st t in Inf_seq(AtomicFamily) holds Fid(it,Inf_seq(
AtomicFamily)).t = AtomicFunc(a,t);
existence
proof
deffunc F(object) = AtomicFunc(a,$1);
A1: for x being object st x in Inf_seq(AtomicFamily) holds F(x) in BOOLEAN;
consider IT be Function of Inf_seq(AtomicFamily),BOOLEAN such that
A2: for x being object st x in Inf_seq(AtomicFamily) holds IT.x=F(x) from
FUNCT_2:sch 2(A1);
reconsider IT as Element of Funcs(Inf_seq(AtomicFamily),BOOLEAN) by
FUNCT_2:8;
reconsider IT as Element of ModelSP(Inf_seq(AtomicFamily)) by
MODELC_1:def 40;
take IT;
for t being set st t in Inf_seq(AtomicFamily) holds Fid(IT,Inf_seq(
AtomicFamily)).t = AtomicFunc(a,t)
proof
reconsider IT as Function of Inf_seq(AtomicFamily),BOOLEAN;
let t be set such that
A3: t in Inf_seq(AtomicFamily);
Fid(IT,Inf_seq(AtomicFamily)).t = IT.t by MODELC_1:def 41
.= AtomicFunc(a,t) by A2,A3;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
for f1,f2 being Element of ModelSP(Inf_seq(AtomicFamily)) st (for t
being set st t in Inf_seq(AtomicFamily) holds Fid(f1,Inf_seq(AtomicFamily)).t =
AtomicFunc(a,t)) & (for t being set st t in Inf_seq(AtomicFamily) holds Fid(f2,
Inf_seq(AtomicFamily)).t = AtomicFunc(a,t)) holds f1=f2
proof
let f1,f2 being Element of ModelSP(Inf_seq(AtomicFamily)) such that
A4: for t being set st t in Inf_seq(AtomicFamily) holds Fid(f1,
Inf_seq(AtomicFamily)).t = AtomicFunc(a,t) and
A5: for t being set st t in Inf_seq(AtomicFamily) holds Fid(f2,
Inf_seq(AtomicFamily)).t = AtomicFunc(a,t);
for t being object st t in Inf_seq(AtomicFamily) holds Fid(f1,Inf_seq(
AtomicFamily)).t = Fid(f2,Inf_seq(AtomicFamily)).t
proof
let t being object such that
A6: t in Inf_seq(AtomicFamily);
Fid(f1,Inf_seq(AtomicFamily)).t = AtomicFunc(a,t) by A4,A6;
hence thesis by A5,A6;
end;
hence thesis by Lm36,FUNCT_2:12;
end;
hence thesis;
end;
end;
definition
func AtomicBasicAsgn -> non empty Subset of ModelSP(Inf_seq(AtomicFamily))
equals
{x where x is Element of ModelSP(Inf_seq(AtomicFamily)): ex a being set
st x = AtomicAsgn(a) };
correctness
proof
set Y = ModelSP(Inf_seq(AtomicFamily));
set z = AtomicAsgn({});
set M = {x where x is Element of ModelSP(Inf_seq(AtomicFamily)): ex a
being set st x = AtomicAsgn(a) };
A1: M c= Y
proof
let x be object;
assume x in M;
then
ex y being Element of Y st x=y & ex a being set st y = AtomicAsgn(a);
hence thesis;
end;
z in M;
hence thesis by A1;
end;
end;
definition
func AtomicKai -> Function of atomic_LTL,the BasicAssign of Inf_seqModel(
AtomicFamily,AtomicBasicAsgn) means
:Def62:
for a being set st a in atomic_LTL holds it.a = AtomicAsgn(a);
existence
proof
deffunc F(object) = AtomicAsgn($1);
A1: for a being object st a in atomic_LTL holds F(a) in the BasicAssign of
Inf_seqModel(AtomicFamily,AtomicBasicAsgn);
consider IT be Function of atomic_LTL,the BasicAssign of Inf_seqModel(
AtomicFamily,AtomicBasicAsgn) such that
A2: for a being object st a in atomic_LTL holds IT.a=F(a) from FUNCT_2:sch
2(A1);
take IT;
thus thesis by A2;
end;
uniqueness
proof
for f1,f2 being Function of atomic_LTL,the BasicAssign of Inf_seqModel(
AtomicFamily,AtomicBasicAsgn) st (for a being set st a in atomic_LTL holds f1.a
= AtomicAsgn(a)) & (for a being set st a in atomic_LTL holds f2.a = AtomicAsgn(
a)) holds f1=f2
proof
let f1,f2 be Function of atomic_LTL,the BasicAssign of Inf_seqModel(
AtomicFamily,AtomicBasicAsgn) such that
A3: for a being set st a in atomic_LTL holds f1.a = AtomicAsgn(a) and
A4: for a being set st a in atomic_LTL holds f2.a = AtomicAsgn(a);
for a being object st a in atomic_LTL holds f1.a = f2.a
proof
let a be object such that
A5: a in atomic_LTL;
f1.a= AtomicAsgn(a) by A3,A5;
hence thesis by A4,A5;
end;
hence thesis by FUNCT_2:12;
end;
hence thesis;
end;
end;
definition
let r be Element of Inf_seq(AtomicFamily);
let H be LTL-formula;
pred r|= H means
:Def63:
r|= Evaluate(H,AtomicKai);
end;
notation
let r be Element of Inf_seq(AtomicFamily);
let H be LTL-formula;
antonym r|/= H for r|= H;
end;
definition
let r be Element of Inf_seq(AtomicFamily);
let W be Subset of LTL_WFF;
pred r|= W means
for H be LTL-formula st H in W holds r|= H;
end;
notation
let r be Element of Inf_seq(AtomicFamily);
let W be Subset of LTL_WFF;
antonym r|/= W for r|= W;
end;
definition
let W be Subset of LTL_WFF;
func 'X' W -> Subset of LTL_WFF equals
{x where x is LTL-formula:ex u being
LTL-formula st u in W & x='X' u};
correctness
proof
set X = {x where x is LTL-formula: ex u being LTL-formula st u in W & x=
'X' u};
X c= LTL_WFF
proof
let y be object;
assume y in X;
then
ex x being LTL-formula st y=x & ex u being LTL-formula st u in W & x=
'X' u;
hence thesis by Th1;
end;
hence thesis;
end;
end;
reserve r for Element of Inf_seq(AtomicFamily);
theorem
H is atomic implies (r |= H iff H in (CastSeq(r,AtomicFamily)).0)
proof
assume
A1: H is atomic;
then
A2: H in atomic_LTL;
A3: r |= H iff r|= Evaluate(H,AtomicKai);
ex f be Function of LTL_WFF, the carrier of Inf_seqModel( AtomicFamily,
AtomicBasicAsgn) st f is-Evaluation-for AtomicKai & Evaluate(H, AtomicKai) = f.
H by Def35;
then Evaluate(H,AtomicKai) = AtomicKai.H by A1
.= AtomicAsgn(H) by A2,Def62;
then r |= H iff (Fid(AtomicAsgn(H),Inf_seq(AtomicFamily))).r=TRUE by A3;
then r |= H iff AtomicFunc(H,r) = TRUE by Def60;
hence thesis by Def59;
end;
theorem Th64:
r|= 'not' H iff r|/= H
proof
r|= 'not' H iff r|= 'not' Evaluate(H,AtomicKai) by Th50;
then r|= 'not' H iff r|/= Evaluate(H,AtomicKai) by Th57;
hence thesis;
end;
theorem Th65:
r|= H1 '&' H2 iff r|= H1 & r|= H2
proof
r|= H1 '&' H2 iff r|= Evaluate(H1,AtomicKai) '&' Evaluate(H2,AtomicKai)
by Th51;
then
r|= H1 '&' H2 iff r|= Evaluate(H1,AtomicKai) & r|= Evaluate(H2,AtomicKai
) by Th58;
hence thesis;
end;
theorem Th66:
r|= H1 'or' H2 iff r|= H1 or r|= H2
proof
r|= H1 'or' H2 iff r|= Evaluate(H1,AtomicKai) 'or' Evaluate(H2,AtomicKai
) by Th52;
then r|= H1 'or' H2 iff r|= Evaluate(H1,AtomicKai) or r|= Evaluate(H2,
AtomicKai) by Th61;
hence thesis;
end;
theorem Th67:
r|= 'X' H iff Shift(r,1)|=H
proof
r|= 'X' H iff r|= 'X' Evaluate(H,AtomicKai) by Th53;
then r|= 'X' H iff Shift(r,1)|= Evaluate(H,AtomicKai) by Th59;
hence thesis;
end;
theorem Th68:
r|= H1 'U' H2 iff ex m being Nat st (for j being Nat st j<m
holds Shift(r,j) |= H1) & Shift(r,m) |= H2
proof
A1: (ex m being Nat st (for j being Nat st j<m holds Shift(r,j) |= Evaluate(
H1,AtomicKai)) & (Shift(r,m) |= Evaluate(H2,AtomicKai) )) implies ex m being
Nat st (for j being Nat st j<m holds Shift(r,j) |= H1) & Shift(r,m) |= H2
proof
assume ex m being Nat st (for j being Nat st j<m holds Shift(r,j) |=
Evaluate(H1,AtomicKai)) & Shift(r,m) |= Evaluate(H2,AtomicKai);
then consider m be Nat such that
A2: for j being Nat st j<m holds Shift(r,j) |= Evaluate(H1,AtomicKai) and
A3: Shift(r,m) |= Evaluate(H2,AtomicKai);
take m;
for j being Nat st j<m holds Shift(r,j) |= H1
by A2;
hence thesis by A3;
end;
A4: (ex m being Nat st (for j being Nat st j<m holds Shift(r,j) |= H1) & (
Shift(r,m) |= H2)) implies ex m being Nat st (for j being Nat st j<m holds
Shift(r,j) |= Evaluate(H1,AtomicKai)) & Shift(r,m) |= Evaluate(H2,AtomicKai)
proof
assume ex m being Nat st (for j being Nat st j<m holds Shift(r,j) |= H1)
& Shift(r,m) |= H2;
then consider m be Nat such that
A5: for j being Nat st j<m holds Shift(r,j) |= H1 and
A6: Shift(r,m) |= H2;
take m;
for j being Nat st j<m holds Shift(r,j) |= Evaluate(H1,AtomicKai)
by A5,Def63;
hence thesis by A6;
end;
r|= H1 'U' H2 iff r|= Evaluate(H1,AtomicKai) 'U' Evaluate(H2,AtomicKai)
by Th54;
hence thesis by A1,A4,Th60;
end;
theorem
r|= H1 'R' H2 iff for m being Nat holds ((for j being Nat st j<m holds
Shift(r,j) |= 'not' H1) implies Shift(r,m) |= H2)
proof
A1: (for m being Nat holds ((for j being Nat st j<m holds Shift(r,j) |=
'not' Evaluate(H1,AtomicKai)) implies Shift(r,m) |= Evaluate(H2,AtomicKai)) )
implies for m being Nat holds ((for j being Nat st j<m holds Shift(r,j) |=
'not' H1) implies Shift(r,m) |= H2)
proof
assume
A2: for m being Nat holds ((for j being Nat st j<m holds Shift(r,j) |=
'not' Evaluate(H1,AtomicKai)) implies Shift(r,m) |= Evaluate(H2,AtomicKai));
for m being Nat holds ((for j being Nat st j<m holds Shift(r,j) |=
'not' H1) implies Shift(r,m) |= H2 )
proof
let m be Nat;
(for j being Nat st j<m holds Shift(r,j) |= 'not' H1) implies Shift(
r,m) |= H2
proof
assume
A3: for j being Nat st j<m holds Shift(r,j) |= 'not' H1;
for j being Nat st j<m holds Shift(r,j) |= 'not' Evaluate(H1,
AtomicKai)
proof
let j be Nat;
assume j<m;
then Shift(r,j) |= 'not' H1 by A3;
then Shift(r,j) |= Evaluate('not' H1,AtomicKai);
hence thesis by Th50;
end;
then Shift(r,m) |= Evaluate(H2,AtomicKai) by A2;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A4: (for m being Nat holds ((for j being Nat st j<m holds Shift(r,j) |=
'not' H1) implies Shift(r,m) |= H2)) implies for m being Nat holds ((for j
being Nat st j<m holds Shift(r,j) |= 'not' Evaluate(H1,AtomicKai)) implies
Shift(r,m) |= Evaluate(H2,AtomicKai))
proof
assume
A5: for m being Nat holds ((for j being Nat st j<m holds Shift(r,j) |=
'not' H1) implies Shift(r,m) |= H2);
for m being Nat holds ((for j being Nat st j<m holds Shift(r,j) |=
'not' Evaluate(H1,AtomicKai)) implies Shift(r,m) |= Evaluate(H2,AtomicKai))
proof
let m be Nat;
(for j being Nat st j<m holds Shift(r,j) |= 'not' Evaluate(H1,
AtomicKai)) implies Shift(r,m) |= Evaluate(H2,AtomicKai)
proof
assume
A6: for j being Nat st j<m holds Shift(r,j) |= 'not' Evaluate(H1,
AtomicKai);
for j being Nat st j<m holds Shift(r,j) |= 'not' H1
proof
let j be Nat;
assume j<m;
then Shift(r,j) |= 'not' Evaluate(H1,AtomicKai) by A6;
then Shift(r,j) |= Evaluate('not' H1,AtomicKai) by Th50;
hence thesis;
end;
then Shift(r,m) |= H2 by A5;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
r|= H1 'R' H2 iff r|= Evaluate(H1,AtomicKai) 'R' Evaluate(H2,AtomicKai)
by Th55;
hence thesis by A1,A4,Th62;
end;
theorem Th70:
r|= 'not' (H1 'or' H2) iff r |= ('not' H1) '&' ('not' H2)
proof
r|= 'not' (H1 'or' H2) iff r|/= H1 'or' H2 by Th64;
then r|= 'not' (H1 'or' H2) iff not (r |= H1 or r |= H2) by Th66;
then r|= 'not' (H1 'or' H2) iff r |= 'not' H1 & r |= 'not' H2 by Th64;
hence thesis by Th65;
end;
theorem Th71:
r|= 'not' (H1 '&' H2) iff r |= ('not' H1) 'or' ('not' H2)
proof
r|= 'not' (H1 '&' H2) iff r|/= H1 '&' H2 by Th64;
then r|= 'not' (H1 '&' H2) iff not (r |= H1 & r |= H2) by Th65;
then r|= 'not' (H1 '&' H2) iff (r |= 'not' H1 or r |= 'not' H2) by Th64;
hence thesis by Th66;
end;
theorem Th72:
r|= H1 'R' H2 iff r |= 'not' ( ('not' H1) 'U' ('not' H2))
proof
set H01= Evaluate(H1,AtomicKai);
set H02= Evaluate(H2,AtomicKai);
set nH1= 'not' H1;
set nH2= 'not' H2;
r|= H1 'R' H2 iff r|= H01 'R' H02 by Th55;
then
A1: r|= H1 'R' H2 iff r |= 'not' ( ('not' H01) 'U' ('not' H02)) by Def55;
'not' H01 = Evaluate(nH1,AtomicKai) & 'not' H02 = Evaluate(nH2,AtomicKai
) by Th50;
then r |= nH1 'U' nH2 iff r |= 'not' H01 'U' 'not' H02 by Th54;
hence thesis by A1,Th57,Th64;
end;
theorem
r |/= 'not' H iff r |= H by Th64;
theorem Th74:
r |= 'X'('not' H) iff r |='not' ('X' H)
proof
r |= 'X'('not' H) iff Shift(r,1)|='not' H by Th67;
then r |= 'X'('not' H) iff Shift(r,1)|/= H by Th64;
then r |= 'X'('not' H) iff not r|= 'X' H by Th67;
hence thesis by Th64;
end;
theorem Th75:
r|= H1 'U' H2 iff r|=H2 'or' (H1 '&' ('X' (H1 'U' H2)))
proof
A1: r|=H2 'or' (H1 '&' ('X' (H1 'U' H2))) implies r|= H1 'U' H2
proof
assume
A2: r|=H2 'or' (H1 '&' ('X' (H1 'U' H2)));
now
per cases by A2,Th66;
suppose
A3: r|=H2;
ex m being Nat st (for j being Nat st j<m holds Shift(r,j) |= H1)
& Shift(r,m) |= H2
proof
take 0;
thus thesis by A3,Lm28;
end;
hence thesis by Th68;
end;
suppose
A4: r|=H1 '&' ('X' (H1 'U' H2));
set r1 = Shift(r,1);
r|='X' (H1 'U' H2) by A4,Th65;
then Shift(r,1) |= H1 'U' H2 by Th67;
then consider m be Nat such that
A5: for j being Nat st j<m holds Shift(r1,j) |= H1 and
A6: Shift(r1,m) |= H2 by Th68;
set m1= m+1;
A7: r|=H1 by A4,Th65;
A8: for j being Nat st j<m1 holds Shift(r,j) |= H1
proof
let j be Nat such that
A9: j<m1;
now
per cases;
suppose
j=0;
hence thesis by A7,Lm28;
end;
suppose
A10: j>0;
set j1= j-1;
reconsider j1 as Nat by A10,NAT_1:20;
j-1<m1-1 by A9,XREAL_1:14;
then Shift(r1,j1) |= H1 by A5;
then Shift(r,j1+1) |= H1 by Lm29;
hence thesis;
end;
end;
hence thesis;
end;
Shift(r,m1) |= H2 by A6,Lm29;
hence thesis by A8,Th68;
end;
end;
hence thesis;
end;
r|= H1 'U' H2 implies r|=H2 'or' (H1 '&' ('X' (H1 'U' H2)))
proof
assume r|= H1 'U' H2;
then consider m be Nat such that
A11: for j being Nat st j<m holds Shift(r,j) |= H1 and
A12: Shift(r,m) |= H2 by Th68;
per cases;
suppose
m = 0;
then r|=H2 by A12,Lm28;
hence thesis by Th66;
end;
suppose
A13: m >0;
set k = m-1;
reconsider k as Nat by A13,NAT_1:20;
set r1= Shift(r,1);
A14: for j being Nat st j<k holds Shift(r1,j) |= H1
proof
let j be Nat;
assume j<k;
then
A15: j+1<k+1 by XREAL_1:8;
Shift(r,j+1) = Shift(r1,j) by Lm29;
hence thesis by A11,A15;
end;
Shift(r,k+1) = Shift(r1,k) by Lm29;
then r1|= H1 'U' H2 by A12,A14,Th68;
then
A16: r |= 'X' (H1 'U' H2) by Th67;
Shift(r,0)= r by Lm28;
then r|=H1 by A11,A13;
then r |= H1 '&' ('X' (H1 'U' H2) ) by A16,Th65;
hence thesis by Th66;
end;
end;
hence thesis by A1;
end;
theorem
r|= H1 'R' H2 iff r|=(H1 '&' H2) 'or' (H2 '&' ('X' (H1 'R' H2)))
proof
set nH1= 'not' H1;
set nH2= 'not' H2;
r|= H1 'R' H2 iff r |= 'not' ( nH1 'U' nH2) by Th72;
then r|= H1 'R' H2 iff r |/= nH1 'U' nH2 by Th64;
then r|= H1 'R' H2 iff r |/= nH2 'or' (nH1 '&' ('X' (nH1 'U' nH2))) by Th75;
then r|= H1 'R' H2 iff r |= 'not'( nH2 'or' (nH1 '&' ('X' (nH1 'U' nH2))) )
by Th64;
then
r|= H1 'R' H2 iff r |= 'not'(nH2) '&' ('not'(nH1 '&' ('X' (nH1 'U' nH2))
)) by Th70;
then
r|= H1 'R' H2 iff r |= 'not'(nH2) & r |= 'not'(nH1 '&' ('X' (nH1 'U' nH2
))) by Th65;
then r|= H1 'R' H2 iff r |/= nH2 & r |= 'not'(nH1) 'or' ('not'('X' (nH1 'U'
nH2))) by Th64,Th71;
then
r|= H1 'R' H2 iff r |= H2 & ( r |= 'not'(nH1) or r |='not'('X' (nH1 'U'
nH2))) by Th64,Th66;
then
r|= H1 'R' H2 iff r |= H2 & ( r |/= nH1 or r |='X' ('not'(nH1 'U' nH2)))
by Th64,Th74;
then r|= H1 'R' H2 iff r |= H2 & ( r |/= nH1 or Shift(r,1) |='not'(nH1 'U'
nH2)) by Th67;
then r|= H1 'R' H2 iff r |= H2 & ( r |= H1 or Shift(r,1)|=H1 'R' H2 ) by Th64
,Th72;
then r|= H1 'R' H2 iff r |= H2 & ( r |= H1 or r |='X' (H1 'R' H2)) by Th67;
then r|= H1 'R' H2 iff r |= H1 '&' H2 or r |= H2 '&' 'X' (H1 'R' H2) by Th65;
hence thesis by Th66;
end;
reserve W for Subset of LTL_WFF;
theorem
r |= 'X' W iff Shift(r,1) |=W
proof
A1: Shift(r,1) |=W implies r |= 'X' W
proof
assume
A2: Shift(r,1) |=W;
A3: for u be LTL-formula st u in W holds r|= 'X' u
by A2,Th67;
for H be LTL-formula st H in 'X' W holds r |= H
proof
let H being LTL-formula;
assume H in 'X' W;
then
ex x being LTL-formula st H = x & ex u being LTL-formula st u in W &
x='X' u;
hence thesis by A3;
end;
hence thesis;
end;
r |= 'X' W implies Shift(r,1) |=W
proof
assume
A4: r |= 'X' W;
for H be LTL-formula st H in W holds Shift(r,1) |= H
proof
let H being LTL-formula;
set u = 'X' H;
assume H in W;
then u in 'X' W;
then r |= u by A4;
hence thesis by Th67;
end;
hence thesis;
end;
hence thesis by A1;
end;
:: theorems for external articles
theorem
(H is atomic implies (not H is negative) & (not H is conjunctive) & (
not H is disjunctive) & (not H is next) & (not H is Until) & not H is Release )
& (H is negative implies (not H is atomic) & (not H is conjunctive) & (not H is
disjunctive) & (not H is next) & (not H is Until) & not H is Release ) & (H is
conjunctive implies (not H is atomic) & (not H is negative) & (not H is
disjunctive) & (not H is next) & (not H is Until) & not H is Release ) & (H is
disjunctive implies (not H is atomic) & (not H is negative) & (not H is
conjunctive) & (not H is next) & (not H is Until) & not H is Release ) & (H is
next implies (not H is atomic) & (not H is negative) & (not H is conjunctive) &
(not H is disjunctive) & (not H is Until) & not H is Release ) & (H is Until
implies (not H is atomic) & (not H is negative) & (not H is conjunctive) & (not
H is disjunctive) & (not H is next) & not H is Release ) & (H is Release
implies (not H is atomic) & (not H is negative) & (not H is conjunctive) & (not
H is disjunctive) & (not H is next) & not H is Until ) by Lm16,Lm17,Lm18,Lm19
,Lm20,Lm21;
theorem
for t being Element of Inf_seq(S) holds Shift(t,0)=t by Lm28;
theorem
for seq being Element of Inf_seq(S) holds Shift(Shift(seq,k),n) =
Shift(seq,n+k) by Lm29;
theorem
for seq being sequence of S holds CastSeq(CastSeq(seq),S) = seq by Def41;
theorem
for seq being Element of Inf_seq(S) holds CastSeq(CastSeq(seq,S)) =
seq by Def41;
theorem
H in W & 'not' H in W implies r |/=W
proof
assume
A1: H in W & 'not' H in W;
now
assume r |=W;
then r |= H & r |='not' H by A1;
hence contradiction by Th64;
end;
hence thesis;
end;