let D be non empty set ; :: thesis: for CR being FinSequence of D holds
( CR separates_uniquely iff len (ovlpart ((CR /^ 1),CR)) = 0 )
let CR be FinSequence of D; :: thesis: ( CR separates_uniquely iff len (ovlpart ((CR /^ 1),CR)) = 0 )
set p = ovlpart ((CR /^ 1),CR);
A1: now :: thesis: ( CR separates_uniquely implies len (ovlpart ((CR /^ 1),CR)) = 0 )
assume A2: CR separates_uniquely ; :: thesis: len (ovlpart ((CR /^ 1),CR)) = 0
set f = (CR | 1) ^ (ovlcon ((CR /^ 1),CR));
A3: (CR | 1) ^ (ovlcon ((CR /^ 1),CR)) = ((CR | 1) ^ (CR /^ 1)) ^ (CR /^ (len (ovlpart ((CR /^ 1),CR)))) by FINSEQ_1:32
.= CR ^ (CR /^ (len (ovlpart ((CR /^ 1),CR)))) by RFINSEQ:8 ;
A4: (CR | 1) ^ (ovlcon ((CR /^ 1),CR)) = (CR | 1) ^ (((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart ((CR /^ 1),CR))))) ^ CR) by Th11
.= ((CR | 1) ^ ((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart ((CR /^ 1),CR)))))) ^ CR by FINSEQ_1:32 ;
A5: len ((CR | 1) ^ ((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart ((CR /^ 1),CR)))))) = (len (CR | 1)) + (len ((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart ((CR /^ 1),CR)))))) by FINSEQ_1:22
.= (len (CR | 1)) + ((len (CR /^ 1)) -' (len (ovlpart ((CR /^ 1),CR)))) by FINSEQ_1:59, NAT_D:35
.= (len (CR | 1)) + ((len (CR /^ 1)) - (len (ovlpart ((CR /^ 1),CR)))) by Th16, XREAL_1:233
.= ((len (CR | 1)) + (len (CR /^ 1))) - (len (ovlpart ((CR /^ 1),CR)))
.= (len ((CR | 1) ^ (CR /^ 1))) - (len (ovlpart ((CR /^ 1),CR))) by FINSEQ_1:22
.= (len CR) - (len (ovlpart ((CR /^ 1),CR))) by RFINSEQ:8 ;
A6: (len CR) - (len (ovlpart ((CR /^ 1),CR))) = (len CR) -' (len (ovlpart ((CR /^ 1),CR))) by Th16, XREAL_1:233;
A7: ((len CR) + 1) -' 1 = len CR by NAT_D:34;
A8: len (ovlpart ((CR /^ 1),CR)) <= len CR by Def2;
A9: len ((CR | 1) ^ (ovlcon ((CR /^ 1),CR))) = (len (CR | 1)) + (len (ovlcon ((CR /^ 1),CR))) by FINSEQ_1:22
.= (len (CR | 1)) + (((len (CR /^ 1)) + (len CR)) - (len (ovlpart ((CR /^ 1),CR)))) by Th15
.= ((len (CR | 1)) + (len (CR /^ 1))) + ((len CR) - (len (ovlpart ((CR /^ 1),CR))))
.= (len ((CR | 1) ^ (CR /^ 1))) + ((len CR) - (len (ovlpart ((CR /^ 1),CR)))) by FINSEQ_1:22
.= (len CR) + ((len CR) - (len (ovlpart ((CR /^ 1),CR)))) by RFINSEQ:8 ;
set j = ((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)));
A10: len CR < (len CR) + 1 by XREAL_1:29;
A11: len (ovlpart ((CR /^ 1),CR)) <= len CR by Def2;
then A12: ((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR))) = (1 + (len CR)) - (len (ovlpart ((CR /^ 1),CR))) by A10, XREAL_1:233, XXREAL_0:2
.= 1 + ((len CR) - (len (ovlpart ((CR /^ 1),CR))))
.= 1 + ((len CR) -' (len (ovlpart ((CR /^ 1),CR)))) by A11, XREAL_1:233 ;
then A13: 1 <= ((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR))) by NAT_1:12;
A14: smid (((CR | 1) ^ (ovlcon ((CR /^ 1),CR))),1,((1 + (len CR)) -' 1)) = (((CR | 1) ^ (ovlcon ((CR /^ 1),CR))) /^ ((0 + 1) -' 1)) | (((len CR) + 1) -' 1) by NAT_D:34
.= (((CR | 1) ^ (ovlcon ((CR /^ 1),CR))) /^ 0) | (len CR) by A7, NAT_D:34
.= ((CR | 1) ^ (ovlcon ((CR /^ 1),CR))) | (len CR) by FINSEQ_5:28
.= CR by A3, FINSEQ_5:23 ;
(((((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) -' 1) + 1 = (((((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) - 1) + 1 by A13, NAT_1:12, XREAL_1:233
.= (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR) ;
then A15: ((((((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) -' 1) + 1) -' (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) = ((((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) - (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) by NAT_1:12, XREAL_1:233
.= len CR ;
1 <= 1 + ((len CR) -' (len (ovlpart ((CR /^ 1),CR)))) by NAT_1:12;
then 1 <= 1 + ((len CR) - (len (ovlpart ((CR /^ 1),CR)))) by A8, XREAL_1:233;
then 1 <= (1 + (len CR)) - (len (ovlpart ((CR /^ 1),CR))) ;
then 1 <= ((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR))) by A8, NAT_1:12, XREAL_1:233;
then (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) -' 1 = (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) - 1 by XREAL_1:233;
then (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) -' 1 = (((len CR) + 1) - (len (ovlpart ((CR /^ 1),CR)))) - 1 by A8, NAT_1:12, XREAL_1:233
.= (((len CR) + 1) - 1) - (len (ovlpart ((CR /^ 1),CR)))
.= (len CR) -' (len (ovlpart ((CR /^ 1),CR))) by A11, XREAL_1:233 ;
then A16: smid (((CR | 1) ^ (ovlcon ((CR /^ 1),CR))),(((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))),(((((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) -' 1)) = CR | (len CR) by A4, A5, A6, A15, FINSEQ_5:37
.= smid (((CR | 1) ^ (ovlcon ((CR /^ 1),CR))),1,((1 + (len CR)) -' 1)) by A14, FINSEQ_1:58 ;
len (ovlpart ((CR /^ 1),CR)) <= len (CR /^ 1) by Th10;
then len (ovlpart ((CR /^ 1),CR)) <= (len CR) -' 1 by RFINSEQ:29;
then A17: ((len CR) + 1) - (len (ovlpart ((CR /^ 1),CR))) >= (1 + (len CR)) - ((len CR) -' 1) by XREAL_1:10;
now :: thesis: ( ( len CR >= 1 & len (ovlpart ((CR /^ 1),CR)) = 0 ) or ( len CR < 1 & len (ovlpart ((CR /^ 1),CR)) = 0 ) )
per cases ( len CR >= 1 or len CR < 1 ) ;
case len CR >= 1 ; :: thesis: len (ovlpart ((CR /^ 1),CR)) = 0
then (1 + (len CR)) - ((len CR) -' 1) = (1 + (len CR)) - ((len CR) - 1) by XREAL_1:233
.= 1 + 1 ;
then 1 < ((len CR) + 1) - (len (ovlpart ((CR /^ 1),CR))) by A17, XXREAL_0:2;
then A18: 1 < ((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR))) by A10, A11, XREAL_1:233, XXREAL_0:2;
((((len CR) -' (len (ovlpart ((CR /^ 1),CR)))) + (len CR)) + 1) -' 1 <= (len CR) + ((len CR) -' (len (ovlpart ((CR /^ 1),CR)))) by NAT_D:34;
then ((1 + ((len CR) -' (len (ovlpart ((CR /^ 1),CR))))) + (len CR)) -' 1 <= (len CR) + ((len CR) - (len (ovlpart ((CR /^ 1),CR)))) by A11, XREAL_1:233;
then A19: (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) -' 1 >= len CR by A2, A9, A12, A14, A16, A18;
A20: (((len CR) + 1) -' (len (ovlpart ((CR /^ 1),CR)))) -' 1 = (1 + ((len CR) -' (len (ovlpart ((CR /^ 1),CR))))) - 1 by A12, NAT_1:12, XREAL_1:233
.= (len CR) -' (len (ovlpart ((CR /^ 1),CR))) ;
A21: (len CR) -' (len (ovlpart ((CR /^ 1),CR))) <= len CR by NAT_D:35;
(len CR) -' (len (ovlpart ((CR /^ 1),CR))) = (len CR) - (len (ovlpart ((CR /^ 1),CR))) by A11, XREAL_1:233;
then (len CR) - (len (ovlpart ((CR /^ 1),CR))) = len CR by A19, A20, A21, XXREAL_0:1;
hence len (ovlpart ((CR /^ 1),CR)) = 0 ; :: thesis: verum
end;
case len CR < 1 ; :: thesis: len (ovlpart ((CR /^ 1),CR)) = 0
then len CR < 0 + 1 ;
then len CR <= 0 by NAT_1:13;
hence len (ovlpart ((CR /^ 1),CR)) = 0 by Def2; :: thesis: verum
end;
end;
end;
hence len (ovlpart ((CR /^ 1),CR)) = 0 ; :: thesis: verum
end;
now :: thesis: ( len (ovlpart ((CR /^ 1),CR)) = 0 implies CR separates_uniquely )
assume A22: len (ovlpart ((CR /^ 1),CR)) = 0 ; :: thesis: CR separates_uniquely
for f being FinSequence of D
for i, j being Element of NAT st 1 <= i & i < j & (j + (len CR)) -' 1 <= len f & smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) & smid (f,i,((i + (len CR)) -' 1)) = CR holds
j -' i >= len CR
proof
let f be FinSequence of D; :: thesis: for i, j being Element of NAT st 1 <= i & i < j & (j + (len CR)) -' 1 <= len f & smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) & smid (f,i,((i + (len CR)) -' 1)) = CR holds
j -' i >= len CR
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i < j & (j + (len CR)) -' 1 <= len f & smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) & smid (f,i,((i + (len CR)) -' 1)) = CR implies j -' i >= len CR )
assume that
A23: 1 <= i and
A24: i < j and
A25: (j + (len CR)) -' 1 <= len f and
A26: smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) and
A27: smid (f,i,((i + (len CR)) -' 1)) = CR ; :: thesis: j -' i >= len CR
A28: j - i > 0 by A24, XREAL_1:50;
then A29: j -' i = j - i by XREAL_0:def 2;
A30: i + (j -' i) = (j - i) + i by A28, XREAL_0:def 2
.= j ;
now :: thesis: ( ( len CR <= 0 & j -' i >= len CR ) or ( len CR > 0 & j -' i >= len CR ) )
per cases ( len CR <= 0 or len CR > 0 ) ;
case len CR <= 0 ; :: thesis: j -' i >= len CR
hence j -' i >= len CR ; :: thesis: verum
end;
case A31: len CR > 0 ; :: thesis: j -' i >= len CR
then A32: 0 + 1 <= len CR by NAT_1:13;
then A33: (len CR) -' 1 = (len CR) - 1 by XREAL_1:233;
A34: (i + (len CR)) -' 1 = (i + (len CR)) - 1 by A32, NAT_1:12, XREAL_1:233;
A35: i <= i + ((len CR) -' 1) by NAT_1:12;
then A36: 1 <= (i + (len CR)) -' 1 by A23, A33, A34, XXREAL_0:2;
set k = j -' i;
A37: 0 + 1 <= j -' i by A24, XREAL_1:50, A29, NAT_1:13;
then A38: (j -' i) - 1 = (j -' i) -' 1 by XREAL_1:233;
A39: i + ((j -' i) -' 1) = i + ((j -' i) - 1) by A37, XREAL_1:233
.= i + ((j - i) - 1) by A28, XREAL_0:def 2
.= j - 1 ;
i + 1 <= j by A24, NAT_1:13;
then A40: (i + 1) - 1 <= j - 1 by XREAL_1:9;
then A41: j -' 1 = j - 1 by XREAL_0:def 2;
j - i > 0 by A24, XREAL_1:50;
then j -' i > 0 by XREAL_0:def 2;
then A42: j -' i >= 0 + 1 by NAT_1:13;
A43: j -' 1 <= (j -' 1) + (len CR) by NAT_1:12;
j <= j + (len CR) by NAT_1:12;
then A44: i < j + (len CR) by A24, XXREAL_0:2;
(j -' 1) + (len CR) = (j - 1) + (len CR) by A40, XREAL_0:def 2
.= (j + (len CR)) - 1
.= (j + (len CR)) -' 1 by A23, A44, XREAL_1:233, XXREAL_0:2 ;
then A45: i + ((j -' i) -' 1) <= len f by A25, A39, A41, A43, XXREAL_0:2;
now :: thesis: not j -' i < len CR
assume A46: j -' i < len CR ; :: thesis: contradiction
then (j -' i) - 1 < (len CR) - 1 by XREAL_1:9;
then (j -' i) -' 1 < (len CR) - 1 by A42, XREAL_1:233;
then (j -' i) -' 1 < (len CR) -' 1 by A32, XREAL_1:233;
then A47: ((j -' i) -' 1) + 1 <= (len CR) -' 1 by NAT_1:13;
A48: (j -' i) - (j -' i) < (len CR) - (j -' i) by A46, XREAL_1:9;
then 0 < (len CR) -' (j -' i) by XREAL_0:def 2;
then A49: 0 + 1 <= (len CR) -' (j -' i) by NAT_1:13;
A50: (len CR) -' (j -' i) = (len CR) - (j -' i) by A48, XREAL_0:def 2;
1 < len CR by A37, A46, XXREAL_0:2;
then 1 + 1 <= len CR by NAT_1:13;
then A51: (1 + 1) - 1 <= (len CR) - 1 by XREAL_1:9;
A52: (len CR) -' 1 = (len CR) - 1 by A37, A46, XREAL_1:233, XXREAL_0:2;
then A53: (len CR) -' (j -' i) <= (len CR) -' 1 by A37, A50, XREAL_1:10;
i <= i + ((j -' i) -' 1) by NAT_1:12;
then A54: i <= len f by A45, XXREAL_0:2;
(j + (len CR)) -' 1 = (j + (len CR)) - 1 by A23, A44, XREAL_1:233, XXREAL_0:2
.= j + ((len CR) - 1)
.= j + ((len CR) -' 1) by A32, XREAL_1:233 ;
then j <= (j + (len CR)) -' 1 by NAT_1:12;
then A55: j <= len f by A25, XXREAL_0:2;
i + 1 <= j by A24, NAT_1:13;
then (i + 1) + (len CR) <= j + (len CR) by XREAL_1:7;
then A56: ((i + 1) + (len CR)) - 1 <= (j + (len CR)) - 1 by XREAL_1:9;
A57: 1 < j by A23, A24, XXREAL_0:2;
A58: j < j + (len CR) by A31, XREAL_1:29;
then A59: 1 < j + (len CR) by A57, XXREAL_0:2;
A60: (j + (len CR)) -' 1 = (j + (len CR)) - 1 by A57, A58, XREAL_1:233, XXREAL_0:2;
then A61: ((i + 1) - 1) + (len CR) <= len f by A25, A56, XXREAL_0:2;
i + (len CR) <= (i + (len CR)) + 1 by NAT_1:12;
then (i + (len CR)) -' 1 <= i + (len CR) by A34, XREAL_1:20;
then A62: (i + (len CR)) -' 1 <= len f by A61, XXREAL_0:2;
A63: 0 + 1 <= (j + (len CR)) -' 1 by A60, NAT_1:13, A59, XREAL_1:50;
j + 1 <= j + (len CR) by A58, NAT_1:13;
then A64: (j + 1) - 1 <= (j + (len CR)) - 1 by XREAL_1:9;
A65: len CR <= (len CR) + (j -' i) by NAT_1:12;
then A66: (len CR) - (j -' i) <= len CR by XREAL_1:20;
A67: (len CR) -' (j -' i) <= len CR by A50, A65, XREAL_1:20;
A68: len (smid (CR,1,((len CR) -' (j -' i)))) = len (mid (CR,1,((len CR) -' (j -' i)))) by A49, Th4;
A69: len (mid (CR,1,((len CR) -' (j -' i)))) = (((len CR) -' (j -' i)) -' 1) + 1 by A32, A49, A50, A66, FINSEQ_6:118
.= (((len CR) -' (j -' i)) - 1) + 1 by A49, XREAL_1:233
.= (len CR) -' (j -' i) ;
A70: ((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1 = (((len CR) -' 1) -' ((len CR) -' (j -' i))) + 1 by RFINSEQ:29
.= (((len CR) -' 1) - ((len CR) -' (j -' i))) + 1 by A53, XREAL_1:233
.= (((len CR) - 1) - ((len CR) - (j -' i))) + 1 by A37, A46, A50, XREAL_1:233, XXREAL_0:2
.= j -' i ;
A71: len (CR /^ 1) = (len CR) -' 1 by RFINSEQ:29;
then A72: smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1))) = mid ((CR /^ 1),(j -' i),((len CR) -' 1)) by A38, A47, A70, Th4;
A73: len (mid ((CR /^ 1),(j -' i),((len CR) -' 1))) = (((len CR) -' 1) -' (j -' i)) + 1 by A37, A38, A47, A51, A52, A71, FINSEQ_6:118
.= (((len CR) -' 1) - (j -' i)) + 1 by A38, A47, XREAL_1:233
.= (((len CR) - 1) - (j -' i)) + 1 by A37, A46, XREAL_1:233, XXREAL_0:2
.= (len CR) -' (j -' i) by A48, XREAL_0:def 2 ;
for jj being Nat st 1 <= jj & jj <= (len CR) -' (j -' i) holds
(smid (CR,1,((len CR) -' (j -' i)))) . jj = (smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1)))) . jj
proof
let jj be Nat; :: thesis: ( 1 <= jj & jj <= (len CR) -' (j -' i) implies (smid (CR,1,((len CR) -' (j -' i)))) . jj = (smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1)))) . jj )
assume that
A74: 1 <= jj and
A75: jj <= (len CR) -' (j -' i) ; :: thesis: (smid (CR,1,((len CR) -' (j -' i)))) . jj = (smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1)))) . jj
A76: jj + (j -' i) <= ((len CR) -' (j -' i)) + (j -' i) by A75, XREAL_1:7;
then A77: (jj + (j -' i)) - 1 <= (len CR) - 1 by A50, XREAL_1:9;
reconsider j1 = jj as Element of NAT by ORDINAL1:def 12;
A78: len (mid (f,i,((i + (len CR)) -' 1))) = (((i + (len CR)) -' 1) -' i) + 1 by A23, A33, A34, A35, A36, A54, A62, FINSEQ_6:118
.= (((i + (len CR)) - 1) - i) + 1 by A33, A34, A35, XREAL_1:233
.= len CR ;
(len CR) -' (j -' i) <= len CR by NAT_D:35;
then A79: jj <= len CR by A75, XXREAL_0:2;
A80: 1 <= jj + ((j -' i) -' 1) by A74, NAT_1:12;
A81: jj + ((j -' i) -' 1) = jj + ((j -' i) - 1) by A37, XREAL_1:233
.= (jj + (j -' i)) - 1
.= (jj + (j -' i)) -' 1 by A74, NAT_1:12, XREAL_1:233 ;
A82: 1 <= jj + (j -' i) by A74, NAT_1:12;
(jj + (j -' i)) -' 1 <= (len CR) - 1 by A74, A77, NAT_1:12, XREAL_1:233;
then (jj + (j -' i)) -' 1 <= (len CR) -' 1 by A32, XREAL_1:233;
then (jj + (j -' i)) -' 1 in Seg (len (CR /^ 1)) by A71, A80, A81;
then A83: (jj + (j -' i)) -' 1 in dom (CR /^ 1) by FINSEQ_1:def 3;
A84: smid (f,j,((j + (len CR)) -' 1)) = mid (f,j,((j + (len CR)) -' 1)) by A60, A64, Th4;
thus (smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1)))) . jj = (CR /^ 1) . ((j1 + (j -' i)) -' 1) by A37, A38, A47, A51, A52, A71, A72, A73, A74, A75, FINSEQ_6:118
.= (smid (f,i,((i + (len CR)) -' 1))) . (((jj + (j -' i)) -' 1) + 1) by A27, A32, A83, RFINSEQ:def 1
.= (mid (f,i,((i + (len CR)) -' 1))) . (((jj + (j -' i)) -' 1) + 1) by A33, A34, A35, Th4
.= (mid (f,i,((i + (len CR)) -' 1))) . (((jj + (j -' i)) - 1) + 1) by A74, NAT_1:12, XREAL_1:233
.= f . ((i + (j1 + (j -' i))) -' 1) by A23, A33, A34, A35, A36, A50, A54, A62, A76, A78, A82, FINSEQ_6:118
.= f . (((i + (j -' i)) + j1) -' 1)
.= CR . jj by A25, A26, A27, A30, A55, A57, A60, A63, A64, A74, A79, A84, FINSEQ_6:118
.= CR . ((j1 + 1) -' 1) by NAT_D:34
.= (mid (CR,1,((len CR) -' (j -' i)))) . j1 by A32, A49, A50, A66, A69, A74, A75, FINSEQ_6:118
.= (smid (CR,1,((len CR) -' (j -' i)))) . jj by A49, Th4 ; :: thesis: verum
end;
then smid (CR,1,((len CR) -' (j -' i))) = smid ((CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1))) by A68, A69, A72, A73;
then (len CR) -' (j -' i) <= len (ovlpart ((CR /^ 1),CR)) by A67, Def2;
hence contradiction by A22, A48, XREAL_0:def 2; :: thesis: verum
end;
hence j -' i >= len CR ; :: thesis: verum
end;
end;
end;
hence j -' i >= len CR ; :: thesis: verum
end;
hence CR separates_uniquely ; :: thesis: verum
end;
hence ( CR separates_uniquely iff len (ovlpart ((CR /^ 1),CR)) = 0 ) by A1; :: thesis: verum