let D be non empty set ; for f, CR being File of D ex r being File of D st r is_a_record_of f,CR
let f, CR be File of D; ex r being File of D st r is_a_record_of f,CR
set i0 = instr (1,(addcr (f,CR)),CR);
A1:
instr (1,(addcr (f,CR)),CR) <> 0
then
instr (1,(addcr (f,CR)),CR) > 0
;
then A2:
instr (1,(addcr (f,CR)),CR) >= 0 + 1
by NAT_1:13;
then
(instr (1,(addcr (f,CR)),CR)) - 1 >= 0
by XREAL_1:48;
then A3:
(instr (1,(addcr (f,CR)),CR)) -' 1 = (instr (1,(addcr (f,CR)),CR)) - 1
by XREAL_0:def 2;
per cases
( len f = 0 or len f <> 0 )
;
suppose A4:
len f <> 0
;
ex r being File of D st r is_a_record_of f,CRset r =
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1);
A5:
CR is_preposition_of (addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)
by A1, FINSEQ_8:def 10;
now (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CRper cases
( len CR <= 0 or len CR > 0 )
;
suppose A6:
len CR <= 0
;
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CRthen A7:
CR = <*> D
;
then
CR /^ (len (ovlpart (f,CR))) = CR
by FINSEQ_6:80;
then
f ^ (CR /^ (len (ovlpart (f,CR)))) = f
by A7, FINSEQ_1:34;
then A8:
ovlcon (
f,
CR)
= f
by FINSEQ_8:def 3;
len f > 0
by A4;
then A9:
len f >= 0 + 1
by NAT_1:13;
A10:
(
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) > 0 implies ( 1
<= len f &
mid (
f,1,
(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))))
= (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) )
proof
assume
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) > 0
;
( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) )
then A11:
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= 0 + 1
by NAT_1:13;
per cases
( len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) < ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 or len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 )
;
suppose A12:
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) < ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1
;
( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) )(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) =
((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))
by FINSEQ_1:58
.=
(addcr (f,CR)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))
by A12, FINSEQ_5:77
.=
f | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))
by A8, FINSEQ_8:def 11
.=
mid (
f,1,
(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))))
by A11, FINSEQ_6:116
;
hence
( 1
<= len f &
mid (
f,1,
(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))))
= (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) )
by A9;
verum end; suppose A13:
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1
;
( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) )A14:
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) <= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1
by FINSEQ_5:17;
mid (
f,1,
(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) =
f | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))
by A11, FINSEQ_6:116
.=
(addcr (f,CR)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))
by A8, FINSEQ_8:def 11
;
hence
( 1
<= len f &
mid (
f,1,
(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))))
= (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) )
by A9, A13, A14, XXREAL_0:1;
verum end; end;
end; A15:
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_terminated_by CR
by A6, FINSEQ_8:def 12;
addcr (
f,
CR)
= f
by A8, FINSEQ_8:def 11;
then
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_preposition_of addcr (
f,
CR)
by A10, FINSEQ_8:def 8;
hence
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,
CR
by A15;
verum end; suppose A16:
len CR > 0
;
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR
CR is_preposition_of (addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)
by A1, FINSEQ_8:def 10;
then A17:
len CR <= len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1))
by NAT_1:43;
then
(instr (1,(addcr (f,CR)),CR)) -' 1
<= len (addcr (f,CR))
by A16, CARD_1:27, RFINSEQ:def 1;
then
len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) = (len (addcr (f,CR))) - ((instr (1,(addcr (f,CR)),CR)) -' 1)
by RFINSEQ:def 1;
then A18:
(len CR) + ((instr (1,(addcr (f,CR)),CR)) -' 1) <= len (addcr (f,CR))
by A17, XREAL_1:19;
A19:
len CR >= 0 + 1
by A16, NAT_1:13;
mid (
((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)),1,
(len CR))
= CR
by A5, A16, FINSEQ_8:def 8;
then
((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) | (len CR) = CR
by A19, FINSEQ_6:116;
then A20:
len CR <= len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1))
by FINSEQ_5:16;
A21:
len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) <= len (addcr (f,CR))
by FINSEQ_5:25;
A22:
now len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CRper cases
( ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 >= len (addcr (f,CR)) or ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 < len (addcr (f,CR)) )
;
suppose
((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1
>= len (addcr (f,CR))
;
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CRthen
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) = addcr (
f,
CR)
by FINSEQ_1:58;
hence
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR
by A20, A21, XXREAL_0:2;
verum end; suppose A23:
((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1
< len (addcr (f,CR))
;
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR
(instr (1,(addcr (f,CR)),CR)) - 1
>= 0
by A2, XREAL_1:48;
then A24:
(len CR) + ((instr (1,(addcr (f,CR)),CR)) - 1) >= (len CR) + 0
by XREAL_1:7;
then
((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1
= ((len CR) + (instr (1,(addcr (f,CR)),CR))) - 1
by XREAL_0:def 2;
hence
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR
by A23, A24, FINSEQ_1:59;
verum end; end; end;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1
>= 0
by A2, NAT_1:12, XREAL_1:48;
then A25:
((len CR) + (instr (1,(addcr (f,CR)),CR))) -' 1
<= len (addcr (f,CR))
by A3, A18, XREAL_0:def 2;
then A26:
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) = ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1
by FINSEQ_1:59;
( (
((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) <> 0 implies ( 1
<= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) &
CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) & ( for
j being
Element of
NAT st
j >= 1 &
j > 0 &
CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) ) ) & (
((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = 0 implies not
CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1 ) )
proof
thus
(
((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) <> 0 implies ( 1
<= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) &
CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) & ( for
j being
Element of
NAT st
j >= 1 &
j > 0 &
CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) ) )
( ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = 0 implies not CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1 )proof
assume
((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) <> 0
;
( 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) & ( for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) )
then
0 + 1
<= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)
by NAT_1:13;
hence
1
<= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)
;
( CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) & ( for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) )
set f2 =
((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1);
A27:
instr (1,
(addcr (f,CR)),
CR)
<= (instr (1,(addcr (f,CR)),CR)) + (len CR)
by NAT_1:12;
(instr (1,(addcr (f,CR)),CR)) - 1
>= 0
by A2, XREAL_1:48;
then A28:
(instr (1,(addcr (f,CR)),CR)) -' 1
= (instr (1,(addcr (f,CR)),CR)) - 1
by XREAL_0:def 2;
A29:
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1
>= 0
by A19, NAT_1:12, XREAL_1:48;
then
((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1
= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1
by XREAL_0:def 2;
then
(instr (1,(addcr (f,CR)),CR)) -' 1
<= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))
by A3, A26, A27, XREAL_1:9;
then A30:
len (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) =
(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) - ((instr (1,(addcr (f,CR)),CR)) -' 1)
by RFINSEQ:def 1
.=
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) - ((instr (1,(addcr (f,CR)),CR)) -' 1)
by A25, FINSEQ_1:59
.=
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) - ((instr (1,(addcr (f,CR)),CR)) - 1)
by A29, A28, XREAL_0:def 2
.=
len CR
;
A31:
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1
>= 0
by A19, NAT_1:12, XREAL_1:48;
(instr (1,(addcr (f,CR)),CR)) + (len CR) >= instr (1,
(addcr (f,CR)),
CR)
by NAT_1:12;
then
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) - ((instr (1,(addcr (f,CR)),CR)) -' 1) >= 0
by NAT_D:42, XREAL_1:48;
then (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) -' ((instr (1,(addcr (f,CR)),CR)) -' 1) =
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) - ((instr (1,(addcr (f,CR)),CR)) -' 1)
by XREAL_0:def 2
.=
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) - ((instr (1,(addcr (f,CR)),CR)) - 1)
by A3, A31, XREAL_0:def 2
.=
len CR
;
then A32:
((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) = ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) | (len CR)
by FINSEQ_5:80;
mid (
((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)),1,
(len CR))
= CR
by A5, A16, FINSEQ_8:def 8;
then
((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) = CR
by A19, A32, FINSEQ_6:116;
then
(((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) | (len CR) = CR
by FINSEQ_1:58;
then A33:
mid (
(((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)),1,
(len CR))
= CR
by A19, FINSEQ_6:116;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1
>= 0
by A19, NAT_1:12, XREAL_1:48;
then A34:
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1 =
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1
by XREAL_0:def 2
.=
(instr (1,(addcr (f,CR)),CR)) + (len CR)
;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1
>= 0
by A2, NAT_1:12, XREAL_1:48;
then
(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1
= (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1
by A26, XREAL_0:def 2;
then A35:
((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = instr (1,
(addcr (f,CR)),
CR)
by NAT_D:34;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - (len CR) >= 0
;
then A36:
((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' (len CR) = instr (1,
(addcr (f,CR)),
CR)
by XREAL_0:def 2;
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1 =
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1
by A31, XREAL_0:def 2
.=
(instr (1,(addcr (f,CR)),CR)) + (len CR)
;
then
((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) = ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)
by A3, A18, A36, FINSEQ_1:59;
hence
CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1)
by A16, A30, A33, FINSEQ_8:def 8;
for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - (len CR) >= 0
;
then A37:
((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' (len CR) = instr (1,
(addcr (f,CR)),
CR)
by XREAL_0:def 2;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1
>= 0
by A19, NAT_1:12, XREAL_1:48;
then A38:
((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1
= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1
by XREAL_0:def 2;
thus
for
j being
Element of
NAT st
j >= 1 &
j > 0 &
CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)
verumproof
let j be
Element of
NAT ;
( j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) implies j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) )
assume that A39:
j >= 1
and
j > 0
and A40:
CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)
;
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)
A41:
(((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)) | (len CR) =
(((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)) | (((j -' 1) + (len CR)) -' (j -' 1))
by NAT_D:34
.=
(((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) | ((len CR) + (j -' 1))) /^ (j -' 1)
by FINSEQ_5:80
;
A42:
mid (
(((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)),1,
(len CR))
= (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)) | (len CR)
by A19, FINSEQ_6:116;
A43:
j - 1
>= 0
by A39, XREAL_1:48;
now not j < ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)assume A44:
j < ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)
;
contradictionthen
j < instr (1,
(addcr (f,CR)),
CR)
by A3, A18, A34, A37, FINSEQ_1:59;
then
j -' 1
< (instr (1,(addcr (f,CR)),CR)) -' 1
by A39, NAT_D:56;
then A45:
len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) <= len ((addcr (f,CR)) /^ (j -' 1))
by Th4;
A46:
(j + (len CR)) - 1
>= 0
by A39, NAT_1:12, XREAL_1:48;
then A47:
(j + (len CR)) -' 1 =
(len CR) + (j - 1)
by XREAL_0:def 2
.=
(len CR) + (j -' 1)
by A43, XREAL_0:def 2
;
j < ((((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1) -' (len CR)
by A25, A44, FINSEQ_1:59;
then
j + (len CR) < (instr (1,(addcr (f,CR)),CR)) + (len CR)
by A34, A37, XREAL_1:8;
then
(j + (len CR)) - 1
< ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1
by XREAL_1:9;
then A48:
(j + (len CR)) -' 1
< ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1
by A38, A46, XREAL_0:def 2;
((addcr (f,CR)) /^ (j -' 1)) | (len CR) =
((addcr (f,CR)) /^ (j -' 1)) | (((j -' 1) + (len CR)) -' (j -' 1))
by NAT_D:34
.=
((addcr (f,CR)) | ((len CR) + (j -' 1))) /^ (j -' 1)
by FINSEQ_5:80
.=
(((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) | ((j + (len CR)) -' 1)) /^ (j -' 1)
by A47, A48, FINSEQ_5:77
.=
CR
by A16, A40, A42, A41, A47, FINSEQ_8:def 8
;
then A49:
mid (
((addcr (f,CR)) /^ (j -' 1)),1,
(len CR))
= CR
by A19, FINSEQ_6:116;
1
<= len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1))
by A5, A16, FINSEQ_8:def 8;
then
1
<= len ((addcr (f,CR)) /^ (j -' 1))
by A45, XXREAL_0:2;
then
CR is_preposition_of (addcr (f,CR)) /^ (j -' 1)
by A49, FINSEQ_8:def 8;
hence
contradiction
by A35, A39, A44, FINSEQ_8:def 10;
verum end;
hence
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)
;
verum
end;
end;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - (len CR) >= 0
;
then A50:
((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' (len CR) = instr (1,
(addcr (f,CR)),
CR)
by XREAL_0:def 2;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1
>= 0
by A19, NAT_1:12, XREAL_1:48;
then A51:
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1 =
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1
by XREAL_0:def 2
.=
(instr (1,(addcr (f,CR)),CR)) + (len CR)
;
assume
((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = 0
;
not CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1
then
instr (1,
(addcr (f,CR)),
CR)
= 0
by A3, A18, A51, A50, FINSEQ_1:59;
then
not
CR is_substring_of addcr (
f,
CR),1
by FINSEQ_8:def 10;
hence
not
CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1
by A16, Th41;
verum
end; then A52:
instr (1,
((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)),
CR)
= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)
by FINSEQ_8:def 10;
per cases
( 1 <= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) or 1 > len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) )
;
suppose A53:
1
<= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))
;
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR
(
(addcr (f,CR)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) &
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) <= len (addcr (f,CR)) )
by A25, FINSEQ_1:59;
then
(
len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) > 0 implies ( 1
<= len (addcr (f,CR)) &
mid (
(addcr (f,CR)),1,
(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))))
= (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) )
by A53, FINSEQ_6:116, XXREAL_0:2;
then A54:
(
CR ^ ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) is_substring_of addcr (
f,
CR),1 or
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_preposition_of addcr (
f,
CR) )
by FINSEQ_8:def 8;
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_terminated_by CR
by A22, A52, FINSEQ_8:def 12;
hence
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,
CR
by A54;
verum end; suppose
1
> len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))
;
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CRthen A55:
0 + 1
>= (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1
by NAT_1:13;
then A56:
len CR <= 0
by A22, XREAL_1:6;
then A57:
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_terminated_by CR
by FINSEQ_8:def 12;
0 >= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))
by A55, XREAL_1:6;
then
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) = {}
;
then
CR ^ ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) = CR
by FINSEQ_1:34;
then
CR ^ ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) is_substring_of addcr (
f,
CR),1
by A56, FINSEQ_8:def 7;
hence
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,
CR
by A57;
verum end; end; end; end; end; hence
ex
r being
File of
D st
r is_a_record_of f,
CR
;
verum end; end;