let n be Nat; for L being FinSequence
for F, v being LTL-formula st L is_Finseq_for v & F in the LTLnew of (CastNode ((L . 1),v)) & 1 < n & n <= len L & not F in the LTLnew of (CastNode ((L . n),v)) holds
ex m being Nat st
( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) )
let L be FinSequence; for F, v being LTL-formula st L is_Finseq_for v & F in the LTLnew of (CastNode ((L . 1),v)) & 1 < n & n <= len L & not F in the LTLnew of (CastNode ((L . n),v)) holds
ex m being Nat st
( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) )
let F, v be LTL-formula; ( L is_Finseq_for v & F in the LTLnew of (CastNode ((L . 1),v)) & 1 < n & n <= len L & not F in the LTLnew of (CastNode ((L . n),v)) implies ex m being Nat st
( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) ) )
assume A1:
( L is_Finseq_for v & F in the LTLnew of (CastNode ((L . 1),v)) & 1 < n & n <= len L & not F in the LTLnew of (CastNode ((L . n),v)) )
; ex m being Nat st
( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) )
defpred S1[ Nat] means for F1 being LTL-formula
for n1 being Nat
for L1 being FinSequence st len L1 <= $1 & L1 is_Finseq_for v & F1 in the LTLnew of (CastNode ((L1 . 1),v)) & 1 < n1 & n1 <= len L1 & not F1 in the LTLnew of (CastNode ((L1 . n1),v)) holds
ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) );
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
S1[k + 1]
S1[
k + 1]
proof
let F1 be
LTL-formula;
for n1 being Nat
for L1 being FinSequence st len L1 <= k + 1 & L1 is_Finseq_for v & F1 in the LTLnew of (CastNode ((L1 . 1),v)) & 1 < n1 & n1 <= len L1 & not F1 in the LTLnew of (CastNode ((L1 . n1),v)) holds
ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )let n1 be
Nat;
for L1 being FinSequence st len L1 <= k + 1 & L1 is_Finseq_for v & F1 in the LTLnew of (CastNode ((L1 . 1),v)) & 1 < n1 & n1 <= len L1 & not F1 in the LTLnew of (CastNode ((L1 . n1),v)) holds
ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )let L1 be
FinSequence;
( len L1 <= k + 1 & L1 is_Finseq_for v & F1 in the LTLnew of (CastNode ((L1 . 1),v)) & 1 < n1 & n1 <= len L1 & not F1 in the LTLnew of (CastNode ((L1 . n1),v)) implies ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) )
assume A4:
len L1 <= k + 1
;
( not L1 is_Finseq_for v or not F1 in the LTLnew of (CastNode ((L1 . 1),v)) or not 1 < n1 or not n1 <= len L1 or F1 in the LTLnew of (CastNode ((L1 . n1),v)) or ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) )
now ( not L1 is_Finseq_for v or not F1 in the LTLnew of (CastNode ((L1 . 1),v)) or not 1 < n1 or not n1 <= len L1 or F1 in the LTLnew of (CastNode ((L1 . n1),v)) or ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) )per cases
( len L1 <= k or len L1 = k + 1 )
by A4, NAT_1:8;
suppose A5:
len L1 = k + 1
;
( not L1 is_Finseq_for v or not F1 in the LTLnew of (CastNode ((L1 . 1),v)) or not 1 < n1 or not n1 <= len L1 or F1 in the LTLnew of (CastNode ((L1 . n1),v)) or ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) )
(
L1 is_Finseq_for v &
F1 in the
LTLnew of
(CastNode ((L1 . 1),v)) & 1
< n1 &
n1 <= len L1 & not
F1 in the
LTLnew of
(CastNode ((L1 . n1),v)) implies ex
m being
Nat st
( 1
<= m &
m < n1 &
F1 in the
LTLnew of
(CastNode ((L1 . m),v)) & not
F1 in the
LTLnew of
(CastNode ((L1 . (m + 1)),v)) ) )
proof
assume that A6:
L1 is_Finseq_for v
and A7:
F1 in the
LTLnew of
(CastNode ((L1 . 1),v))
and A8:
1
< n1
and A9:
n1 <= len L1
and A10:
not
F1 in the
LTLnew of
(CastNode ((L1 . n1),v))
;
ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )
now ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )per cases
( n1 <= k or n1 = k + 1 )
by A5, A9, NAT_1:8;
suppose A11:
n1 <= k
;
ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )set L2 =
L1 | (Seg k);
reconsider L2 =
L1 | (Seg k) as
FinSequence by FINSEQ_1:15;
A12:
k + 0 <= k + 1
by XREAL_1:7;
then A13:
dom L2 = Seg k
by A5, FINSEQ_1:17;
then
n1 in dom L2
by A8, A11, FINSEQ_1:1;
then A14:
L2 . n1 = L1 . n1
by FUNCT_1:47;
1
< k
by A8, A11, XXREAL_0:2;
then
1
in dom L2
by A13, FINSEQ_1:1;
then A15:
F1 in the
LTLnew of
(CastNode ((L2 . 1),v))
by A7, FUNCT_1:47;
(
len L2 = k &
L2 is_Finseq_for v )
by A5, A6, A12, Th26, FINSEQ_1:17;
then consider m being
Nat such that A16:
1
<= m
and A17:
m < n1
and A18:
(
F1 in the
LTLnew of
(CastNode ((L2 . m),v)) & not
F1 in the
LTLnew of
(CastNode ((L2 . (m + 1)),v)) )
by A3, A8, A10, A11, A15, A14;
m + 1
<= n1
by A17, NAT_1:13;
then A19:
m + 1
<= k
by A11, XXREAL_0:2;
1
<= m + 1
by A16, NAT_1:13;
then
m + 1
in dom L2
by A13, A19, FINSEQ_1:1;
then A20:
L2 . (m + 1) = L1 . (m + 1)
by FUNCT_1:47;
m <= k
by A11, A17, XXREAL_0:2;
then
m in dom L2
by A13, A16, FINSEQ_1:1;
then
L2 . m = L1 . m
by FUNCT_1:47;
hence
ex
m being
Nat st
( 1
<= m &
m < n1 &
F1 in the
LTLnew of
(CastNode ((L1 . m),v)) & not
F1 in the
LTLnew of
(CastNode ((L1 . (m + 1)),v)) )
by A16, A17, A18, A20;
verum end; suppose A21:
n1 = k + 1
;
ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )then A22:
1
<= k
by A8, NAT_1:13;
A23:
k + 0 < k + 1
by XREAL_1:8;
now ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )per cases
( F1 in the LTLnew of (CastNode ((L1 . k),v)) or not F1 in the LTLnew of (CastNode ((L1 . k),v)) )
;
suppose A24:
not
F1 in the
LTLnew of
(CastNode ((L1 . k),v))
;
ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )A25:
1
< k
set L2 =
L1 | (Seg k);
reconsider L2 =
L1 | (Seg k) as
FinSequence by FINSEQ_1:15;
A27:
k + 0 <= k + 1
by XREAL_1:7;
then A28:
dom L2 = Seg k
by A5, FINSEQ_1:17;
then
k in dom L2
by A22, FINSEQ_1:1;
then A29:
not
F1 in the
LTLnew of
(CastNode ((L2 . k),v))
by A24, FUNCT_1:47;
1
in dom L2
by A22, A28, FINSEQ_1:1;
then A30:
F1 in the
LTLnew of
(CastNode ((L2 . 1),v))
by A7, FUNCT_1:47;
(
len L2 = k &
L2 is_Finseq_for v )
by A5, A6, A27, Th26, FINSEQ_1:17;
then consider m being
Nat such that A31:
1
<= m
and A32:
m < k
and A33:
F1 in the
LTLnew of
(CastNode ((L2 . m),v))
and A34:
not
F1 in the
LTLnew of
(CastNode ((L2 . (m + 1)),v))
by A3, A30, A29, A25;
m in dom L2
by A28, A31, A32, FINSEQ_1:1;
then A35:
F1 in the
LTLnew of
(CastNode ((L1 . m),v))
by A33, FUNCT_1:47;
( 1
<= m + 1 &
m + 1
<= k )
by A31, A32, NAT_1:13;
then
m + 1
in dom L2
by A28, FINSEQ_1:1;
then A36:
L2 . (m + 1) = L1 . (m + 1)
by FUNCT_1:47;
m < n1
by A21, A23, A32, XXREAL_0:2;
hence
ex
m being
Nat st
( 1
<= m &
m < n1 &
F1 in the
LTLnew of
(CastNode ((L1 . m),v)) & not
F1 in the
LTLnew of
(CastNode ((L1 . (m + 1)),v)) )
by A31, A34, A35, A36;
verum end; end; end; hence
ex
m being
Nat st
( 1
<= m &
m < n1 &
F1 in the
LTLnew of
(CastNode ((L1 . m),v)) & not
F1 in the
LTLnew of
(CastNode ((L1 . (m + 1)),v)) )
;
verum end; end; end;
hence
ex
m being
Nat st
( 1
<= m &
m < n1 &
F1 in the
LTLnew of
(CastNode ((L1 . m),v)) & not
F1 in the
LTLnew of
(CastNode ((L1 . (m + 1)),v)) )
;
verum
end; hence
( not
L1 is_Finseq_for v or not
F1 in the
LTLnew of
(CastNode ((L1 . 1),v)) or not 1
< n1 or not
n1 <= len L1 or
F1 in the
LTLnew of
(CastNode ((L1 . n1),v)) or ex
m being
Nat st
( 1
<= m &
m < n1 &
F1 in the
LTLnew of
(CastNode ((L1 . m),v)) & not
F1 in the
LTLnew of
(CastNode ((L1 . (m + 1)),v)) ) )
;
verum end; end; end;
hence
( not
L1 is_Finseq_for v or not
F1 in the
LTLnew of
(CastNode ((L1 . 1),v)) or not 1
< n1 or not
n1 <= len L1 or
F1 in the
LTLnew of
(CastNode ((L1 . n1),v)) or ex
m being
Nat st
( 1
<= m &
m < n1 &
F1 in the
LTLnew of
(CastNode ((L1 . m),v)) & not
F1 in the
LTLnew of
(CastNode ((L1 . (m + 1)),v)) ) )
;
verum
end;
hence
S1[
k + 1]
;
verum
end;
A37:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A37, A2);
hence
ex m being Nat st
( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) )
by A1; verum