For an introduction to nice loops, I would recommend looking here first:
http://www.paulspages.co.uk/sudokuxp/ho ... eloops.htm
As regards your screenshots, the arrows are a bit confusing at first sight. Take the first screenshot for example. It would have been better for the programmer to have linked the 6 in r1c2 with the 6 in r1c5 (instead of the 7). Similarly, the two "3"s should be linked in r1c12 and the two "1"s in r12c1. In other words, the candidate used for a link is not necessarily the candidate used for the predecessor link (if any), as the graphic appears to imply. In addition, if the polarity (true/false) of the ends of each link would have been represented in a different color, the illustration would be much more understandable. As it is, we just have to keep in mind that the candidate used for a link is the candidate highlighted for the end cell of that link, and keep track of the polarity ourselves.
It also appears that continuous arrows are being used to represent strong links (i.e., between conjugate pairs) and broken arrows for the weak links. But here there is something I don't fully understand. The first screenshot shows a strong link on candidate 3 between r1c1 and r1c2, even though the "3"s in these cells do not form a conjugate pair in row 1 or box 1. My previous understanding was that the strong and weak links are identified in advance and then joined up to form a loop. But this can't be the case here. Instead, it looks like the programmer is making use of the fact that the loop is discontinous and that the inference chain asserts r1c5 = 7, and hence not 3, thus dynamically making the "3"s in r1c12 a strongly linked pair, which is necessary here to complete the loop. Because of this, I'm wondering whether the first example is really a valid nice loop. Maybe someone else can answer this?
The implications are valid though:
r2c1 = 7 --> r2c5 <> 7 --> r1c5 = 7 --> r1c2 = 6 --> r1c1 = 3 --> r2c1 = 1
In other words, r2c1 = 7 --> r2c1 <> 7, which is a logical contradiction. Therefore the original hypothesis (r2c1 = 7) must be incorrect and that we can delete 7 as a candidate from r2c1.
In the second example the implications are:
r3c2 = 6 --> r1c2 <> 6 --> r1c5 = 6 --> r1c8 = 8 --> r3c9 = 6 --> r3c2 <> 6
Again, this is a logical contradiction, implying that the original hypothesis (r3c2 = 6) must be incorrect and that we can delete 6 as a candidate from r3c2.
Hopefully, others on this forum can elaborate on this, and/or answer your other questions (as well as mine on nice loop validity above).