defpred S₁[ Nat] means for x being Tuple of $1, BOOLEAN holds Absval ('not' x) = ((- (Absval x)) + (2 to_power $1)) - 1;
A1: S₁[1]

proof

let x be Tuple of 1, BOOLEAN ; :: thesis: Absval ('not' x) = ((- (Absval x)) + (2 to_power 1)) - 1

per cases ( x = <*FALSE*> or x = <*TRUE*> ) by BINARITH:14;

suppose A2: x = <*FALSE*> ; :: thesis: Absval ('not' x) = ((- (Absval x)) + (2 to_power 1)) - 1

then A3: x /. 1 = FALSE by FINSEQ_4:16;
consider k being Element of BOOLEAN such that
A4: 'not' x = <*k*> by FINSEQ_2:97;
A5: ('not' x) /. 1 = k by A4, FINSEQ_4:16;
1 in Seg 1 by FINSEQ_1:3;
then A6: ('not' x) /. 1 = 'not' FALSE by A3, BINARITH:def 1
.= TRUE ;
((- (Absval x)) + (2 to_power 1)) - 1 = ((- 0) + (2 to_power 1)) - 1 by A2, BINARITH:15
.= (0 + 2) - 1 by POWER:25
.= 1 ;
hence Absval ('not' x) = ((- (Absval x)) + (2 to_power 1)) - 1 by A4, A5, A6, BINARITH:16; :: thesis: verum

end;

suppose A7: x = <*TRUE*> ; :: thesis: Absval ('not' x) = ((- (Absval x)) + (2 to_power 1)) - 1

then A8: x /. 1 = TRUE by FINSEQ_4:16;
consider k being Element of BOOLEAN such that
A9: 'not' x = <*k*> by FINSEQ_2:97;
A10: ('not' x) /. 1 = k by A9, FINSEQ_4:16;
1 in Seg 1 by FINSEQ_1:3;
then A11: ('not' x) /. 1 = 'not' TRUE by A8, BINARITH:def 1
.= FALSE ;
((- (Absval x)) + (2 to_power 1)) - 1 = ((- 1) + (2 to_power 1)) - 1 by A7, BINARITH:16
.= ((- 1) + 2) - 1 by POWER:25
.= 0 ;
hence Absval ('not' x) = ((- (Absval x)) + (2 to_power 1)) - 1 by A9, A10, A11, BINARITH:15; :: thesis: verum

end;

end;

end;

A12: now :: thesis: for m being non zero Nat st S₁[m] holds
S₁[m + 1]

let m be non zero Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A13: S₁[m] ; :: thesis: S₁[m + 1]

now :: thesis: for x being Tuple of m + 1, BOOLEAN holds Absval ('not' x) = ((- (Absval x)) + (2 to_power (m + 1))) - 1

let x be Tuple of m + 1, BOOLEAN ; :: thesis: Absval ('not' x) = ((- (Absval x)) + (2 to_power (m + 1))) - 1
consider t being Element of m -tuples_on BOOLEAN, d being Element of BOOLEAN such that
A14: x = t ^ <*d*> by FINSEQ_2:117;
A15: Absval ('not' x) = Absval (('not' t) ^ <*('not' d)*>) by A14, Th9
.= (Absval ('not' t)) + (IFEQ (('not' d),FALSE,0,(2 to_power m))) by BINARITH:20
.= (((- (Absval t)) + (2 to_power m)) - 1) + (IFEQ (('not' d),FALSE,0,(2 to_power m))) by A13 ;
A16: ((- (Absval x)) + (2 to_power (m + 1))) - 1 = ((- ((Absval t) + (IFEQ (d,FALSE,0,(2 to_power m))))) + (2 to_power (m + 1))) - 1 by A14, BINARITH:20;
thus Absval ('not' x) = ((- (Absval x)) + (2 to_power (m + 1))) - 1 :: thesis: verum

proof

per cases ( d = FALSE or d = TRUE ) by XBOOLEAN:def 3;

suppose A17: d = FALSE ; :: thesis: Absval ('not' x) = ((- (Absval x)) + (2 to_power (m + 1))) - 1

then A18: Absval ('not' x) = (((- (Absval t)) + (2 to_power m)) - 1) + (2 to_power m) by A15, FUNCOP_1:def 8
.= ((- (Absval t)) + (2 * (2 to_power m))) - 1
.= ((- (Absval t)) + ((2 to_power 1) * (2 to_power m))) - 1 by POWER:25
.= ((- (Absval t)) + (2 to_power (m + 1))) - 1 by POWER:27 ;
((- (Absval x)) + (2 to_power (m + 1))) - 1 = ((- ((Absval t) + 0)) + (2 to_power (m + 1))) - 1 by A16, A17, FUNCOP_1:def 8
.= ((- (Absval t)) + (2 to_power (m + 1))) - 1 ;
hence Absval ('not' x) = ((- (Absval x)) + (2 to_power (m + 1))) - 1 by A18; :: thesis: verum

end;

suppose A19: d = TRUE ; :: thesis: Absval ('not' x) = ((- (Absval x)) + (2 to_power (m + 1))) - 1

then A20: Absval ('not' x) = (((- (Absval t)) + (2 to_power m)) - 1) + 0 by A15, FUNCOP_1:def 8
.= ((- (Absval t)) + (2 to_power m)) - 1 ;
((- (Absval x)) + (2 to_power (m + 1))) - 1 = ((- ((Absval t) + (2 to_power m))) + (2 to_power (m + 1))) - 1 by A16, A19, FUNCOP_1:def 8
.= (((- (Absval t)) - (2 to_power m)) + ((2 to_power 1) * (2 to_power m))) - 1 by POWER:27
.= (((- (Absval t)) - (2 to_power m)) + (2 * (2 to_power m))) - 1 by POWER:25
.= ((- (Absval t)) + (2 to_power m)) - 1 ;
hence Absval ('not' x) = ((- (Absval x)) + (2 to_power (m + 1))) - 1 by A20; :: thesis: verum

end;

end;

end;

end;

hence S₁[m + 1] ; :: thesis: verum

end;

thus for m being non zero Nat holds S₁[m] from NAT_1:sch 10(A1, A12); :: thesis: verum