let i, j, n, k be Element of NAT ; :: thesis: ADD_MOD ((ADD_MOD (i,j,n)),k,n) = ADD_MOD (i,(ADD_MOD (j,k,n)),n)
thus ADD_MOD ((ADD_MOD (i,j,n)),k,n) = ((i + j) + k) mod (2 to_power n) by NAT_D:23
.= (i + (j + k)) mod (2 to_power n)
.= ADD_MOD (i,(ADD_MOD (j,k,n)),n) by NAT_D:22 ; :: thesis: verum