defpred S₁[ non zero Nat] means for z being Tuple of $1, BOOLEAN
for d being Element of BOOLEAN holds Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>;
A1: S₁[1]

proof

let z be Tuple of 1, BOOLEAN ; :: thesis: for d being Element of BOOLEAN holds Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>
let d be Element of BOOLEAN ; :: thesis: Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>
set NZD = ('not' d) 'xor' ('not' (z /. 1));
set DPI = d '&' (z /. 1);
set NZ1 = ('not' z) /. 1;
set B1 = (Bin1 1) /. 1;
A2: 1 in Seg 1 by FINSEQ_1:3;
A3: (('not' d) 'xor' FALSE) 'xor' (add_ovfl (('not' z),(Bin1 1))) = ('not' d) 'xor' ((((('not' z) /. 1) '&' ((Bin1 1) /. 1)) 'or' ((('not' z) /. 1) '&' ((carry (('not' z),(Bin1 1))) /. 1))) 'or' (((Bin1 1) /. 1) '&' ((carry (('not' z),(Bin1 1))) /. 1))) by BINARITH:def 6
.= ('not' d) 'xor' ((((('not' z) /. 1) '&' ((Bin1 1) /. 1)) 'or' ((('not' z) /. 1) '&' FALSE)) 'or' (((Bin1 1) /. 1) '&' ((carry (('not' z),(Bin1 1))) /. 1))) by BINARITH:def 2
.= ('not' d) 'xor' ((((('not' z) /. 1) '&' ((Bin1 1) /. 1)) 'or' FALSE) 'or' (((Bin1 1) /. 1) '&' FALSE)) by BINARITH:def 2
.= ('not' d) 'xor' (TRUE '&' (('not' z) /. 1)) by A2, Th5
.= ('not' d) 'xor' ('not' (z /. 1)) by A2, BINARITH:def 1 ;
A4: (('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' FALSE) 'xor' (add_ovfl (('not' (('not' z) + (Bin1 1))),(Bin1 1))) = ('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' ((((('not' (('not' z) + (Bin1 1))) /. 1) '&' ((Bin1 1) /. 1)) 'or' ((('not' (('not' z) + (Bin1 1))) /. 1) '&' ((carry (('not' (('not' z) + (Bin1 1))),(Bin1 1))) /. 1))) 'or' (((Bin1 1) /. 1) '&' ((carry (('not' (('not' z) + (Bin1 1))),(Bin1 1))) /. 1))) by BINARITH:def 6
.= ('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' ((((('not' (('not' z) + (Bin1 1))) /. 1) '&' ((Bin1 1) /. 1)) 'or' ((('not' (('not' z) + (Bin1 1))) /. 1) '&' FALSE)) 'or' (((Bin1 1) /. 1) '&' ((carry (('not' (('not' z) + (Bin1 1))),(Bin1 1))) /. 1))) by BINARITH:def 2
.= ('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' ((((('not' (('not' z) + (Bin1 1))) /. 1) '&' ((Bin1 1) /. 1)) 'or' FALSE) 'or' (((Bin1 1) /. 1) '&' FALSE)) by BINARITH:def 2
.= ('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' (TRUE '&' (('not' (('not' z) + (Bin1 1))) /. 1)) by A2, Th5
.= ('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' ('not' ((('not' z) + (Bin1 1)) /. 1)) by A2, BINARITH:def 1
.= ('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' ('not' (((('not' z) /. 1) 'xor' ((Bin1 1) /. 1)) 'xor' ((carry (('not' z),(Bin1 1))) /. 1))) by A2, BINARITH:def 5
.= ('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' ('not' (((('not' z) /. 1) 'xor' ((Bin1 1) /. 1)) 'xor' FALSE)) by BINARITH:def 2
.= ('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' ('not' ((('not' z) /. 1) 'xor' TRUE)) by A2, Th5
.= ('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' ('not' (z /. 1)) by A2, BINARITH:def 1 ;
A5: Neg2 (Neg2 (z ^ <*d*>)) = ('not' ((('not' z) ^ <*('not' d)*>) + (Bin1 (1 + 1)))) + (Bin1 (1 + 1)) by Th9
.= ('not' ((('not' z) ^ <*('not' d)*>) + ((Bin1 1) ^ <*FALSE*>))) + (Bin1 (1 + 1)) by Th7
.= ('not' ((('not' z) + (Bin1 1)) ^ <*((('not' d) 'xor' FALSE) 'xor' (add_ovfl (('not' z),(Bin1 1))))*>)) + (Bin1 (1 + 1)) by BINARITH:19
.= (('not' (('not' z) + (Bin1 1))) ^ <*('not' (('not' d) 'xor' ('not' (z /. 1))))*>) + (Bin1 (1 + 1)) by A3, Th9
.= (('not' (('not' z) + (Bin1 1))) ^ <*('not' (('not' d) 'xor' ('not' (z /. 1))))*>) + ((Bin1 1) ^ <*FALSE*>) by Th7
.= (('not' (('not' z) + (Bin1 1))) + (Bin1 1)) ^ <*(('not' (('not' d) 'xor' ('not' (z /. 1)))) 'xor' ('not' (z /. 1)))*> by A4, BINARITH:19 ;
then A6: (Neg2 (Neg2 (z ^ <*d*>))) /. 1 = (('not' (('not' z) + (Bin1 1))) + (Bin1 1)) /. 1 by A2, BINARITH:1
.= ((('not' (('not' z) + (Bin1 1))) /. 1) 'xor' ((Bin1 1) /. 1)) 'xor' ((carry (('not' (('not' z) + (Bin1 1))),(Bin1 1))) /. 1) by A2, BINARITH:def 5
.= ((('not' (('not' z) + (Bin1 1))) /. 1) 'xor' ((Bin1 1) /. 1)) 'xor' FALSE by BINARITH:def 2
.= (('not' (('not' z) + (Bin1 1))) /. 1) 'xor' TRUE by A2, Th5
.= 'not' ('not' ((('not' z) + (Bin1 1)) /. 1)) by A2, BINARITH:def 1
.= ((('not' z) /. 1) 'xor' ((Bin1 1) /. 1)) 'xor' ((carry (('not' z),(Bin1 1))) /. 1) by A2, BINARITH:def 5
.= ((('not' z) /. 1) 'xor' ((Bin1 1) /. 1)) 'xor' FALSE by BINARITH:def 2
.= (('not' z) /. 1) 'xor' TRUE by A2, Th5
.= 'not' ('not' (z /. 1)) by A2, BINARITH:def 1
.= z /. 1 ;
reconsider p = d, q = z /. 1 as boolean object ;
A7: (Neg2 (Neg2 (z ^ <*d*>))) /. 2 = ((('not' d) 'or' ('not' ('not' (z /. 1)))) '&' (('not' ('not' d)) 'or' ('not' (z /. 1)))) 'xor' ('not' (z /. 1)) by A5, BINARITH:2
.= (((('not' p) 'or' q) '&' p) 'or' ((('not' p) 'or' q) '&' ('not' q))) 'xor' ('not' (z /. 1)) by XBOOLEAN:8
.= (((p '&' ('not' p)) 'or' (p '&' q)) 'or' (('not' q) '&' (('not' p) 'or' q))) 'xor' ('not' (z /. 1)) by XBOOLEAN:8
.= (((d '&' ('not' d)) 'or' (d '&' (z /. 1))) 'or' ((('not' (z /. 1)) '&' ('not' d)) 'or' (('not' (z /. 1)) '&' (z /. 1)))) 'xor' ('not' (z /. 1)) by XBOOLEAN:8
.= ((FALSE 'or' (d '&' (z /. 1))) 'or' ((('not' (z /. 1)) '&' ('not' d)) 'or' (('not' (z /. 1)) '&' (z /. 1)))) 'xor' ('not' (z /. 1)) by XBOOLEAN:138
.= ((d '&' (z /. 1)) 'or' ((('not' (z /. 1)) '&' ('not' d)) 'or' FALSE)) 'xor' ('not' (z /. 1)) by XBOOLEAN:138
.= ((('not' d) 'or' ('not' (z /. 1))) '&' (('not' (z /. 1)) '&' ((z /. 1) 'or' d))) 'or' (((d '&' (z /. 1)) 'or' (('not' (z /. 1)) '&' ('not' d))) '&' ('not' ('not' (z /. 1))))
.= ((('not' d) 'or' ('not' (z /. 1))) '&' ((('not' (z /. 1)) '&' (z /. 1)) 'or' (('not' (z /. 1)) '&' d))) 'or' (((d '&' (z /. 1)) 'or' (('not' (z /. 1)) '&' ('not' d))) '&' ('not' ('not' (z /. 1)))) by XBOOLEAN:8
.= ((('not' d) 'or' ('not' (z /. 1))) '&' (FALSE 'or' (('not' (z /. 1)) '&' d))) 'or' (((d '&' (z /. 1)) 'or' (('not' (z /. 1)) '&' ('not' d))) '&' ('not' ('not' (z /. 1)))) by XBOOLEAN:138
.= (((('not' (z /. 1)) '&' d) '&' ('not' d)) 'or' ((('not' (z /. 1)) '&' d) '&' ('not' (z /. 1)))) 'or' (((d '&' (z /. 1)) 'or' (('not' (z /. 1)) '&' ('not' d))) '&' ('not' ('not' (z /. 1)))) by XBOOLEAN:8
.= ((('not' (z /. 1)) '&' (d '&' ('not' d))) 'or' ((('not' (z /. 1)) '&' d) '&' ('not' (z /. 1)))) 'or' (((d '&' (z /. 1)) 'or' (('not' (z /. 1)) '&' ('not' d))) '&' ('not' ('not' (z /. 1))))
.= ((('not' (z /. 1)) '&' FALSE) 'or' ((('not' (z /. 1)) '&' d) '&' ('not' (z /. 1)))) 'or' (((d '&' (z /. 1)) 'or' (('not' (z /. 1)) '&' ('not' d))) '&' ('not' ('not' (z /. 1)))) by XBOOLEAN:138
.= (d '&' (('not' (z /. 1)) '&' ('not' (z /. 1)))) 'or' (((d '&' (z /. 1)) 'or' (('not' (z /. 1)) '&' ('not' d))) '&' ('not' ('not' (z /. 1))))
.= (d '&' ('not' (z /. 1))) 'or' (((z /. 1) '&' ((z /. 1) '&' d)) 'or' ((z /. 1) '&' (('not' (z /. 1)) '&' ('not' d)))) by XBOOLEAN:8
.= (d '&' ('not' (z /. 1))) 'or' ((((z /. 1) '&' (z /. 1)) '&' d) 'or' ((z /. 1) '&' (('not' (z /. 1)) '&' ('not' d))))
.= (d '&' ('not' (z /. 1))) 'or' (((z /. 1) '&' d) 'or' (((z /. 1) '&' ('not' (z /. 1))) '&' ('not' d)))
.= (d '&' ('not' (z /. 1))) 'or' (((z /. 1) '&' d) 'or' (FALSE '&' ('not' d))) by XBOOLEAN:138
.= d '&' (('not' (z /. 1)) 'or' (z /. 1)) by XBOOLEAN:8
.= TRUE '&' d by XBOOLEAN:102
.= d ;
consider k1, k2 being Element of BOOLEAN such that
A8: Neg2 (Neg2 (z ^ <*d*>)) = <*k1,k2*> by FINSEQ_2:100;
A9: ( (Neg2 (Neg2 (z ^ <*d*>))) /. 1 = k1 & (Neg2 (Neg2 (z ^ <*d*>))) /. 2 = k2 ) by A8, FINSEQ_4:17;
consider k being Element of BOOLEAN such that
A10: z = <*k*> by FINSEQ_2:97;
Neg2 (Neg2 (z ^ <*d*>)) = <*k,d*> by A6, A7, A8, A9, A10, FINSEQ_4:16;
hence Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*> by A10, FINSEQ_1:def 9; :: thesis: verum

end;

A11: 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 A12: S₁[m] ; :: thesis: S₁[m + 1]

now :: thesis: for z being Tuple of m + 1, BOOLEAN
for d being Element of BOOLEAN holds Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>

let z be Tuple of m + 1, BOOLEAN ; :: thesis: for d being Element of BOOLEAN holds Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>
let d be Element of BOOLEAN ; :: thesis: Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>
consider t being Element of m -tuples_on BOOLEAN, k being Element of BOOLEAN such that
A13: z = t ^ <*k*> by FINSEQ_2:117;
set A = add_ovfl (('not' t),(Bin1 m));
set B = add_ovfl (('not' (Neg2 t)),(Bin1 m));
Neg2 (Neg2 (t ^ <*k*>)) = Neg2 ((Neg2 t) ^ <*(('not' k) 'xor' (add_ovfl (('not' t),(Bin1 m))))*>) by Th14
.= (Neg2 (Neg2 t)) ^ <*(('not' (('not' k) 'xor' (add_ovfl (('not' t),(Bin1 m))))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m))))*> by Th14 ;
then A14: (Neg2 (Neg2 (t ^ <*k*>))) /. (m + 1) = ('not' (('not' k) 'xor' (add_ovfl (('not' t),(Bin1 m))))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m))) by BINARITH:2;
A15: (t ^ <*k*>) /. (m + 1) = k by BINARITH:2;
reconsider p = k, q = add_ovfl (('not' t),(Bin1 m)) as boolean object ;
('not' (('not' k) 'xor' (add_ovfl (('not' t),(Bin1 m))))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m))) = ((p '&' (('not' p) 'or' ('not' q))) 'or' ((('not' p) 'or' ('not' q)) '&' q)) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m))) by XBOOLEAN:8
.= ((k '&' ('not' (add_ovfl (('not' t),(Bin1 m))))) 'or' ((add_ovfl (('not' t),(Bin1 m))) '&' (('not' k) 'or' ('not' (add_ovfl (('not' t),(Bin1 m))))))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m))) by XBOOLEAN:11
.= ((add_ovfl (('not' t),(Bin1 m))) 'xor' k) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m))) by XBOOLEAN:11
.= k 'xor' ((add_ovfl (('not' t),(Bin1 m))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m)))) by XBOOLEAN:73 ;
then A16: k 'xor' ((add_ovfl (('not' t),(Bin1 m))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m)))) = k 'xor' FALSE by A12, A14, A15;
A17: k 'xor' (k 'xor' ((add_ovfl (('not' t),(Bin1 m))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m))))) = (k 'xor' k) 'xor' ((add_ovfl (('not' t),(Bin1 m))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m)))) by XBOOLEAN:73
.= FALSE 'xor' ((add_ovfl (('not' t),(Bin1 m))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m)))) by XBOOLEAN:138
.= (add_ovfl (('not' t),(Bin1 m))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m))) ;
A18: k 'xor' (k 'xor' FALSE) = FALSE by XBOOLEAN:138;
A19: (add_ovfl (('not' t),(Bin1 m))) 'xor' ((add_ovfl (('not' t),(Bin1 m))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m)))) = ((add_ovfl (('not' t),(Bin1 m))) 'xor' (add_ovfl (('not' t),(Bin1 m)))) 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m))) by XBOOLEAN:73
.= FALSE 'xor' (add_ovfl (('not' (Neg2 t)),(Bin1 m))) by XBOOLEAN:138
.= add_ovfl (('not' (Neg2 t)),(Bin1 m)) ;
A20: m + 1 in Seg (m + 1) by FINSEQ_1:3;
A21: add_ovfl (('not' z),(Bin1 (m + 1))) = add_ovfl ((('not' t) ^ <*('not' k)*>),(Bin1 (m + 1))) by A13, Th9
.= add_ovfl ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>)) by Th7
.= ((((('not' t) ^ <*('not' k)*>) /. (m + 1)) '&' (((Bin1 m) ^ <*FALSE*>) /. (m + 1))) 'or' (((('not' t) ^ <*('not' k)*>) /. (m + 1)) '&' ((carry ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)))) 'or' ((((Bin1 m) ^ <*FALSE*>) /. (m + 1)) '&' ((carry ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1))) by BINARITH:def 6
.= ((((('not' t) ^ <*('not' k)*>) /. (m + 1)) '&' FALSE) 'or' (((('not' t) ^ <*('not' k)*>) /. (m + 1)) '&' ((carry ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)))) 'or' ((((Bin1 m) ^ <*FALSE*>) /. (m + 1)) '&' ((carry ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1))) by BINARITH:2
.= (FALSE 'or' (((('not' t) ^ <*('not' k)*>) /. (m + 1)) '&' ((carry ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)))) 'or' (FALSE '&' ((carry ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1))) by BINARITH:2
.= ('not' k) '&' ((carry ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by BINARITH:2
.= ('not' k) '&' (add_ovfl (('not' t),(Bin1 m))) by BINARITH:18 ;
A22: add_ovfl (('not' (Neg2 z)),(Bin1 (m + 1))) = add_ovfl (('not' (Neg2 z)),((Bin1 m) ^ <*FALSE*>)) by Th7
.= (((('not' (Neg2 z)) /. (m + 1)) '&' (((Bin1 m) ^ <*FALSE*>) /. (m + 1))) 'or' ((('not' (Neg2 z)) /. (m + 1)) '&' ((carry (('not' (Neg2 z)),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)))) 'or' ((((Bin1 m) ^ <*FALSE*>) /. (m + 1)) '&' ((carry (('not' (Neg2 z)),((Bin1 m) ^ <*FALSE*>))) /. (m + 1))) by BINARITH:def 6
.= (((('not' (Neg2 z)) /. (m + 1)) '&' FALSE) 'or' ((('not' (Neg2 z)) /. (m + 1)) '&' ((carry (('not' (Neg2 z)),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)))) 'or' ((((Bin1 m) ^ <*FALSE*>) /. (m + 1)) '&' ((carry (('not' (Neg2 z)),((Bin1 m) ^ <*FALSE*>))) /. (m + 1))) by BINARITH:2
.= (FALSE 'or' ((('not' (Neg2 z)) /. (m + 1)) '&' ((carry (('not' (Neg2 z)),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)))) 'or' (FALSE '&' ((carry (('not' (Neg2 z)),((Bin1 m) ^ <*FALSE*>))) /. (m + 1))) by BINARITH:2
.= (('not' ((('not' t) ^ <*('not' k)*>) + (Bin1 (m + 1)))) /. (m + 1)) '&' ((carry (('not' (('not' (t ^ <*k*>)) + (Bin1 (m + 1)))),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by A13, Th9
.= (('not' ((('not' t) ^ <*('not' k)*>) + (Bin1 (m + 1)))) /. (m + 1)) '&' ((carry (('not' ((('not' t) ^ <*('not' k)*>) + (Bin1 (m + 1)))),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by Th9
.= (('not' ((('not' t) ^ <*('not' k)*>) + ((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) '&' ((carry (('not' ((('not' t) ^ <*('not' k)*>) + (Bin1 (m + 1)))),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by Th7
.= (('not' ((('not' t) ^ <*('not' k)*>) + ((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) '&' ((carry (('not' ((('not' t) ^ <*('not' k)*>) + ((Bin1 m) ^ <*FALSE*>))),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by Th7
.= ('not' (((('not' t) ^ <*('not' k)*>) + ((Bin1 m) ^ <*FALSE*>)) /. (m + 1))) '&' ((carry (('not' ((('not' t) ^ <*('not' k)*>) + ((Bin1 m) ^ <*FALSE*>))),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by A20, BINARITH:def 1
.= ('not' ((((('not' t) ^ <*('not' k)*>) /. (m + 1)) 'xor' (((Bin1 m) ^ <*FALSE*>) /. (m + 1))) 'xor' ((carry ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)))) '&' ((carry (('not' ((('not' t) ^ <*('not' k)*>) + ((Bin1 m) ^ <*FALSE*>))),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by A20, BINARITH:def 5
.= ('not' ((('not' k) 'xor' (((Bin1 m) ^ <*FALSE*>) /. (m + 1))) 'xor' ((carry ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)))) '&' ((carry (('not' ((('not' t) ^ <*('not' k)*>) + ((Bin1 m) ^ <*FALSE*>))),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by BINARITH:2
.= ('not' ((('not' k) 'xor' FALSE) 'xor' ((carry ((('not' t) ^ <*('not' k)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)))) '&' ((carry (('not' ((('not' t) ^ <*('not' k)*>) + ((Bin1 m) ^ <*FALSE*>))),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by BINARITH:2
.= ('not' ((('not' k) 'xor' FALSE) 'xor' (add_ovfl (('not' t),(Bin1 m))))) '&' ((carry (('not' ((('not' t) ^ <*('not' k)*>) + ((Bin1 m) ^ <*FALSE*>))),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by BINARITH:18
.= ('not' (('not' k) 'xor' (add_ovfl (('not' t),(Bin1 m))))) '&' ((carry (('not' ((('not' t) + (Bin1 m)) ^ <*((('not' k) 'xor' FALSE) 'xor' (add_ovfl (('not' t),(Bin1 m))))*>)),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by BINARITH:19
.= ('not' (('not' k) 'xor' (add_ovfl (('not' t),(Bin1 m))))) '&' ((carry ((('not' (('not' t) + (Bin1 m))) ^ <*('not' ((('not' k) 'xor' FALSE) 'xor' (add_ovfl (('not' t),(Bin1 m)))))*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1)) by Th9
.= ((('not' k) 'or' ('not' (add_ovfl (('not' t),(Bin1 m))))) '&' (k 'or' ('not' ('not' (add_ovfl (('not' t),(Bin1 m))))))) '&' (add_ovfl (('not' t),(Bin1 m))) by A16, A17, A18, A19, BINARITH:18
.= (('not' k) 'or' ('not' (add_ovfl (('not' t),(Bin1 m))))) '&' ((add_ovfl (('not' t),(Bin1 m))) '&' (k 'or' (add_ovfl (('not' t),(Bin1 m)))))
.= (add_ovfl (('not' t),(Bin1 m))) '&' (('not' (add_ovfl (('not' t),(Bin1 m)))) 'or' ('not' k)) by XBOOLEAN:6
.= (add_ovfl (('not' t),(Bin1 m))) '&' ('not' k) by XBOOLEAN:11 ;
set C = ('not' k) '&' (add_ovfl (('not' t),(Bin1 m)));
reconsider p = d, q = ('not' k) '&' (add_ovfl (('not' t),(Bin1 m))) as boolean object ;
A23: ('not' (('not' d) 'xor' (('not' k) '&' (add_ovfl (('not' t),(Bin1 m)))))) 'xor' (('not' k) '&' (add_ovfl (('not' t),(Bin1 m)))) = ((p '&' (('not' p) 'or' ('not' q))) 'or' ((('not' p) 'or' ('not' q)) '&' q)) 'xor' (('not' k) '&' (add_ovfl (('not' t),(Bin1 m)))) by XBOOLEAN:8
.= ((d '&' ('not' (('not' k) '&' (add_ovfl (('not' t),(Bin1 m)))))) 'or' ((('not' k) '&' (add_ovfl (('not' t),(Bin1 m)))) '&' (('not' d) 'or' ('not' (('not' k) '&' (add_ovfl (('not' t),(Bin1 m)))))))) 'xor' (('not' k) '&' (add_ovfl (('not' t),(Bin1 m)))) by XBOOLEAN:11
.= ((('not' k) '&' (add_ovfl (('not' t),(Bin1 m)))) 'xor' d) 'xor' (('not' k) '&' (add_ovfl (('not' t),(Bin1 m)))) by XBOOLEAN:11
.= d 'xor' ((('not' k) '&' (add_ovfl (('not' t),(Bin1 m)))) 'xor' (('not' k) '&' (add_ovfl (('not' t),(Bin1 m))))) by XBOOLEAN:73
.= d 'xor' FALSE by XBOOLEAN:138
.= d ;
thus Neg2 (Neg2 (z ^ <*d*>)) = Neg2 ((Neg2 z) ^ <*(('not' d) 'xor' (add_ovfl (('not' z),(Bin1 (m + 1)))))*>) by Th14
.= (Neg2 (Neg2 z)) ^ <*(('not' (('not' d) 'xor' (add_ovfl (('not' z),(Bin1 (m + 1)))))) 'xor' (add_ovfl (('not' (Neg2 z)),(Bin1 (m + 1)))))*> by Th14
.= z ^ <*d*> by A12, A13, A21, A22, A23 ; :: thesis: verum

end;

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

end;

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