let f1, f2 be FinSequence of LTLB_WFF ; ( ( len f > 0 & len f1 = len f & f1 . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
f1 . (i + 1) = ('G' (f /. (i + 1))) => (f1 /. i) ) & len f2 = len f & f2 . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
f2 . (i + 1) = ('G' (f /. (i + 1))) => (f2 /. i) ) implies f1 = f2 ) & ( not len f > 0 & f1 = <*> LTLB_WFF & f2 = <*> LTLB_WFF implies f1 = f2 ) )
thus
( len f > 0 & len f1 = len f & f1 . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
f1 . (i + 1) = ('G' (f /. (i + 1))) => (f1 /. i) ) & len f2 = len f & f2 . 1 = ('G' (f /. 1)) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
f2 . (i + 1) = ('G' (f /. (i + 1))) => (f2 /. i) ) implies f1 = f2 )
( not len f > 0 & f1 = <*> LTLB_WFF & f2 = <*> LTLB_WFF implies f1 = f2 )proof
assume that A5:
len f > 0
and A6:
len f1 = len f
and A7:
f1 . 1
= ('G' (f /. 1)) => A
and A8:
for
i being
Element of
NAT st 1
<= i &
i < len f holds
f1 . (i + 1) = ('G' (f /. (i + 1))) => (f1 /. i)
and A9:
len f2 = len f
and A10:
f2 . 1
= ('G' (f /. 1)) => A
and A11:
for
i being
Element of
NAT st 1
<= i &
i < len f holds
f2 . (i + 1) = ('G' (f /. (i + 1))) => (f2 /. i)
;
f1 = f2
A12:
1
<= len f2
by A9, NAT_1:25, A5;
1
<= len f1
by A6, NAT_1:25, A5;
then A13:
f1 /. 1 =
f1 . 1
by FINSEQ_4:15
.=
f2 /. 1
by FINSEQ_4:15, A12, A10, A7
;
A14:
now for n being Element of NAT st n in dom f1 holds
f1 . n = f2 . ndefpred S1[
Nat]
means ( $1
< len f implies
f1 . ($1 + 1) = f2 . ($1 + 1) );
let n be
Element of
NAT ;
( n in dom f1 implies f1 . n = f2 . n )set m =
n -' 1;
assume
n in dom f1
;
f1 . n = f2 . nthen A15:
n in Seg (len f1)
by FINSEQ_1:def 3;
then
1
<= n
by FINSEQ_1:1;
then
1
+ (- 1) <= n + (- 1)
by XREAL_1:6;
then A16:
n -' 1
= n - 1
by XREAL_0:def 2;
then A17:
(n -' 1) + 1
<= len f
by A6, A15, FINSEQ_1:1;
A18:
for
i being
Nat st
S1[
i] holds
S1[
i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A19:
S1[
i]
;
S1[i + 1]
assume A20:
i + 1
< len f
;
f1 . ((i + 1) + 1) = f2 . ((i + 1) + 1)
A21:
1
<= i + 1
by NAT_1:25;
per cases
( i = 0 or i >= 1 )
by NAT_1:25;
suppose
i >= 1
;
f1 . ((i + 1) + 1) = f2 . ((i + 1) + 1)A22:
f1 /. (i + 1) =
f1 . (i + 1)
by FINSEQ_4:15, A6, A20, A21
.=
f2 /. (i + 1)
by FINSEQ_4:15, A9, A20, A19, NAT_1:12
;
thus f1 . ((i + 1) + 1) =
('G' (f /. ((i + 1) + 1))) => (f1 /. (i + 1))
by A20, A21, A8
.=
f2 . ((i + 1) + 1)
by A20, A21, A11, A22
;
verum end; end;
end; A23:
S1[
0 ]
by A7, A10;
A24:
for
i being
Nat holds
S1[
i]
from NAT_1:sch 2(A23, A18);
thus
f1 . n = f2 . n
by A16, A24, A17, XREAL_1:145;
verum end;
dom f1 = dom f2
by FINSEQ_3:29, A6, A9;
hence
f1 = f2
by A14, PARTFUN1:5;
verum
end;
thus
( not len f > 0 & f1 = <*> LTLB_WFF & f2 = <*> LTLB_WFF implies f1 = f2 )
; verum