let n be non zero Nat; for x being Tuple of n, BOOLEAN
for m, l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* m) holds
Absval y = Absval x
let x be Tuple of n, BOOLEAN ; for m, l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* m) holds
Absval y = Absval x
defpred S1[ Nat] means for l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* $1) holds
Absval y = Absval x;
A1:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A2:
for
l being
Nat for
y being
Tuple of
l,
BOOLEAN st
y = x ^ (0* m) holds
Absval y = Absval x
;
S1[m + 1]
let l be
Nat;
for y being Tuple of l, BOOLEAN st y = x ^ (0* (m + 1)) holds
Absval y = Absval xlet y be
Tuple of
l,
BOOLEAN ;
( y = x ^ (0* (m + 1)) implies Absval y = Absval x )
assume A3:
y = x ^ (0* (m + 1))
;
Absval y = Absval x
0* m in BOOLEAN *
by BINARI_3:4;
then reconsider z =
0* m as
Tuple of
m,
BOOLEAN by FINSEQ_1:def 11;
x ^ z is
Tuple of
n + m,
BOOLEAN
;
then reconsider y1 =
x ^ (0* m) as
Tuple of
n + m,
BOOLEAN ;
0* (m + 1) = (0* m) ^ <*FALSE*>
by FINSEQ_2:60;
then A4:
y = y1 ^ <*FALSE*>
by FINSEQ_1:32, A3;
X1:
len y = l
by CARD_1:def 7;
len (y1 ^ <*FALSE*>) =
(len y1) + (len <*FALSE*>)
by FINSEQ_1:22
.=
(len y1) + 1
by FINSEQ_1:40
.=
(n + m) + 1
by CARD_1:def 7
;
hence Absval y =
(Absval y1) + (IFEQ (FALSE,FALSE,0,(2 to_power (n + m))))
by X1, BINARITH:20, A4
.=
(Absval x) + (IFEQ (FALSE,FALSE,0,(2 to_power (n + m))))
by A2
.=
(Absval x) + 0
by FUNCOP_1:def 8
.=
Absval x
;
verum
end;
A0:
S1[ 0 ]
for m being Nat holds S1[m]
from NAT_1:sch 2(A0, A1);
hence
for m, l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* m) holds
Absval y = Absval x
; verum