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:40;

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

A3: x /. 1 = FALSE by A2, FINSEQ_4:25;
consider k being Element of BOOLEAN such that
A4: 'not' x = <*k*> by FINSEQ_2:117;
A5: ('not' x) /. 1 = k by A4, FINSEQ_4:25;
A6: 1 in Seg 1 by FINSEQ_1:5;
A7: ('not' x) /. 1 = 'not' FALSE by A3, A6, BINARITH:def 4
.= TRUE ;
A8: ((- (Absval x)) + (2 to_power 1)) - 1 = ((- 0 ) + (2 to_power 1)) - 1 by A2, BINARITH:41
.= (0 + 2) - 1 by POWER:30
.= 1 ;
thus Absval ('not' x) = ((- (Absval x)) + (2 to_power 1)) - 1 by A4, A5, A7, A8, BINARITH:42; :: thesis: verum

end;

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

A10: x /. 1 = TRUE by A9, FINSEQ_4:25;
consider k being Element of BOOLEAN such that
A11: 'not' x = <*k*> by FINSEQ_2:117;
A12: ('not' x) /. 1 = k by A11, FINSEQ_4:25;
A13: 1 in Seg 1 by FINSEQ_1:5;
A14: ('not' x) /. 1 = 'not' TRUE by A10, A13, BINARITH:def 4
.= FALSE ;
A15: ((- (Absval x)) + (2 to_power 1)) - 1 = ((- 1) + (2 to_power 1)) - 1 by A9, BINARITH:42
.= ((- 1) + 2) - 1 by POWER:30
.= 0 ;
thus Absval ('not' x) = ((- (Absval x)) + (2 to_power 1)) - 1 by A11, A12, A14, A15, BINARITH:41; :: thesis: verum

end;

end;

end;

A16: now

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

A18: now

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
A19: x = t ^ <*d*> by FINSEQ_2:137;
A20: Absval ('not' x) = Absval (('not' t) ^ <*('not' d)*>) by A19, Th11
.= (Absval ('not' t)) + (IFEQ ('not' d),FALSE ,0 ,(2 to_power m)) by BINARITH:46
.= (((- (Absval t)) + (2 to_power m)) - 1) + (IFEQ ('not' d),FALSE ,0 ,(2 to_power m)) by A17 ;
A21: ((- (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 A19, BINARITH:46;
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 A22: d = FALSE ; :: thesis: Absval ('not' x) = ((- (Absval x)) + (2 to_power (m + 1))) - 1

A23: Absval ('not' x) = (((- (Absval t)) + (2 to_power m)) - 1) + (2 to_power m) by A20, A22, 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:30
.= ((- (Absval t)) + (2 to_power (m + 1))) - 1 by POWER:32 ;
A24: ((- (Absval x)) + (2 to_power (m + 1))) - 1 = ((- ((Absval t) + 0 )) + (2 to_power (m + 1))) - 1 by A21, A22, FUNCOP_1:def 8
.= ((- (Absval t)) + (2 to_power (m + 1))) - 1 ;
thus Absval ('not' x) = ((- (Absval x)) + (2 to_power (m + 1))) - 1 by A23, A24; :: thesis: verum

end;

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

A26: Absval ('not' x) = (((- (Absval t)) + (2 to_power m)) - 1) + 0 by A20, A25, FUNCOP_1:def 8
.= ((- (Absval t)) + (2 to_power m)) - 1 ;
A27: ((- (Absval x)) + (2 to_power (m + 1))) - 1 = ((- ((Absval t) + (2 to_power m))) + (2 to_power (m + 1))) - 1 by A21, A25, FUNCOP_1:def 8
.= (((- (Absval t)) - (2 to_power m)) + ((2 to_power 1) * (2 to_power m))) - 1 by POWER:32
.= (((- (Absval t)) - (2 to_power m)) + (2 * (2 to_power m))) - 1 by POWER:30
.= ((- (Absval t)) + (2 to_power m)) - 1 ;
thus Absval ('not' x) = ((- (Absval x)) + (2 to_power (m + 1))) - 1 by A26, A27; :: thesis: verum

end;

end;

end;

end;

thus S₁[m + 1] by A18; :: thesis: verum

end;

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