let D be non empty set ; for a, b being set
for f, r, CR being File of D st a <> b & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds
( CR is_a_record_of f,CR & r is_a_record_of f,CR )
let a, b be set ; for f, r, CR being File of D st a <> b & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds
( CR is_a_record_of f,CR & r is_a_record_of f,CR )
let f, r, CR be File of D; ( a <> b & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> implies ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) )
assume that
A1:
a <> b
and
A2:
CR = <*b*>
and
A3:
f = <*b,a,b*>
and
A4:
r = <*a,b*>
; ( CR is_a_record_of f,CR & r is_a_record_of f,CR )
reconsider b2 = b, a2 = a as Element of D by A3, Th10;
A5:
( CR . 1 = b & len CR = 1 )
by A2, FINSEQ_1:40;
f =
<*b,a*> ^ <*b*>
by A3, FINSEQ_1:43
.=
(f | 2) ^ CR
by A2, A3, Th14
;
then
ovlpart (f,CR) = CR
by FINSEQ_8:14;
then
CR /^ (len (ovlpart (f,CR))) = {}
by FINSEQ_6:167;
then
f ^ (CR /^ (len (ovlpart (f,CR)))) = f
by FINSEQ_1:34;
then A6:
ovlcon (f,CR) = f
by FINSEQ_8:def 3;
A7:
f = CR ^ r
by A2, A3, A4, FINSEQ_1:43;
then A8: len f =
(len CR) + (len r)
by FINSEQ_1:22
.=
1 + (len <*a,b*>)
by A2, A4, FINSEQ_1:40
.=
1 + 2
by FINSEQ_1:44
.=
3
;
then
CR ^ r is_substring_of f,1
by A7, FINSEQ_8:19;
then A9:
CR ^ r is_substring_of addcr (f,CR),1
by A6, FINSEQ_8:def 11;
A10:
len CR = 1
by A2, FINSEQ_1:40;
then mid (f,1,(len CR)) =
(f /^ (1 -' 1)) | ((1 -' 1) + 1)
by FINSEQ_6:def 3
.=
(f /^ (1 -' 1)) | (1 + 0)
by NAT_2:8
.=
(f /^ 0) | 1
by NAT_D:34
.=
f | 1
.=
<*b2,a2,b2*> | (Seg 1)
by A3, FINSEQ_1:def 15
.=
CR
by A2, FINSEQ_6:4
;
then
CR is_preposition_of f
by A8, FINSEQ_8:def 8;
then A11:
CR is_preposition_of addcr (f,CR)
by A6, FINSEQ_8:def 11;
r /^ (1 -' 1) =
r /^ ((0 + 1) -' 1)
.=
r /^ 0
by NAT_D:34
.=
r
;
then
(r /^ (1 -' 1)) . 1 = a
by A4, FINSEQ_1:44;
then A12:
not CR is_preposition_of r /^ (1 -' 1)
by A1, A5, FINSEQ_8:21;
A13:
for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of r /^ (j -' 1) holds
j >= 2
r /^ (2 -' 1) =
r /^ ((1 + 1) -' 1)
.=
<*a2,b2*> /^ 1
by A4, NAT_D:34
.=
CR
by A2, FINSEQ_6:46
;
then A16:
instr (1,r,CR) = 2
by A13, FINSEQ_8:def 10;
A17:
len r = 2
by A4, FINSEQ_1:44;
then
((len r) + 1) -' (len CR) = 2
by A10, NAT_D:34;
then
( CR is_terminated_by CR & r is_terminated_by CR )
by A10, A17, A16, FINSEQ_8:28, FINSEQ_8:def 12;
hence
( CR is_a_record_of f,CR & r is_a_record_of f,CR )
by A11, A9; verum