:: Model Checking, Part II
:: by Kazuhisa Ishida
::
:: Received April 21, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem DefCastNat defines CastNat MODELC_2:def 1 :
Lm1:
for m, n, k being Nat st m < n & n <= k + 1 holds
m <= k
:: deftheorem defines atom. MODELC_2:def 2 :
:: deftheorem defines 'not' MODELC_2:def 3 :
:: deftheorem defines '&' MODELC_2:def 4 :
:: deftheorem defines 'or' MODELC_2:def 5 :
:: deftheorem defines 'X' MODELC_2:def 6 :
:: deftheorem defines 'U' MODELC_2:def 7 :
:: deftheorem defines 'R' MODELC_2:def 8 :
Lm2:
for n being Nat
for p, q being FinSequence of NAT holds len ((<*n*> ^ p) ^ q) = (1 + (len p)) + (len q)
definition
func LTL_WFF -> non
empty set means :
Def12:
:: MODELC_2:def 9
( ( for
a being
set st
a in it holds
a is
FinSequence of
NAT ) & ( for
n being
Nat holds
atom. n in it ) & ( for
p being
FinSequence of
NAT st
p in it holds
'not' p in it ) & ( for
p,
q being
FinSequence of
NAT st
p in it &
q in it holds
p '&' q in it ) & ( for
p,
q being
FinSequence of
NAT st
p in it &
q in it holds
p 'or' q in it ) & ( for
p being
FinSequence of
NAT st
p in it holds
'X' p in it ) & ( for
p,
q being
FinSequence of
NAT st
p in it &
q in it holds
p 'U' q in it ) & ( for
p,
q being
FinSequence of
NAT st
p in it &
q in it holds
p 'R' q in it ) & ( for
D being non
empty set st ( for
a being
set st
a in D holds
a is
FinSequence of
NAT ) & ( for
n being
Nat holds
atom. n in D ) & ( for
p being
FinSequence of
NAT st
p in D holds
'not' p in D ) & ( for
p,
q being
FinSequence of
NAT st
p in D &
q in D holds
p '&' q in D ) & ( for
p,
q being
FinSequence of
NAT st
p in D &
q in D holds
p 'or' q in D ) & ( for
p being
FinSequence of
NAT st
p in D holds
'X' p in D ) & ( for
p,
q being
FinSequence of
NAT st
p in D &
q in D holds
p 'U' q in D ) & ( for
p,
q being
FinSequence of
NAT st
p in D &
q in D holds
p 'R' q in D ) holds
it c= D ) );
existence
ex b1 being non empty set st
( ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'or' q in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'X' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'U' q in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'R' q in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
b1 c= D ) )
uniqueness
for b1, b2 being non empty set st ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'or' q in b1 ) & ( for p being FinSequence of NAT st p in b1 holds
'X' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'U' q in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p 'R' q in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
b1 c= D ) & ( for a being set st a in b2 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in b2 ) & ( for p being FinSequence of NAT st p in b2 holds
'not' p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p '&' q in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p 'or' q in b2 ) & ( for p being FinSequence of NAT st p in b2 holds
'X' p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p 'U' q in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p 'R' q in b2 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
b2 c= D ) holds
b1 = b2
end;
:: deftheorem Def12 defines LTL_WFF MODELC_2:def 9 :
:: deftheorem Def13 defines LTL-formula-like MODELC_2:def 10 :
theorem Th1: :: MODELC_2:1
:: deftheorem Def14 defines atomic MODELC_2:def 11 :
:: deftheorem Def15 defines negative MODELC_2:def 12 :
:: deftheorem Def16 defines conjunctive MODELC_2:def 13 :
:: deftheorem Def17 defines disjunctive MODELC_2:def 14 :
:: deftheorem Def18 defines next MODELC_2:def 15 :
:: deftheorem Def19 defines Until MODELC_2:def 16 :
:: deftheorem Def1901 defines Release MODELC_2:def 17 :
theorem Th2: :: MODELC_2:2
Lm3:
for H being LTL-formula st H is negative holds
H . 1 = 0
Lm4:
for H being LTL-formula st H is conjunctive holds
H . 1 = 1
Lm5:
for H being LTL-formula st H is disjunctive holds
H . 1 = 2
Lm6:
for H being LTL-formula st H is next holds
H . 1 = 3
Lm7:
for H being LTL-formula st H is Until holds
H . 1 = 4
Lm701:
for H being LTL-formula st H is Release holds
H . 1 = 5
Lm8:
for H being LTL-formula st H is atomic holds
( not H . 1 = 0 & not H . 1 = 1 & not H . 1 = 2 & not H . 1 = 3 & not H . 1 = 4 & not H . 1 = 5 )
Lm9:
for H being LTL-formula holds
( ( 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 ) )
theorem Thlen01: :: MODELC_2:3
Lm11:
for H, F being LTL-formula
for sq being FinSequence st H = F ^ sq holds
H = F
Lm12:
for H, G, H1, G1 being LTL-formula st H '&' G = H1 '&' G1 holds
( H = H1 & G = G1 )
Lm1201:
for H, G, H1, G1 being LTL-formula st H 'or' G = H1 'or' G1 holds
( H = H1 & G = G1 )
Lm13:
for H, G, H1, G1 being LTL-formula st H 'U' G = H1 'U' G1 holds
( H = H1 & G = G1 )
Lm1301:
for H, G, H1, G1 being LTL-formula st H 'R' G = H1 'R' G1 holds
( H = H1 & G = G1 )
Lm15:
for H being LTL-formula st H is negative holds
( not H is atomic & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release )
Lm16:
for H being LTL-formula st H is conjunctive holds
( not H is atomic & not H is negative & not H is disjunctive & not H is next & not H is Until & not H is Release )
Lm1601:
for H being LTL-formula st H is disjunctive holds
( not H is atomic & not H is negative & not H is conjunctive & not H is next & not H is Until & not H is Release )
Lm17:
for H being LTL-formula st H is next holds
( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is Until & not H is Release )
Lm18:
for H being LTL-formula st H is Until holds
( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Release )
Lm1801:
for H being LTL-formula st H is Release holds
( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until )
:: deftheorem Def21 defines the_argument_of MODELC_2:def 18 :
definition
let H be
LTL-formula;
assume A1:
(
H is
conjunctive or
H is
disjunctive or
H is
Until or
H is
Release )
;
func the_left_argument_of H -> LTL-formula means :
Def22:
:: MODELC_2:def 19
ex
H1 being
LTL-formula st
it '&' H1 = H if H is
conjunctive ex
H1 being
LTL-formula st
it 'or' H1 = H if H is
disjunctive ex
H1 being
LTL-formula st
it 'U' H1 = H if H is
Until otherwise ex
H1 being
LTL-formula st
it 'R' H1 = H;
existence
( ( H is conjunctive implies ex b1, H1 being LTL-formula st b1 '&' H1 = H ) & ( H is disjunctive implies ex b1, H1 being LTL-formula st b1 'or' H1 = H ) & ( H is Until implies ex b1, H1 being LTL-formula st b1 'U' H1 = H ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ex b1, H1 being LTL-formula st b1 'R' H1 = H ) )
by A1, Def16, Def17, Def19, Def1901;
uniqueness
for b1, b2 being LTL-formula holds
( ( H is conjunctive & ex H1 being LTL-formula st b1 '&' H1 = H & ex H1 being LTL-formula st b2 '&' H1 = H implies b1 = b2 ) & ( H is disjunctive & ex H1 being LTL-formula st b1 'or' H1 = H & ex H1 being LTL-formula st b2 'or' H1 = H implies b1 = b2 ) & ( H is Until & ex H1 being LTL-formula st b1 'U' H1 = H & ex H1 being LTL-formula st b2 'U' H1 = H implies b1 = b2 ) & ( not H is conjunctive & not H is disjunctive & not H is Until & ex H1 being LTL-formula st b1 'R' H1 = H & ex H1 being LTL-formula st b2 'R' H1 = H implies b1 = b2 ) )
by Lm12, Lm1201, Lm13, Lm1301;
consistency
for b1 being LTL-formula holds
( ( H is conjunctive & H is disjunctive implies ( ex H1 being LTL-formula st b1 '&' H1 = H iff ex H1 being LTL-formula st b1 'or' H1 = H ) ) & ( H is conjunctive & H is Until implies ( ex H1 being LTL-formula st b1 '&' H1 = H iff ex H1 being LTL-formula st b1 'U' H1 = H ) ) & ( H is disjunctive & H is Until implies ( ex H1 being LTL-formula st b1 'or' H1 = H iff ex H1 being LTL-formula st b1 'U' H1 = H ) ) )
by Lm16, Lm1601;
func the_right_argument_of H -> LTL-formula means :
Def23:
:: MODELC_2:def 20
ex
H1 being
LTL-formula st
H1 '&' it = H if H is
conjunctive ex
H1 being
LTL-formula st
H1 'or' it = H if H is
disjunctive ex
H1 being
LTL-formula st
H1 'U' it = H if H is
Until otherwise ex
H1 being
LTL-formula st
H1 'R' it = H;
existence
( ( H is conjunctive implies ex b1, H1 being LTL-formula st H1 '&' b1 = H ) & ( H is disjunctive implies ex b1, H1 being LTL-formula st H1 'or' b1 = H ) & ( H is Until implies ex b1, H1 being LTL-formula st H1 'U' b1 = H ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ex b1, H1 being LTL-formula st H1 'R' b1 = H ) )
uniqueness
for b1, b2 being LTL-formula holds
( ( H is conjunctive & ex H1 being LTL-formula st H1 '&' b1 = H & ex H1 being LTL-formula st H1 '&' b2 = H implies b1 = b2 ) & ( H is disjunctive & ex H1 being LTL-formula st H1 'or' b1 = H & ex H1 being LTL-formula st H1 'or' b2 = H implies b1 = b2 ) & ( H is Until & ex H1 being LTL-formula st H1 'U' b1 = H & ex H1 being LTL-formula st H1 'U' b2 = H implies b1 = b2 ) & ( not H is conjunctive & not H is disjunctive & not H is Until & ex H1 being LTL-formula st H1 'R' b1 = H & ex H1 being LTL-formula st H1 'R' b2 = H implies b1 = b2 ) )
by Lm12, Lm1201, Lm13, Lm1301;
consistency
for b1 being LTL-formula holds
( ( H is conjunctive & H is disjunctive implies ( ex H1 being LTL-formula st H1 '&' b1 = H iff ex H1 being LTL-formula st H1 'or' b1 = H ) ) & ( H is conjunctive & H is Until implies ( ex H1 being LTL-formula st H1 '&' b1 = H iff ex H1 being LTL-formula st H1 'U' b1 = H ) ) & ( H is disjunctive & H is Until implies ( ex H1 being LTL-formula st H1 'or' b1 = H iff ex H1 being LTL-formula st H1 'U' b1 = H ) ) )
by Lm1601, Lm18;
end;
:: deftheorem Def22 defines the_left_argument_of MODELC_2:def 19 :
:: deftheorem Def23 defines the_right_argument_of MODELC_2:def 20 :
theorem :: MODELC_2:4
theorem ThArg2: :: MODELC_2:5
theorem ThArg3: :: MODELC_2:6
theorem ThArg4: :: MODELC_2:7
theorem ThArg5: :: MODELC_2:8
theorem ThArg6: :: MODELC_2:9
theorem ThArg7: :: MODELC_2:10
theorem ThArg8: :: MODELC_2:11
:: deftheorem Def100 defines is_immediate_constituent_of MODELC_2:def 21 :
theorem Th100: :: MODELC_2:12
theorem Th101: :: MODELC_2:13
theorem Th102: :: MODELC_2:14
theorem Th103: :: MODELC_2:15
theorem Th104: :: MODELC_2:16
theorem Th105: :: MODELC_2:17
theorem Th106: :: MODELC_2:18
theorem Th107: :: MODELC_2:19
theorem Th108: :: MODELC_2:20
theorem Th109: :: MODELC_2:21
theorem Th110: :: MODELC_2:22
theorem Th111: :: MODELC_2:23
theorem Th112: :: MODELC_2:24
theorem Th113: :: MODELC_2:25
theorem :: MODELC_2:26
:: deftheorem Def101 defines is_subformula_of MODELC_2:def 22 :
theorem Th115: :: MODELC_2:27
:: deftheorem Def102 defines is_proper_subformula_of MODELC_2:def 23 :
theorem Th116: :: MODELC_2:28
theorem Th117: :: MODELC_2:29
theorem :: MODELC_2:30
theorem :: MODELC_2:31
theorem Th118: :: MODELC_2:32
theorem :: MODELC_2:33
theorem Th120: :: MODELC_2:34
theorem Th121: :: MODELC_2:35
theorem :: MODELC_2:36
theorem Th123: :: MODELC_2:37
theorem Th124: :: MODELC_2:38
theorem :: MODELC_2:39
theorem :: MODELC_2:40
theorem :: MODELC_2:41
theorem :: MODELC_2:42
theorem :: MODELC_2:43
theorem :: MODELC_2:44
:: deftheorem Def103 defines Subformulae MODELC_2:def 24 :
theorem Th131: :: MODELC_2:45
theorem :: MODELC_2:46
theorem :: MODELC_2:47
:: deftheorem Def24 defines CastLTL MODELC_2:def 25 :
:: deftheorem defines atomic_LTL MODELC_2:def 26 :
:: deftheorem Def26 defines is-Evaluation-for MODELC_2:def 27 :
:: deftheorem Def27 defines is-PreEvaluation-for MODELC_2:def 28 :
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
Assignations of
V;
let n be
Nat;
let H be
LTL-formula;
func GraftEval V,
Kai,
f,
h,
n,
H -> set equals :
Def28:
:: MODELC_2:def 29
f . H if len H > n + 1
Kai . H if (
len H = n + 1 &
H is
atomic )
the
Not of
V . (h . (the_argument_of H)) if (
len H = n + 1 &
H is
negative )
the
And of
V . (h . (the_left_argument_of H)),
(h . (the_right_argument_of H)) if (
len H = n + 1 &
H is
conjunctive )
the
Or 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
( ( len H > n + 1 implies f . H is set ) & ( len H = n + 1 & H is atomic implies Kai . H is set ) & ( len H = n + 1 & H is negative implies the Not of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is conjunctive implies the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) is set ) & ( len H = n + 1 & H is disjunctive implies the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) is set ) & ( len H = n + 1 & H is next implies the NEXT of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is Until implies the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) is set ) & ( len H = n + 1 & H is Release implies the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) is set ) & ( len H < n + 1 implies h . H is set ) & ( not len H > n + 1 & ( not len H = n + 1 or not H is atomic ) & ( not len H = n + 1 or not H is negative ) & ( not len H = n + 1 or not H is conjunctive ) & ( not len H = n + 1 or not H is disjunctive ) & ( not len H = n + 1 or not H is next ) & ( not len H = n + 1 or not H is Until ) & ( not len H = n + 1 or not H is Release ) & not len H < n + 1 implies {} is set ) )
;
consistency
for b1 being set holds
( ( len H > n + 1 & len H = n + 1 & H is atomic implies ( b1 = f . H iff b1 = Kai . H ) ) & ( len H > n + 1 & len H = n + 1 & H is negative implies ( b1 = f . H iff b1 = the Not of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is conjunctive implies ( b1 = f . H iff b1 = the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is disjunctive implies ( b1 = f . H iff b1 = the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is next implies ( b1 = f . H iff b1 = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is Until implies ( b1 = f . H iff b1 = the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H > n + 1 & len H = n + 1 & H is Release implies ( b1 = f . H iff b1 = the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H > n + 1 & len H < n + 1 implies ( b1 = f . H iff b1 = h . H ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is negative implies ( b1 = Kai . H iff b1 = the Not of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is conjunctive implies ( b1 = Kai . H iff b1 = the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is disjunctive implies ( b1 = Kai . H iff b1 = the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is next implies ( b1 = Kai . H iff b1 = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is Until implies ( b1 = Kai . H iff b1 = the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H = n + 1 & H is Release implies ( b1 = Kai . H iff b1 = the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is atomic & len H < n + 1 implies ( b1 = Kai . H iff b1 = h . H ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is conjunctive implies ( b1 = the Not of V . (h . (the_argument_of H)) iff b1 = the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is disjunctive implies ( b1 = the Not of V . (h . (the_argument_of H)) iff b1 = the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is next implies ( b1 = the Not of V . (h . (the_argument_of H)) iff b1 = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is Until implies ( b1 = the Not of V . (h . (the_argument_of H)) iff b1 = the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H = n + 1 & H is Release implies ( b1 = the Not of V . (h . (the_argument_of H)) iff b1 = the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is negative & len H < n + 1 implies ( b1 = the Not of V . (h . (the_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is disjunctive implies ( b1 = the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is next implies ( b1 = the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is Until implies ( b1 = the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H = n + 1 & H is Release implies ( b1 = the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is conjunctive & len H < n + 1 implies ( b1 = the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is next implies ( b1 = the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = the NEXT of V . (h . (the_argument_of H)) ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is Until implies ( b1 = the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is disjunctive & len H = n + 1 & H is Release implies ( b1 = the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is disjunctive & len H < n + 1 implies ( b1 = the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is next & len H = n + 1 & H is Until implies ( b1 = the NEXT of V . (h . (the_argument_of H)) iff b1 = the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is next & len H = n + 1 & H is Release implies ( b1 = the NEXT of V . (h . (the_argument_of H)) iff b1 = the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is next & len H < n + 1 implies ( b1 = the NEXT of V . (h . (the_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is Until & len H = n + 1 & H is Release implies ( b1 = the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) ) ) & ( len H = n + 1 & H is Until & len H < n + 1 implies ( b1 = the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = h . H ) ) & ( len H = n + 1 & H is Release & len H < n + 1 implies ( b1 = the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) iff b1 = h . H ) ) )
by Lm15, Lm16, Lm1601, Lm17, Lm18, Lm1801;
end;
:: deftheorem Def28 defines GraftEval MODELC_2:def 29 :
for
V being
LTLModelStr for
Kai being
Function of
atomic_LTL ,the
BasicAssign of
V for
f,
h being
Function of
LTL_WFF ,the
Assignations of
V for
n being
Nat for
H being
LTL-formula holds
( (
len H > n + 1 implies
GraftEval V,
Kai,
f,
h,
n,
H = f . H ) & (
len H = n + 1 &
H is
atomic implies
GraftEval V,
Kai,
f,
h,
n,
H = Kai . H ) & (
len H = n + 1 &
H is
negative implies
GraftEval V,
Kai,
f,
h,
n,
H = the
Not of
V . (h . (the_argument_of H)) ) & (
len H = n + 1 &
H is
conjunctive implies
GraftEval V,
Kai,
f,
h,
n,
H = the
And of
V . (h . (the_left_argument_of H)),
(h . (the_right_argument_of H)) ) & (
len H = n + 1 &
H is
disjunctive implies
GraftEval V,
Kai,
f,
h,
n,
H = the
Or of
V . (h . (the_left_argument_of H)),
(h . (the_right_argument_of H)) ) & (
len H = n + 1 &
H is
next implies
GraftEval V,
Kai,
f,
h,
n,
H = the
NEXT of
V . (h . (the_argument_of H)) ) & (
len H = n + 1 &
H is
Until implies
GraftEval V,
Kai,
f,
h,
n,
H = the
UNTIL of
V . (h . (the_left_argument_of H)),
(h . (the_right_argument_of H)) ) & (
len H = n + 1 &
H is
Release implies
GraftEval V,
Kai,
f,
h,
n,
H = the
RELEASE of
V . (h . (the_left_argument_of H)),
(h . (the_right_argument_of H)) ) & (
len H < n + 1 implies
GraftEval V,
Kai,
f,
h,
n,
H = h . H ) & ( not
len H > n + 1 & ( not
len H = n + 1 or not
H is
atomic ) & ( not
len H = n + 1 or not
H is
negative ) & ( not
len H = n + 1 or not
H is
conjunctive ) & ( not
len H = n + 1 or not
H is
disjunctive ) & ( not
len H = n + 1 or not
H is
next ) & ( not
len H = n + 1 or not
H is
Until ) & ( not
len H = n + 1 or not
H is
Release ) & not
len H < n + 1 implies
GraftEval V,
Kai,
f,
h,
n,
H = {} ) );
Lm24:
for V being LTLModelStr
for Kai being Function of atomic_LTL ,the BasicAssign of V
for f being Function of LTL_WFF ,the Assignations of V holds f is-PreEvaluation-for 0 ,Kai
Lm25:
for n being Nat
for V being LTLModelStr
for Kai being Function of atomic_LTL ,the BasicAssign of V
for f being Function of LTL_WFF ,the Assignations of V st f is-PreEvaluation-for n + 1,Kai holds
f is-PreEvaluation-for n,Kai
Lm26:
for n being Nat
for V being LTLModelStr
for Kai being Function of atomic_LTL ,the BasicAssign of V
for f being Function of LTL_WFF ,the Assignations of V st f is-Evaluation-for Kai holds
f is-PreEvaluation-for n,Kai
Lm27:
for n being Nat
for V being LTLModelStr
for Kai being Function of atomic_LTL ,the BasicAssign of V
for f1, f2 being Function of LTL_WFF ,the Assignations of V st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being LTL-formula st len H <= n holds
f1 . H = f2 . H
Lm28:
for V being LTLModelStr
for Kai being Function of atomic_LTL ,the BasicAssign of V
for n being Nat ex f being Function of LTL_WFF ,the Assignations of V st f is-PreEvaluation-for n,Kai
Lm29:
for V being LTLModelStr
for Kai being Function of atomic_LTL ,the BasicAssign of V
for f being Function of LTL_WFF ,the Assignations of V st ( for n being Nat holds f is-PreEvaluation-for n,Kai ) holds
f is-Evaluation-for Kai
:: deftheorem defines EvalSet MODELC_2:def 30 :
:: deftheorem Def30 defines CastEval MODELC_2:def 31 :
definition
let V be
LTLModelStr ;
let Kai be
Function of
atomic_LTL ,the
BasicAssign of
V;
func EvalFamily V,
Kai -> non
empty set means :
Def31:
:: MODELC_2:def 32
for
p being
set holds
(
p in it iff (
p in bool (Funcs LTL_WFF ,the Assignations of V) & ex
n being
Nat st
p = EvalSet V,
Kai,
n ) );
existence
ex b1 being non empty set st
for p being set holds
( p in b1 iff ( p in bool (Funcs LTL_WFF ,the Assignations of V) & ex n being Nat st p = EvalSet V,Kai,n ) )
uniqueness
for b1, b2 being non empty set st ( for p being set holds
( p in b1 iff ( p in bool (Funcs LTL_WFF ,the Assignations of V) & ex n being Nat st p = EvalSet V,Kai,n ) ) ) & ( for p being set holds
( p in b2 iff ( p in bool (Funcs LTL_WFF ,the Assignations of V) & ex n being Nat st p = EvalSet V,Kai,n ) ) ) holds
b1 = b2
end;
:: deftheorem Def31 defines EvalFamily MODELC_2:def 32 :
Lm30:
for n being Nat
for V being LTLModelStr
for Kai being Function of atomic_LTL ,the BasicAssign of V holds EvalSet V,Kai,n in EvalFamily V,Kai
theorem Th3: :: MODELC_2:48
theorem Th4: :: MODELC_2:49
:: deftheorem Def32 defines Evaluate MODELC_2:def 33 :
:: deftheorem defines 'not' MODELC_2:def 34 :
:: deftheorem defines '&' MODELC_2:def 35 :
:: deftheorem defines 'or' MODELC_2:def 36 :
:: deftheorem defines 'X' MODELC_2:def 37 :
:: deftheorem defines 'U' MODELC_2:def 38 :
:: deftheorem defines 'R' MODELC_2:def 39 :
theorem Th5: :: MODELC_2:50
theorem Th6: :: MODELC_2:51
theorem Th7: :: MODELC_2:52
theorem Th8: :: MODELC_2:53
theorem Th9: :: MODELC_2:54
theorem Th10: :: MODELC_2:55
:: deftheorem defines Inf_seq MODELC_2:def 40 :
:: deftheorem defines CastSeq MODELC_2:def 41 :
:: deftheorem DefCasetSeq2 defines CastSeq MODELC_2:def 42 :
:: deftheorem DefShift01 defines Shift MODELC_2:def 43 :
:: deftheorem defines Shift MODELC_2:def 44 :
:: deftheorem defines Shift MODELC_2:def 45 :
LemShift03:
for S being non empty set
for seq being Element of Inf_seq S holds Shift seq,0 = seq
LemShift04:
for k, n being Nat
for S being non empty set
for seq being Element of Inf_seq S holds Shift (Shift seq,k),n = Shift seq,(n + k)
definition
let S be non
empty set ;
let f be
set ;
func Not_0 f,
S -> Element of
ModelSP (Inf_seq S) means :
Def42:
:: MODELC_2:def 46
for
t being
set st
t in Inf_seq S holds
(
'not' (Castboolean ((Fid f,(Inf_seq S)) . t)) = TRUE iff
(Fid it,(Inf_seq S)) . t = TRUE );
existence
ex b1 being Element of ModelSP (Inf_seq S) st
for t being set st t in Inf_seq S holds
( 'not' (Castboolean ((Fid f,(Inf_seq S)) . t)) = TRUE iff (Fid b1,(Inf_seq S)) . t = TRUE )
uniqueness
for b1, b2 being Element of ModelSP (Inf_seq S) st ( for t being set st t in Inf_seq S holds
( 'not' (Castboolean ((Fid f,(Inf_seq S)) . t)) = TRUE iff (Fid b1,(Inf_seq S)) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds
( 'not' (Castboolean ((Fid f,(Inf_seq S)) . t)) = TRUE iff (Fid b2,(Inf_seq S)) . t = TRUE ) ) holds
b1 = b2
end;
:: deftheorem Def42 defines Not_0 MODELC_2:def 46 :
Lm36:
for S being non empty set ex o being UnOp of ModelSP (Inf_seq S) st
for f being set st f in ModelSP (Inf_seq S) holds
o . f = Not_0 f,S
Lm37:
for S being non empty set
for o1, o2 being UnOp of ModelSP (Inf_seq S) st ( for f being set st f in ModelSP (Inf_seq S) holds
o1 . f = Not_0 f,S ) & ( for f being set st f in ModelSP (Inf_seq S) holds
o2 . f = Not_0 f,S ) holds
o1 = o2
:: deftheorem Def43 defines Not_ MODELC_2:def 47 :
:: deftheorem Def44 defines Next_univ MODELC_2:def 48 :
definition
let S be non
empty set ;
let f be
set ;
func Next_0 f,
S -> Element of
ModelSP (Inf_seq S) means :
Def45:
:: MODELC_2:def 49
for
t being
set st
t in Inf_seq S holds
(
Next_univ t,
(Fid f,(Inf_seq S)) = TRUE iff
(Fid it,(Inf_seq S)) . t = TRUE );
existence
ex b1 being Element of ModelSP (Inf_seq S) st
for t being set st t in Inf_seq S holds
( Next_univ t,(Fid f,(Inf_seq S)) = TRUE iff (Fid b1,(Inf_seq S)) . t = TRUE )
uniqueness
for b1, b2 being Element of ModelSP (Inf_seq S) st ( for t being set st t in Inf_seq S holds
( Next_univ t,(Fid f,(Inf_seq S)) = TRUE iff (Fid b1,(Inf_seq S)) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds
( Next_univ t,(Fid f,(Inf_seq S)) = TRUE iff (Fid b2,(Inf_seq S)) . t = TRUE ) ) holds
b1 = b2
end;
:: deftheorem Def45 defines Next_0 MODELC_2:def 49 :
Lm38:
for S being non empty set ex o being UnOp of ModelSP (Inf_seq S) st
for f being set st f in ModelSP (Inf_seq S) holds
o . f = Next_0 f,S
Lm39:
for S being non empty set
for o1, o2 being UnOp of ModelSP (Inf_seq S) st ( for f being set st f in ModelSP (Inf_seq S) holds
o1 . f = Next_0 f,S ) & ( for f being set st f in ModelSP (Inf_seq S) holds
o2 . f = Next_0 f,S ) holds
o1 = o2
:: deftheorem Def46 defines Next_ MODELC_2:def 50 :
definition
let S be non
empty set ;
let f,
g be
set ;
func And_0 f,
g,
S -> Element of
ModelSP (Inf_seq S) means :
Def50:
:: MODELC_2:def 51
for
t being
set st
t in Inf_seq S holds
(
(Castboolean ((Fid f,(Inf_seq S)) . t)) '&' (Castboolean ((Fid g,(Inf_seq S)) . t)) = TRUE iff
(Fid it,(Inf_seq S)) . t = TRUE );
existence
ex b1 being Element of ModelSP (Inf_seq S) st
for t being set st t in Inf_seq S holds
( (Castboolean ((Fid f,(Inf_seq S)) . t)) '&' (Castboolean ((Fid g,(Inf_seq S)) . t)) = TRUE iff (Fid b1,(Inf_seq S)) . t = TRUE )
uniqueness
for b1, b2 being Element of ModelSP (Inf_seq S) st ( for t being set st t in Inf_seq S holds
( (Castboolean ((Fid f,(Inf_seq S)) . t)) '&' (Castboolean ((Fid g,(Inf_seq S)) . t)) = TRUE iff (Fid b1,(Inf_seq S)) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds
( (Castboolean ((Fid f,(Inf_seq S)) . t)) '&' (Castboolean ((Fid g,(Inf_seq S)) . t)) = TRUE iff (Fid b2,(Inf_seq S)) . t = TRUE ) ) holds
b1 = b2
end;
:: deftheorem Def50 defines And_0 MODELC_2:def 51 :
Lm42:
for S being non empty set ex o being BinOp of ModelSP (Inf_seq S) st
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o . f,g = And_0 f,g,S
Lm43:
for S being non empty set
for o1, o2 being BinOp of ModelSP (Inf_seq S) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o1 . f,g = And_0 f,g,S ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . f,g = And_0 f,g,S ) holds
o1 = o2
definition
let S be non
empty set ;
func And_ S -> BinOp of
ModelSP (Inf_seq S) means :
Def51:
:: MODELC_2:def 52
for
f,
g being
set st
f in ModelSP (Inf_seq S) &
g in ModelSP (Inf_seq S) holds
it . f,
g = And_0 f,
g,
S;
existence
ex b1 being BinOp of ModelSP (Inf_seq S) st
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b1 . f,g = And_0 f,g,S
by Lm42;
uniqueness
for b1, b2 being BinOp of ModelSP (Inf_seq S) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b1 . f,g = And_0 f,g,S ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b2 . f,g = And_0 f,g,S ) holds
b1 = b2
by Lm43;
end;
:: deftheorem Def51 defines And_ MODELC_2:def 52 :
definition
let S be non
empty set ;
let f,
g be
Function of
Inf_seq S,
BOOLEAN ;
let t be
set ;
func Until_univ t,
f,
g,
S -> Element of
BOOLEAN equals :
Def52:
:: MODELC_2:def 53
TRUE if (
t is
Element of
Inf_seq S & ex
m being
Nat st
( ( for
j being
Nat st
j < m holds
f . (Shift t,j,S) = TRUE ) &
g . (Shift t,m,S) = TRUE ) )
otherwise FALSE ;
correctness
coherence
( ( t is Element of Inf_seq S & ex m being Nat st
( ( for j being Nat st j < m holds
f . (Shift t,j,S) = TRUE ) & g . (Shift t,m,S) = TRUE ) implies TRUE is Element of BOOLEAN ) & ( ( not t is Element of Inf_seq S or for m being Nat holds
( ex j being Nat st
( j < m & not f . (Shift t,j,S) = TRUE ) or not g . (Shift t,m,S) = TRUE ) ) implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;
:: deftheorem Def52 defines Until_univ MODELC_2:def 53 :
for
S being non
empty set for
f,
g being
Function of
Inf_seq S,
BOOLEAN for
t being
set holds
( (
t is
Element of
Inf_seq S & ex
m being
Nat st
( ( for
j being
Nat st
j < m holds
f . (Shift t,j,S) = TRUE ) &
g . (Shift t,m,S) = TRUE ) implies
Until_univ t,
f,
g,
S = TRUE ) & ( ( not
t is
Element of
Inf_seq S or for
m being
Nat holds
( ex
j being
Nat st
(
j < m & not
f . (Shift t,j,S) = TRUE ) or not
g . (Shift t,m,S) = TRUE ) ) implies
Until_univ t,
f,
g,
S = FALSE ) );
definition
let S be non
empty set ;
let f,
g be
set ;
func Until_0 f,
g,
S -> Element of
ModelSP (Inf_seq S) means :
Def53:
:: MODELC_2:def 54
for
t being
set st
t in Inf_seq S holds
(
Until_univ t,
(Fid f,(Inf_seq S)),
(Fid g,(Inf_seq S)),
S = TRUE iff
(Fid it,(Inf_seq S)) . t = TRUE );
existence
ex b1 being Element of ModelSP (Inf_seq S) st
for t being set st t in Inf_seq S holds
( Until_univ t,(Fid f,(Inf_seq S)),(Fid g,(Inf_seq S)),S = TRUE iff (Fid b1,(Inf_seq S)) . t = TRUE )
uniqueness
for b1, b2 being Element of ModelSP (Inf_seq S) st ( for t being set st t in Inf_seq S holds
( Until_univ t,(Fid f,(Inf_seq S)),(Fid g,(Inf_seq S)),S = TRUE iff (Fid b1,(Inf_seq S)) . t = TRUE ) ) & ( for t being set st t in Inf_seq S holds
( Until_univ t,(Fid f,(Inf_seq S)),(Fid g,(Inf_seq S)),S = TRUE iff (Fid b2,(Inf_seq S)) . t = TRUE ) ) holds
b1 = b2
end;
:: deftheorem Def53 defines Until_0 MODELC_2:def 54 :
Lm44:
for S being non empty set ex o being BinOp of ModelSP (Inf_seq S) st
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o . f,g = Until_0 f,g,S
Lm45:
for S being non empty set
for o1, o2 being BinOp of ModelSP (Inf_seq S) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o1 . f,g = Until_0 f,g,S ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . f,g = Until_0 f,g,S ) holds
o1 = o2
definition
let S be non
empty set ;
func Until_ S -> BinOp of
ModelSP (Inf_seq S) means :
Def54:
:: MODELC_2:def 55
for
f,
g being
set st
f in ModelSP (Inf_seq S) &
g in ModelSP (Inf_seq S) holds
it . f,
g = Until_0 f,
g,
S;
existence
ex b1 being BinOp of ModelSP (Inf_seq S) st
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b1 . f,g = Until_0 f,g,S
by Lm44;
uniqueness
for b1, b2 being BinOp of ModelSP (Inf_seq S) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b1 . f,g = Until_0 f,g,S ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b2 . f,g = Until_0 f,g,S ) holds
b1 = b2
by Lm45;
end;
:: deftheorem Def54 defines Until_ MODELC_2:def 55 :
Lm4401:
for S being non empty set ex o being BinOp of ModelSP (Inf_seq S) st
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o . f,g = (Not_ S) . ((And_ S) . ((Not_ S) . f),((Not_ S) . g))
Lm4501:
for S being non empty set
for o1, o2 being BinOp of ModelSP (Inf_seq S) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o1 . f,g = (Not_ S) . ((And_ S) . ((Not_ S) . f),((Not_ S) . g)) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . f,g = (Not_ S) . ((And_ S) . ((Not_ S) . f),((Not_ S) . g)) ) holds
o1 = o2
Lm4402:
for S being non empty set ex o being BinOp of ModelSP (Inf_seq S) st
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g))
Lm4502:
for S being non empty set
for o1, o2 being BinOp of ModelSP (Inf_seq S) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o1 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) holds
o1 = o2
definition
let S be non
empty set ;
func Or_ S -> BinOp of
ModelSP (Inf_seq S) means :
Def5401:
:: MODELC_2:def 56
for
f,
g being
set st
f in ModelSP (Inf_seq S) &
g in ModelSP (Inf_seq S) holds
it . f,
g = (Not_ S) . ((And_ S) . ((Not_ S) . f),((Not_ S) . g));
existence
ex b1 being BinOp of ModelSP (Inf_seq S) st
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b1 . f,g = (Not_ S) . ((And_ S) . ((Not_ S) . f),((Not_ S) . g))
by Lm4401;
uniqueness
for b1, b2 being BinOp of ModelSP (Inf_seq S) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b1 . f,g = (Not_ S) . ((And_ S) . ((Not_ S) . f),((Not_ S) . g)) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b2 . f,g = (Not_ S) . ((And_ S) . ((Not_ S) . f),((Not_ S) . g)) ) holds
b1 = b2
by Lm4501;
func Release_ S -> BinOp of
ModelSP (Inf_seq S) means :
Def5402:
:: MODELC_2:def 57
for
f,
g being
set st
f in ModelSP (Inf_seq S) &
g in ModelSP (Inf_seq S) holds
it . f,
g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g));
existence
ex b1 being BinOp of ModelSP (Inf_seq S) st
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b1 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g))
by Lm4402;
uniqueness
for b1, b2 being BinOp of ModelSP (Inf_seq S) st ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b1 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b2 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) holds
b1 = b2
by Lm4502;
end;
:: deftheorem Def5401 defines Or_ MODELC_2:def 56 :
:: deftheorem Def5402 defines Release_ MODELC_2:def 57 :
definition
let S be non
empty set ;
let BASSIGN be non
empty Subset of
(ModelSP (Inf_seq S));
func LTLModel S,
BASSIGN -> LTLModelStr equals :: MODELC_2:def 58
LTLModelStr(#
(ModelSP (Inf_seq S)),
BASSIGN,
(And_ S),
(Or_ S),
(Not_ S),
(Next_ S),
(Until_ S),
(Release_ S) #);
coherence
LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #) is LTLModelStr
;
end;
:: deftheorem defines LTLModel MODELC_2:def 58 :
:: deftheorem Def59 defines |= MODELC_2:def 59 :
theorem :: MODELC_2:56
theorem Th12: :: MODELC_2:57
theorem Th13: :: MODELC_2:58
theorem Th14: :: MODELC_2:59
theorem Th15: :: MODELC_2:60
theorem Th16: :: MODELC_2:61
theorem Th17: :: MODELC_2:62
:: deftheorem defines AtomicFamily MODELC_2:def 60 :
:: deftheorem Def61 defines AtomicFunc MODELC_2:def 61 :
LemFid:
for S being non empty set
for f1, f2 being set st f1 in ModelSP S & f2 in ModelSP S & Fid f1,S = Fid f2,S holds
f1 = f2
:: deftheorem Def62 defines AtomicAsgn MODELC_2:def 62 :
:: deftheorem defines AtomicBasicAsgn MODELC_2:def 63 :
:: deftheorem Def64 defines AtomicKai MODELC_2:def 64 :
:: deftheorem Def65 defines |= MODELC_2:def 65 :
:: deftheorem Def66 defines |= MODELC_2:def 66 :
:: deftheorem defines 'X' MODELC_2:def 67 :
theorem :: MODELC_2:63
theorem Th19: :: MODELC_2:64
theorem Th20: :: MODELC_2:65
theorem Th21: :: MODELC_2:66
theorem Th22: :: MODELC_2:67
theorem Th23: :: MODELC_2:68
theorem :: MODELC_2:69
theorem Th25: :: MODELC_2:70
theorem Th2501: :: MODELC_2:71
theorem Th26: :: MODELC_2:72
theorem :: MODELC_2:73
theorem Th28: :: MODELC_2:74
theorem Th29: :: MODELC_2:75
theorem :: MODELC_2:76
theorem :: MODELC_2:77
theorem :: MODELC_2:78
theorem :: MODELC_2:79
theorem :: MODELC_2:80
theorem :: MODELC_2:81
theorem :: MODELC_2:82
theorem :: MODELC_2:83