modelc_2.miz
begin
definition
let x be
object;
::
MODELC_2:def1
func
CastNat (x) ->
Nat equals
:
Def1: x if x is
Nat
otherwise
0 ;
correctness ;
end
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 ;
definition
let n;
::
MODELC_2:def2
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;
::
MODELC_2:def3
func
'not' p ->
FinSequence of
NAT equals (
<*
0 *>
^ p);
coherence ;
let q;
::
MODELC_2:def4
func p
'&' q ->
FinSequence of
NAT equals ((
<*1*>
^ p)
^ q);
coherence ;
::
MODELC_2:def5
func p
'or' q ->
FinSequence of
NAT equals ((
<*2*>
^ p)
^ q);
coherence ;
end
definition
let p;
::
MODELC_2:def6
func
'X' p ->
FinSequence of
NAT equals (
<*3*>
^ p);
coherence ;
let q;
::
MODELC_2:def7
func p
'U' q ->
FinSequence of
NAT equals ((
<*4*>
^ p)
^ q);
coherence ;
::
MODELC_2:def8
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;
definition
::
MODELC_2:def9
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 be
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 ;
::
MODELC_2:def10
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 ::
MODELC_2:1
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;
::
MODELC_2:def11
attr H is
atomic means ex n st H
= (
atom. n);
::
MODELC_2:def12
attr H is
negative means ex H1 st H
= (
'not' H1);
::
MODELC_2:def13
attr H is
conjunctive means ex F, G st H
= (F
'&' G);
::
MODELC_2:def14
attr H is
disjunctive means ex F, G st H
= (F
'or' G);
::
MODELC_2:def15
attr H is
next means ex H1 st H
= (
'X' H1);
::
MODELC_2:def16
attr H is
Until means ex F, G st H
= (F
'U' G);
::
MODELC_2:def17
attr H is
Release means ex F, G st H
= (F
'R' G);
end
theorem ::
MODELC_2:2
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);
A2: (3
+
0 )
< (3
+ (3
+ n)) & (4
+
0 )
< (4
+ (2
+ n)) by
XREAL_1: 8;
A3: (5
+
0 )
< (5
+ (1
+ n)) by
XREAL_1: 8;
(1
+
0 )
< (1
+ (5
+ n)) & (2
+
0 )
< (2
+ (4
+ n)) by
XREAL_1: 8;
hence thesis by
A1,
A2,
A3,
FINSEQ_1: 40;
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 ::
MODELC_2:3
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 be
Nat st (for k be
Nat st k
< n holds for H, F, sq st (
len H)
= k & H
= (F
^ sq) holds H
= F) holds for H, F, sq st (
len H)
= n & H
= (F
^ sq) holds H
= F
proof
let n be
Nat such that
A1: for k be
Nat st k
< n holds 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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 be
Nat st for n be
Nat st n
< k holds
P[n] holds
P[k];
A89: for n be
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,
Lm9;
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;
::
MODELC_2:def18
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;
::
MODELC_2:def19
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;
::
MODELC_2:def20
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 ::
MODELC_2:4
H is
negative implies H
= (
'not' (
the_argument_of H)) by
Def18;
theorem ::
MODELC_2:5
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 ::
MODELC_2:6
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 ::
MODELC_2:7
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 ::
MODELC_2:8
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 ::
MODELC_2:9
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 ::
MODELC_2:10
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 ::
MODELC_2:11
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;
definition
let H, F;
::
MODELC_2:def21
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 ::
MODELC_2:12
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 ::
MODELC_2:13
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 ::
MODELC_2:14
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 ::
MODELC_2:15
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 ::
MODELC_2:16
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 ::
MODELC_2:17
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 ::
MODELC_2:18
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 ::
MODELC_2:19
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 ::
MODELC_2:20
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 ::
MODELC_2:21
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 ::
MODELC_2:22
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 ::
MODELC_2:23
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 ::
MODELC_2:24
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 ::
MODELC_2:25
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 ::
MODELC_2:26
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;
reserve L,L9 for
FinSequence;
definition
let H, F;
::
MODELC_2:def22
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 holds 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 by
FINSEQ_1:def 8;
thus thesis;
end;
end
theorem ::
MODELC_2:27
H
is_subformula_of H;
definition
let H, F;
::
MODELC_2:def23
pred H
is_proper_subformula_of F means H
is_subformula_of F & H
<> F;
irreflexivity ;
end
theorem ::
MODELC_2:28
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 ::
MODELC_2:29
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 by
FINSEQ_1: 44;
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 by
FINSEQ_1: 44;
thus thesis by
A1;
end;
assume H
= F;
then (
len H)
= (
len F);
hence contradiction by
A1,
Th28;
end;
theorem ::
MODELC_2:30
(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 ::
MODELC_2:31
(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 ::
MODELC_2:32
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 holds 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,
NAT_1: 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 ::
MODELC_2:33
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 holds 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 ::
MODELC_2:34
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 holds 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 holds 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 ::
MODELC_2:35
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 ::
MODELC_2:36
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 ::
MODELC_2:37
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 holds 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 be
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 ::
MODELC_2:38
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 holds 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 be
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 ::
MODELC_2:39
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 ::
MODELC_2:40
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 ::
MODELC_2:41
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 ::
MODELC_2:42
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 ::
MODELC_2:43
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 ::
MODELC_2:44
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;
definition
let H;
::
MODELC_2:def24
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 be
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 ::
MODELC_2:45
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 ::
MODELC_2:46
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 ::
MODELC_2:47
a is
Subset of (
Subformulae H) implies a is
Subset of
LTL_WFF
proof
assume
A1: a is
Subset of (
Subformulae H);
for x be
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 ::
MODELC_2:sch1
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];
defpred
Q[
Nat] means for H st (
len H)
= $1 holds P[H];
A4: for n be
Nat st for k be
Nat st k
< n holds
Q[k] holds
Q[n]
proof
let n be
Nat such that
A5: for k be
Nat st k
< n holds 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 be
Nat holds
Q[n] from
NAT_1:sch 4(
A4);
let H;
(
len H)
= (
len H);
hence thesis by
A11;
end;
scheme ::
MODELC_2:sch2
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];
defpred
Q[
Nat] means for H st (
len H)
= $1 holds P[H];
A2: for n be
Nat st for k be
Nat st k
< n holds
Q[k] holds
Q[n]
proof
let n be
Nat such that
A3: for k be
Nat st k
< n holds 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 be
Nat holds
Q[n] from
NAT_1:sch 4(
A2);
let H;
(
len H)
= (
len H);
hence thesis by
A5;
end;
definition
let x be
object;
::
MODELC_2:def25
func
CastLTL (x) ->
LTL-formula equals
:
Def25: x if x
in
LTL_WFF
otherwise (
atom.
0 );
correctness by
Th1;
end
definition
struct (
OrthoLattStr)
LTLModelStr
(# the
carrier ->
set,
the
BasicAssign ->
Subset of the carrier,
the
L_meet ->
BinOp of the carrier,
the
L_join ->
BinOp of the carrier,
the
Compl ->
UnOp of the carrier,
the
NEXT ->
UnOp of the carrier,
the
UNTIL ->
BinOp of the carrier,
the
RELEASE ->
BinOp of the carrier #)
attr strict
strict;
end
definition
let V be
LTLModelStr;
mode
Assign of V is
Element of the
carrier of V;
end
definition
::
MODELC_2:def26
func
atomic_LTL ->
Subset of
LTL_WFF equals { x where x be
LTL-formula : x is
atomic };
correctness
proof
set X = { x where x be
LTL-formula : x is
atomic };
X
c=
LTL_WFF
proof
let y be
object;
assume y
in X;
then ex x be
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;
::
MODELC_2:def27
pred f
is-Evaluation-for Kai means for H be
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;
::
MODELC_2:def28
pred f
is-PreEvaluation-for n,Kai means
:
Def28: for H be
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;
::
MODELC_2:def29
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;
::
MODELC_2:def30
attr C is
with_basic means
:
Def30: the
BasicAssign of C is non
empty;
end
definition
::
MODELC_2:def31
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 be
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 be
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 be
LTL-formula st (
len H)
<= $1 holds (f1
. H)
= (f2
. H));
A1: for k be
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 be
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 be
Function of
LTL_WFF , the
carrier of V st f
is-PreEvaluation-for ($1,Kai);
A1: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
P[k];
then
consider h be
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 be
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 be
object st H
in
LTL_WFF holds (f
. H)
=
F(H) from
FUNCT_2:sch 2(
A3);
take f;
A20: for H be
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 be
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 be
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;
::
MODELC_2:def32
func
EvalSet (V,Kai,n) -> non
empty
set equals { h where h be
Function of
LTL_WFF , the
carrier of V : h
is-PreEvaluation-for (n,Kai) };
correctness
proof
set X = { h where h be
Function of
LTL_WFF , the
carrier of V : h
is-PreEvaluation-for (n,Kai) };
consider h be
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;
::
MODELC_2:def33
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;
::
MODELC_2:def34
func
EvalFamily (V,Kai) -> non
empty
set means
:
Def34: for p be
set holds p
in it iff p
in (
bool (
Funcs (
LTL_WFF ,the
carrier of V))) & ex n be
Nat st p
= (
EvalSet (V,Kai,n));
existence
proof
defpred
Q[
set] means ex n be
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 be
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 be
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 be
Nat st $1
= (
EvalSet (V,Kai,n));
for X1,X2 be
set st (for x be
set holds x
in X1 iff
P[x]) & (for x be
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 be
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 ::
MODELC_2:48
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 be
set st X
in M holds X
<>
{}
proof
let X be
set;
assume X
in M;
then ex n be
Nat st X
= (
EvalSet (V,Kai,n)) by
Def34;
hence thesis;
end;
then
consider Choice be
Function such that (
dom Choice)
= M and
A1: for X be
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 be
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 be
Function of
LTL_WFF , the
carrier of V st Y
= h & h
is-PreEvaluation-for (n,Kai);
hence thesis;
end;
A4: for n be
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 be
sequence of (
Funcs (
LTL_WFF ,the
carrier of V)) such that
A5: for n be
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 be
object st H
in
LTL_WFF holds
G(H)
in the
carrier of V by
FUNCT_2: 5;
consider f be
Function of
LTL_WFF , the
carrier of V such that
A7: for H be
object st H
in
LTL_WFF holds (f
. H)
=
G(H) from
FUNCT_2:sch 2(
A6);
take f;
for n be
Nat holds f
is-PreEvaluation-for (n,Kai)
proof
defpred
P[
Nat] means f
is-PreEvaluation-for ($1,Kai);
A8: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat such that
A9:
P[k];
for H be
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);
A12: H
in
LTL_WFF by
Th1;
then (f1
. (
len (
CastLTL H)))
= (f1
. (
len H)) by
Def25
.=
F(len) by
A5;
then
A13: (
CastEval (V,(f1
. (
len (
CastLTL H))),v0))
=
F(len) 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 be
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 be
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 be
Nat holds
P[n] from
NAT_1:sch 2(
A38,
A8);
hence thesis;
end;
hence thesis by
Lm26;
end;
theorem ::
MODELC_2:49
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 be
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;
::
MODELC_2:def35
func
Evaluate (H,Kai) ->
Assign of V means
:
Def35: ex f be
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;
::
MODELC_2:def36
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;
::
MODELC_2:def37
func f
'U' g ->
Assign of V equals (the
UNTIL of V
. (f,g));
correctness ;
::
MODELC_2:def38
func f
'R' g ->
Assign of V equals (the
RELEASE of V
. (f,g));
correctness ;
end
theorem ::
MODELC_2:50
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 ::
MODELC_2:51
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 ::
MODELC_2:52
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 ::
MODELC_2:53
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 ::
MODELC_2:54
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 ::
MODELC_2:55
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
let S be non
empty
set;
::
MODELC_2:def39
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;
::
MODELC_2:def40
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);
::
MODELC_2:def41
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;
::
MODELC_2:def42
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;
::
MODELC_2:def43
func
Shift (t,k) ->
Element of (
Inf_seq S) equals (
Shift (t,k,S));
correctness ;
end
Lm28: for seq be
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 be
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 be
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 be
object st x
in
NAT holds ((ct1
^\ n)
. x)
= ((cseq
^\ nk)
. x);
hence thesis by
FUNCT_2: 12;
end;
definition
let S be non
empty
set;
let f be
object;
::
MODELC_2:def44
func
Not_0 (f,S) ->
Element of (
ModelSP (
Inf_seq S)) means
:
Def44: for t be
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 be
set such that
A1: IT
in (
ModelSP SEQ) & for t be
set st t
in SEQ holds
F(t,Fid)
=
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 be
set st g1
in (
ModelSP SEQ) & (for t be
set st t
in SEQ holds
F(t,Fid)
=
TRUE iff ((
Fid (g1,SEQ))
. t)
=
TRUE ) & g2
in (
ModelSP SEQ) & (for t be
set st t
in SEQ holds
F(t,Fid)
=
TRUE iff ((
Fid (g2,SEQ))
. t)
=
TRUE ) holds g1
= g2 from
MODELC_1:sch 3;
hence thesis;
end;
end
Lm30: for o1,o2 be
UnOp of (
ModelSP (
Inf_seq S)) st (for f be
object st f
in (
ModelSP (
Inf_seq S)) holds (o1
. f)
= (
Not_0 (f,S))) & (for f be
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 be
UnOp of M st (for f be
object st f
in M holds (o1
. f)
=
F(f)) & (for f be
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;
::
MODELC_2:def45
func
Not_ (S) ->
UnOp of (
ModelSP (
Inf_seq S)) means
:
Def45: for f be
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 be
UnOp of M st for f be
object st f
in M holds (o
. f)
=
F(f) from
MODELC_1:sch 4;
hence thesis;
end;
uniqueness by
Lm30;
end
definition
let S be non
empty
set;
let f be
Function of (
Inf_seq S),
BOOLEAN ;
let t be
set;
::
MODELC_2:def46
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;
::
MODELC_2:def47
func
Next_0 (f,S) ->
Element of (
ModelSP (
Inf_seq S)) means
:
Def47: for t be
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 be
set such that
A1: IT
in (
ModelSP (
Inf_seq S)) & for t be
set st t
in (
Inf_seq S) holds
F(t,Fid)
=
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 be
set st g1
in (
ModelSP (
Inf_seq S)) & (for t be
set st t
in (
Inf_seq S) holds
F(t,Fid)
=
TRUE iff ((
Fid (g1,(
Inf_seq S)))
. t)
=
TRUE ) & g2
in (
ModelSP (
Inf_seq S)) & (for t be
set st t
in (
Inf_seq S) holds
F(t,Fid)
=
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 be
UnOp of (
ModelSP (
Inf_seq S)) st (for f be
object st f
in (
ModelSP (
Inf_seq S)) holds (o1
. f)
= (
Next_0 (f,S))) & (for f be
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 be
UnOp of M st (for f be
object st f
in M holds (o1
. f)
=
F(f)) & (for f be
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;
::
MODELC_2:def48
func
Next_ (S) ->
UnOp of (
ModelSP (
Inf_seq S)) means
:
Def48: for f be
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 be
UnOp of M st for f be
object st f
in M holds (o
. f)
=
F(f) from
MODELC_1:sch 4;
hence thesis;
end;
uniqueness by
Lm31;
end
definition
let S be non
empty
set;
let f,g be
set;
::
MODELC_2:def49
func
And_0 (f,g,S) ->
Element of (
ModelSP (
Inf_seq S)) means
:
Def49: for t be
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 be
set such that
A1: IT
in (
ModelSP (
Inf_seq S)) & for t be
set st t
in (
Inf_seq S) holds
F(t,Fid,Fid)
=
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 be
set st h1
in (
ModelSP (
Inf_seq S)) & (for t be
set st t
in (
Inf_seq S) holds
F(t,Fid,Fid)
=
TRUE iff ((
Fid (h1,(
Inf_seq S)))
. t)
=
TRUE ) & h2
in (
ModelSP (
Inf_seq S)) & (for t be
set st t
in (
Inf_seq S) holds
F(t,Fid,Fid)
=
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 be
BinOp of (
ModelSP (
Inf_seq S)) st (for f,g be
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 be
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 be
BinOp of M st (for f,g be
Element of M holds (o1
. (f,g))
=
O(f,g)) & (for f,g be
Element of M holds (o2
. (f,g))
=
O(f,g)) holds o1
= o2 from
BINOP_2:sch 2;
for o1,o2 be
BinOp of M st (for f,g be
set st (f
in M) & (g
in M) holds (o1
. (f,g))
= (
And_0 (f,g,S))) & (for f,g be
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 be
set st f
in M & g
in M holds (o1
. (f,g))
= (
And_0 (f,g,S))) & for f,g be
set st f
in M & g
in M holds (o2
. (f,g))
= (
And_0 (f,g,S));
then (for f,g be
Element of M holds (o1
. (f,g))
=
O(f,g)) & for f,g be
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;
::
MODELC_2:def50
func
And_ (S) ->
BinOp of (
ModelSP (
Inf_seq S)) means
:
Def50: for f,g be
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 be
BinOp of M such that
A1: for f,g be
Element of M holds (o
. (f,g))
=
O(f,g) from
BINOP_1:sch 4;
for f,g be
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
let S be non
empty
set;
let f,g be
Function of (
Inf_seq S),
BOOLEAN ;
let t be
set;
::
MODELC_2:def51
func
Until_univ (t,f,g,S) ->
Element of
BOOLEAN equals
:
Def51:
TRUE if t is
Element of (
Inf_seq S) & ex m be
Nat st (for j be
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;
::
MODELC_2:def52
func
Until_0 (f,g,S) ->
Element of (
ModelSP (
Inf_seq S)) means
:
Def52: for t be
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 be
set such that
A1: IT
in (
ModelSP (
Inf_seq S)) & for t be
set st t
in (
Inf_seq S) holds
F(t,Fid,Fid)
=
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 be
set st h1
in (
ModelSP (
Inf_seq S)) & (for t be
set st t
in (
Inf_seq S) holds
F(t,Fid,Fid)
=
TRUE iff ((
Fid (h1,(
Inf_seq S)))
. t)
=
TRUE ) & h2
in (
ModelSP (
Inf_seq S)) & (for t be
set st t
in (
Inf_seq S) holds
F(t,Fid,Fid)
=
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 be
BinOp of (
ModelSP (
Inf_seq S)) st (for f,g be
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 be
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 be
BinOp of M st (for f,g be
Element of M holds (o1
. (f,g))
=
O(f,g)) & (for f,g be
Element of M holds (o2
. (f,g))
=
O(f,g)) holds o1
= o2 from
BINOP_2:sch 2;
for o1,o2 be
BinOp of M st (for f,g be
set st f
in M & g
in M holds (o1
. (f,g))
= (
Until_0 (f,g,S))) & (for f,g be
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 be
set st f
in M & g
in M holds (o1
. (f,g))
= (
Until_0 (f,g,S))) & for f,g be
set st f
in M & g
in M holds (o2
. (f,g))
= (
Until_0 (f,g,S));
then (for f,g be
Element of M holds (o1
. (f,g))
=
O(f,g)) & for f,g be
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;
::
MODELC_2:def53
func
Until_ (S) ->
BinOp of (
ModelSP (
Inf_seq S)) means
:
Def53: for f,g be
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 be
BinOp of M such that
A1: for f,g be
Element of M holds (o
. (f,g))
=
O(f,g) from
BINOP_1:sch 4;
for f,g be
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 be
BinOp of (
ModelSP (
Inf_seq S)) st (for f,g be
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 be
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 be
BinOp of M st (for f,g be
Element of M holds (o1
. (f,g))
=
O(f,g)) & (for f,g be
Element of M holds (o2
. (f,g))
=
O(f,g)) holds o1
= o2 from
BINOP_2:sch 2;
for o1,o2 be
BinOp of M st (for f,g be
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 be
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 be
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 be
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 be
Element of M holds (o1
. (f,g))
=
O(f,g)) & for f,g be
Element of M holds (o2
. (f,g))
=
O(f,g);
hence thesis by
A1;
end;
hence thesis;
end;
Lm35: for o1,o2 be
BinOp of (
ModelSP (
Inf_seq S)) st (for f,g be
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 be
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 be
BinOp of M st (for f,g be
Element of M holds (o1
. (f,g))
=
O(f,g)) & (for f,g be
Element of M holds (o2
. (f,g))
=
O(f,g)) holds o1
= o2 from
BINOP_2:sch 2;
for o1,o2 be
BinOp of M st (for f,g be
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 be
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 be
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 be
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 be
Element of M holds (o1
. (f,g))
=
O(f,g)) & for f,g be
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;
::
MODELC_2:def54
func
Or_ (S) ->
BinOp of (
ModelSP (
Inf_seq S)) means
:
Def54: for f,g be
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 be
BinOp of M such that
A1: for f,g be
Element of M holds (o
. (f,g))
=
O(f,g) from
BINOP_1:sch 4;
for f,g be
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;
::
MODELC_2:def55
func
Release_ (S) ->
BinOp of (
ModelSP (
Inf_seq S)) means
:
Def55: for f,g be
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 be
BinOp of M such that
A2: for f,g be
Element of M holds (o
. (f,g))
=
O(f,g) from
BINOP_1:sch 4;
for f,g be
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
let S be non
empty
set;
let BASSIGN be non
empty
Subset of (
ModelSP (
Inf_seq S));
::
MODELC_2:def56
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
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));
::
MODELC_2:def57
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 ::
MODELC_2:56
(f
'or' g)
= (
'not' ((
'not' f)
'&' (
'not' g))) & (f
'R' g)
= (
'not' ((
'not' f)
'U' (
'not' g))) by
Def54,
Def55;
theorem ::
MODELC_2:57
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 ::
MODELC_2:58
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 ::
MODELC_2:59
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 ::
MODELC_2:60
Th60: t
|= (f
'U' g) iff ex m be
Nat st (for j be
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 be
Nat st (for j be
Nat st j
< m holds (
Shift (t,j))
|= f) & ((
Shift (t,m))
|= g)) implies t
|= (f
'U' g)
proof
assume
A3: ex m be
Nat st (for j be
Nat st j
< m holds (
Shift (t,j))
|= f) & (
Shift (t,m))
|= g;
ex m be
Nat st (for j be
Nat st j
< m holds ((
Fid (f,S1))
. (
Shift (t,j,S)))
=
TRUE ) & ((
Fid (g,S1))
. (
Shift (t,m,S)))
=
TRUE
proof
consider m be
Nat such that
A4: for j be
Nat st j
< m holds (
Shift (t,j))
|= f and
A5: (
Shift (t,m))
|= g by
A3;
take m;
for j be
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 be
Nat st (for j be
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 be
Nat such that
A6: for j be
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 be
Nat st j
< m holds (
Shift (t,j))
|= f by
A6;
hence thesis by
A7;
end;
hence thesis by
A2;
end;
theorem ::
MODELC_2:61
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 ::
MODELC_2:62
Th62: t
|= (f
'R' g) iff for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (t,j))
|= (
'not' f)) implies (
Shift (t,m))
|= g)
proof
A1: (for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (t,j))
|= (
'not' f)) implies (
Shift (t,m))
|/= (
'not' g))) implies for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (t,j))
|= (
'not' f)) implies (
Shift (t,m))
|= g)
proof
assume
A2: for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (t,j))
|= (
'not' f)) implies (
Shift (t,m))
|/= (
'not' g));
for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (t,j))
|= (
'not' f)) implies (
Shift (t,m))
|= g)
proof
let m be
Nat;
(for j be
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 be
Nat holds ((for j be
Nat st j
< m holds (
Shift (t,j))
|= (
'not' f)) implies (
Shift (t,m))
|= g)) implies for m be
Nat holds ((for j be
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
::
MODELC_2:def58
func
AtomicFamily -> non
empty
set equals (
bool
atomic_LTL );
correctness ;
end
definition
let a,t be
object;
::
MODELC_2:def59
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 be
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;
::
MODELC_2:def60
func
AtomicAsgn (a) ->
Element of (
ModelSP (
Inf_seq
AtomicFamily )) means
:
Def60: for t be
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 be
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 be
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 be
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 be
Element of (
ModelSP (
Inf_seq
AtomicFamily )) st (for t be
set st t
in (
Inf_seq
AtomicFamily ) holds ((
Fid (f1,(
Inf_seq
AtomicFamily )))
. t)
= (
AtomicFunc (a,t))) & (for t be
set st t
in (
Inf_seq
AtomicFamily ) holds ((
Fid (f2,(
Inf_seq
AtomicFamily )))
. t)
= (
AtomicFunc (a,t))) holds f1
= f2
proof
let f1,f2 be
Element of (
ModelSP (
Inf_seq
AtomicFamily )) such that
A4: for t be
set st t
in (
Inf_seq
AtomicFamily ) holds ((
Fid (f1,(
Inf_seq
AtomicFamily )))
. t)
= (
AtomicFunc (a,t)) and
A5: for t be
set st t
in (
Inf_seq
AtomicFamily ) holds ((
Fid (f2,(
Inf_seq
AtomicFamily )))
. t)
= (
AtomicFunc (a,t));
for t be
object st t
in (
Inf_seq
AtomicFamily ) holds ((
Fid (f1,(
Inf_seq
AtomicFamily )))
. t)
= ((
Fid (f2,(
Inf_seq
AtomicFamily )))
. t)
proof
let t be
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
::
MODELC_2:def61
func
AtomicBasicAsgn -> non
empty
Subset of (
ModelSP (
Inf_seq
AtomicFamily )) equals { x where x be
Element of (
ModelSP (
Inf_seq
AtomicFamily )) : ex a be
set st x
= (
AtomicAsgn a) };
correctness
proof
set Y = (
ModelSP (
Inf_seq
AtomicFamily ));
set z = (
AtomicAsgn
{} );
set M = { x where x be
Element of (
ModelSP (
Inf_seq
AtomicFamily )) : ex a be
set st x
= (
AtomicAsgn a) };
A1: M
c= Y
proof
let x be
object;
assume x
in M;
then ex y be
Element of Y st x
= y & ex a be
set st y
= (
AtomicAsgn a);
hence thesis;
end;
z
in M;
hence thesis by
A1;
end;
end
definition
::
MODELC_2:def62
func
AtomicKai ->
Function of
atomic_LTL , the
BasicAssign of (
Inf_seqModel (
AtomicFamily ,
AtomicBasicAsgn )) means
:
Def62: for a be
set st a
in
atomic_LTL holds (it
. a)
= (
AtomicAsgn a);
existence
proof
deffunc
F(
object) = (
AtomicAsgn $1);
A1: for a be
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 be
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 be
Function of
atomic_LTL , the
BasicAssign of (
Inf_seqModel (
AtomicFamily ,
AtomicBasicAsgn )) st (for a be
set st a
in
atomic_LTL holds (f1
. a)
= (
AtomicAsgn a)) & (for a be
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 be
set st a
in
atomic_LTL holds (f1
. a)
= (
AtomicAsgn a) and
A4: for a be
set st a
in
atomic_LTL holds (f2
. a)
= (
AtomicAsgn a);
for a be
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;
::
MODELC_2:def63
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 ;
::
MODELC_2:def64
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 ;
::
MODELC_2:def65
func
'X' W ->
Subset of
LTL_WFF equals { x where x be
LTL-formula : ex u be
LTL-formula st u
in W & x
= (
'X' u) };
correctness
proof
set X = { x where x be
LTL-formula : ex u be
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 be
LTL-formula st y
= x & ex u be
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 ::
MODELC_2:63
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 ::
MODELC_2:64
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 ::
MODELC_2:65
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 ::
MODELC_2:66
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 ::
MODELC_2:67
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 ::
MODELC_2:68
Th68: r
|= (H1
'U' H2) iff ex m be
Nat st (for j be
Nat st j
< m holds (
Shift (r,j))
|= H1) & (
Shift (r,m))
|= H2
proof
A1: (ex m be
Nat st (for j be
Nat st j
< m holds (
Shift (r,j))
|= (
Evaluate (H1,
AtomicKai ))) & ((
Shift (r,m))
|= (
Evaluate (H2,
AtomicKai )))) implies ex m be
Nat st (for j be
Nat st j
< m holds (
Shift (r,j))
|= H1) & (
Shift (r,m))
|= H2
proof
assume ex m be
Nat st (for j be
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 be
Nat st j
< m holds (
Shift (r,j))
|= (
Evaluate (H1,
AtomicKai )) and
A3: (
Shift (r,m))
|= (
Evaluate (H2,
AtomicKai ));
take m;
for j be
Nat st j
< m holds (
Shift (r,j))
|= H1 by
A2;
hence thesis by
A3;
end;
A4: (ex m be
Nat st (for j be
Nat st j
< m holds (
Shift (r,j))
|= H1) & ((
Shift (r,m))
|= H2)) implies ex m be
Nat st (for j be
Nat st j
< m holds (
Shift (r,j))
|= (
Evaluate (H1,
AtomicKai ))) & (
Shift (r,m))
|= (
Evaluate (H2,
AtomicKai ))
proof
assume ex m be
Nat st (for j be
Nat st j
< m holds (
Shift (r,j))
|= H1) & (
Shift (r,m))
|= H2;
then
consider m be
Nat such that
A5: for j be
Nat st j
< m holds (
Shift (r,j))
|= H1 and
A6: (
Shift (r,m))
|= H2;
take m;
for j be
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 ::
MODELC_2:69
r
|= (H1
'R' H2) iff for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' H1)) implies (
Shift (r,m))
|= H2)
proof
A1: (for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' (
Evaluate (H1,
AtomicKai )))) implies (
Shift (r,m))
|= (
Evaluate (H2,
AtomicKai )))) implies for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' H1)) implies (
Shift (r,m))
|= H2)
proof
assume
A2: for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' (
Evaluate (H1,
AtomicKai )))) implies (
Shift (r,m))
|= (
Evaluate (H2,
AtomicKai )));
for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' H1)) implies (
Shift (r,m))
|= H2)
proof
let m be
Nat;
(for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' H1)) implies (
Shift (r,m))
|= H2
proof
assume
A3: for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' H1);
for j be
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 be
Nat holds ((for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' H1)) implies (
Shift (r,m))
|= H2)) implies for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' (
Evaluate (H1,
AtomicKai )))) implies (
Shift (r,m))
|= (
Evaluate (H2,
AtomicKai )))
proof
assume
A5: for m be
Nat holds ((for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' H1)) implies (
Shift (r,m))
|= H2);
for m be
Nat holds ((for j be
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 be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' (
Evaluate (H1,
AtomicKai )))) implies (
Shift (r,m))
|= (
Evaluate (H2,
AtomicKai ))
proof
assume
A6: for j be
Nat st j
< m holds (
Shift (r,j))
|= (
'not' (
Evaluate (H1,
AtomicKai )));
for j be
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 ::
MODELC_2:70
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 ::
MODELC_2:71
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 ::
MODELC_2:72
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 ::
MODELC_2:73
r
|/= (
'not' H) iff r
|= H by
Th64;
theorem ::
MODELC_2:74
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 ::
MODELC_2:75
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 be
Nat st (for j be
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 be
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 be
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 be
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 be
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 ::
MODELC_2:76
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 ::
MODELC_2:77
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 be
LTL-formula;
assume H
in (
'X' W);
then ex x be
LTL-formula st H
= x & ex u be
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 be
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;
theorem ::
MODELC_2:78
(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 ::
MODELC_2:79
for t be
Element of (
Inf_seq S) holds (
Shift (t,
0 ))
= t by
Lm28;
theorem ::
MODELC_2:80
for seq be
Element of (
Inf_seq S) holds (
Shift ((
Shift (seq,k)),n))
= (
Shift (seq,(n
+ k))) by
Lm29;
theorem ::
MODELC_2:81
for seq be
sequence of S holds (
CastSeq ((
CastSeq seq),S))
= seq by
Def41;
theorem ::
MODELC_2:82
for seq be
Element of (
Inf_seq S) holds (
CastSeq (
CastSeq (seq,S)))
= seq by
Def41;
theorem ::
MODELC_2:83
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;