begin
Lm1:
for m, n, k being Nat st m < n & n <= k + 1 holds
m <= k
Lm2:
for n being Nat
for p, q being FinSequence of NAT holds len ((<*n*> ^ p) ^ q) = (1 + (len p)) + (len q)
definition
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;
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
Lm8:
for H being LTL-formula st H is Release holds
H . 1 = 5
Lm9:
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 )
Lm10:
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 ) )
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 )
Lm13:
for H, G, H1, G1 being LTL-formula st H 'or' G = H1 'or' G1 holds
( H = H1 & G = G1 )
Lm14:
for H, G, H1, G1 being LTL-formula st H 'U' G = H1 'U' G1 holds
( H = H1 & G = G1 )
Lm15:
for H, G, H1, G1 being LTL-formula st H 'R' G = H1 'R' G1 holds
( H = H1 & G = G1 )
Lm16:
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 )
Lm17:
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 )
Lm18:
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 )
Lm19:
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 )
Lm20:
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 )
Lm21:
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 )
definition
let H be
LTL-formula;
assume A1:
(
H is
conjunctive or
H is
disjunctive or
H is
Until or
H is
Release )
;
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, Def13, Def14, Def16, Def17;
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, Lm13, Lm14, Lm15;
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 Lm17, Lm18;
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, Lm13, Lm14, Lm15;
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 Lm18, Lm20;
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;
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 Compl of V . (h . (the_argument_of H)) is set ) & ( len H = n + 1 & H is conjunctive implies the L_meet 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 L_join 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 Compl 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 L_meet 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 L_join 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 Compl 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 L_meet 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 L_join 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 Compl of V . (h . (the_argument_of H)) iff b1 = the L_meet 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 Compl of V . (h . (the_argument_of H)) iff b1 = the L_join 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 Compl 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 Compl 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 Compl 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 Compl 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 L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) iff b1 = the L_join 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 L_meet 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 L_meet 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 L_meet 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 L_meet 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 L_join 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 L_join 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 L_join 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 L_join 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 Lm16, Lm17, Lm18, Lm19, Lm20, Lm21;
end;
::
deftheorem Def29 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 carrier 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 Compl of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is conjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_meet 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 L_join 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) = {} ) );
Lm22:
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for f being Function of LTL_WFF, the carrier of V holds f is-PreEvaluation-for 0 ,Kai
Lm23:
for n being Nat
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for n + 1,Kai holds
f is-PreEvaluation-for n,Kai
Lm24:
for n being Nat
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for f being Function of LTL_WFF, the carrier of V st f is-Evaluation-for Kai holds
f is-PreEvaluation-for n,Kai
Lm25:
for n being Nat
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for f1, f2 being Function of LTL_WFF, the carrier 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
Lm26:
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for n being Nat ex f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for n,Kai
Lm27:
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for f being Function of LTL_WFF, the carrier of V st ( for n being Nat holds f is-PreEvaluation-for n,Kai ) holds
f is-Evaluation-for Kai
definition
let V be
LTLModel;
let Kai be
Function of
atomic_LTL, the
BasicAssign of
V;
existence
ex b1 being non empty set st
for p being set holds
( p in b1 iff ( p in bool (Funcs (LTL_WFF, the carrier 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 carrier 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 carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) ) holds
b1 = b2
end;
Lm28:
for n being Nat
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V holds EvalSet (V,Kai,n) in EvalFamily (V,Kai)
Lm29:
for S being non empty set
for seq being Element of Inf_seq S holds Shift (seq,0) = seq
Lm30:
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))
Lm31:
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
definition
let S be non
empty set ;
let f be
set ;
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;
Lm32:
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
definition
let S be non
empty set ;
let f,
g be
set ;
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;
Lm33:
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 ;
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)
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 Lm33;
end;
definition
let S be non
empty set ;
let f,
g be
Function of
(Inf_seq S),
BOOLEAN;
let t be
set ;
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 Def51 defines
Until_univ MODELC_2:def 51 :
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 ;
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;
Lm34:
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 ;
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)
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 Lm34;
end;
Lm35:
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
Lm36:
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 ;
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)))
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 Lm35;
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)))
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 Lm36;
end;
Lm37:
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