-- PUZZLEPROOF

Derivation of

loop(4,[source])

Narrowing the preceding formula leads to the formula

loop(4,[(2,2,0)^(1,1,2)^(1,2,8)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1)])

Narrowing the preceding formula leads to 4 summands. The current summand is given by

loop(3,[(2,3,0)^(2,2,4)^(1,1,2)^(1,2,8)^(1,3,3)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1),(2,2,0)^
                                                                                (1,1,2)^
                                                                                (1,2,8)^
                                                                                (1,3,3)^
                                                                                (2,3,4)^
                                                                                (3,3,5)^
                                                                                (3,2,6)^(3,1,7)^(2,1,1)])

Narrowing the preceding summands (5 steps) leads to the summand

loop(2,[(1,3,0)^(2,3,3)^(2,2,4)^(1,1,2)^(1,2,8)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1),
        (2,3,0)^(2,2,4)^(1,1,2)^(1,2,8)^(1,3,3)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1),(2,2,0)^
                                                                                (1,1,2)^
                                                                                (1,2,8)^
                                                                                (1,3,3)^
                                                                                (2,3,4)^
                                                                                (3,3,5)^
                                                                                (3,2,6)^(3,1,7)^(2,1,1)])

Narrowing the preceding summands (5 steps) leads to 4 summands. The current summand is given by

loop(2,[(3,3,0)^(3,2,5)^(2,2,6)^(1,1,2)^(1,2,8)^(1,3,3)^(2,3,4)^(3,1,7)^(2,1,1),
        (3,2,0)^(2,2,6)^(1,1,2)^(1,2,8)^(1,3,3)^(2,3,4)^(3,3,5)^(3,1,7)^(2,1,1),(2,2,0)^
                                                                                (1,1,2)^
                                                                                (1,2,8)^
                                                                                (1,3,3)^
                                                                                (2,3,4)^
                                                                                (3,3,5)^
                                                                                (3,2,6)^(3,1,7)^(2,1,1)])

The tree slider has been moved. The current summand is given by

loop(2,[(3,3,0)^(3,2,5)^(2,2,6)^(1,1,2)^(1,2,8)^(1,3,3)^(2,3,4)^(3,1,7)^(2,1,1),
        (3,2,0)^(2,2,6)^(1,1,2)^(1,2,8)^(1,3,3)^(2,3,4)^(3,3,5)^(3,1,7)^(2,1,1),(2,2,0)^
                                                                                (1,1,2)^
                                                                                (1,2,8)^
                                                                                (1,3,3)^
                                                                                (2,3,4)^
                                                                                (3,3,5)^
                                                                                (3,2,6)^(3,1,7)^(2,1,1)])

Narrowing the preceding summands (11 steps) leads to 4 summands. The current summand is given by

loop(0,[(3,3,0)^(3,2,5)^(3,1,6)^(2,1,7)^(2,2,1)^(1,1,2)^(1,2,8)^(1,3,3)^(2,3,4),
        (3,2,0)^(3,1,6)^(2,1,7)^(2,2,1)^(1,1,2)^(1,2,8)^(1,3,3)^(2,3,4)^(3,3,5),
        (3,1,0)^(2,1,7)^(2,2,1)^(1,1,2)^(1,2,8)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6),
        (2,1,0)^(2,2,1)^(1,1,2)^(1,2,8)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7),(2,2,0)^
                                                                                (1,1,2)^
                                                                                (1,2,8)^
                                                                                (1,3,3)^
                                                                                (2,3,4)^
                                                                                (3,3,5)^
                                                                                (3,2,6)^(3,1,7)^(2,1,1)])

The tree slider has been moved. The current summand is given by

loop(3,[(1,2,0)^(2,2,8)^(1,1,2)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1),(2,2,0)^
                                                                                (1,1,2)^
                                                                                (1,2,8)^
                                                                                (1,3,3)^
                                                                                (2,3,4)^
                                                                                (3,3,5)^
                                                                                (3,2,6)^(3,1,7)^(2,1,1)])

Narrowing the preceding summands (11 steps) leads to a single formula, which is given by

loop(2,[(1,1,0)^(1,2,2)^(2,2,8)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1),
        (1,2,0)^(2,2,8)^(1,1,2)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1),(2,2,0)^
                                                                                (1,1,2)^
                                                                                (1,2,8)^
                                                                                (1,3,3)^
                                                                                (2,3,4)^
                                                                                (3,3,5)^
                                                                                (3,2,6)^(3,1,7)^(2,1,1)])

Narrowing the preceding formula leads to the formula

loop(1,[(2,1,0)^(1,1,1)^(1,2,2)^(2,2,8)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7),
        (1,1,0)^(1,2,2)^(2,2,8)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1),
        (1,2,0)^(2,2,8)^(1,1,2)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1),(2,2,0)^
                                                                                (1,1,2)^
                                                                                (1,2,8)^
                                                                                (1,3,3)^
                                                                                (2,3,4)^
                                                                                (3,3,5)^
                                                                                (3,2,6)^(3,1,7)^(2,1,1)])

Narrowing the preceding formula leads to 2 summands. The current summand is given by

loop(0,[(2,2,0)^(2,1,8)^(1,1,1)^(1,2,2)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7),
        (2,1,0)^(1,1,1)^(1,2,2)^(2,2,8)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7),
        (1,1,0)^(1,2,2)^(2,2,8)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1),
        (1,2,0)^(2,2,8)^(1,1,2)^(1,3,3)^(2,3,4)^(3,3,5)^(3,2,6)^(3,1,7)^(2,1,1),(2,2,0)^
                                                                                (1,1,2)^
                                                                                (1,2,8)^
                                                                                (1,3,3)^
                                                                                (2,3,4)^
                                                                                (3,3,5)^
                                                                                (3,2,6)^(3,1,7)^(2,1,1)])

Narrowing the entire formula leads to True.

Number of proof steps: 11