3.7.61. Contractible

        𝚊𝚕𝚕_𝚍𝚒𝚏𝚏𝚎𝚛_𝚏𝚛𝚘𝚖_𝚊𝚝_𝚕𝚎𝚊𝚜𝚝_𝚔_𝚙𝚘𝚜 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂),

        𝚊𝚕𝚕_𝚍𝚒𝚏𝚏𝚎𝚛_𝚏𝚛𝚘𝚖_𝚎𝚡𝚊𝚌𝚝𝚕𝚢_𝚔_𝚙𝚘𝚜 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂),

        𝚊𝚕𝚕_𝚎𝚚𝚞𝚊𝚕 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚕𝚕_𝚒𝚗𝚌𝚘𝚖𝚙𝚊𝚛𝚊𝚋𝚕𝚎 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂),

        𝚊𝚕𝚕_𝚖𝚒𝚗_𝚍𝚒𝚜𝚝 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝_𝚋𝚎𝚝𝚠𝚎𝚎𝚗_𝚜𝚎𝚝𝚜 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝_𝚌𝚜𝚝 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝_𝚎𝚡𝚌𝚎𝚙𝚝_0 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝_𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝_𝚖𝚘𝚍𝚞𝚕𝚘 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝_𝚘𝚗_𝚒𝚗𝚝𝚎𝚛𝚜𝚎𝚌𝚝𝚒𝚘𝚗 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂1),

        𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝_𝚘𝚗_𝚒𝚗𝚝𝚎𝚛𝚜𝚎𝚌𝚝𝚒𝚘𝚗 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂2),

        𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝_𝚙𝚊𝚛𝚝𝚒𝚝𝚒𝚘𝚗 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚕𝚕𝚙𝚎𝚛𝚖 (suffix-contractible wrt 𝙼𝙰𝚃𝚁𝙸𝚇.𝚟𝚎𝚌),

        𝚊𝚖𝚘𝚗𝚐 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=0),

        𝚊𝚖𝚘𝚗𝚐 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|),

        𝚊𝚖𝚘𝚗𝚐_𝚍𝚒𝚏𝚏_0 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=0),

        𝚊𝚖𝚘𝚗𝚐_𝚍𝚒𝚏𝚏_0 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|),

        𝚊𝚖𝚘𝚗𝚐_𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=0),

        𝚊𝚖𝚘𝚗𝚐_𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|),

        𝚊𝚖𝚘𝚗𝚐_𝚕𝚘𝚠_𝚞𝚙 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚄𝙿=0),

        𝚊𝚖𝚘𝚗𝚐_𝚕𝚘𝚠_𝚞𝚙 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚄𝙿=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|),

        𝚊𝚖𝚘𝚗𝚐_𝚖𝚘𝚍𝚞𝚕𝚘 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=0),

        𝚊𝚖𝚘𝚗𝚐_𝚖𝚘𝚍𝚞𝚕𝚘 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|),

        𝚊𝚖𝚘𝚗𝚐_𝚜𝚎𝚚 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚄𝙿=0),

        𝚊𝚖𝚘𝚗𝚐_𝚜𝚎𝚚 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚂𝙴𝚀=1),

        𝚊𝚖𝚘𝚗𝚐_𝚜𝚎𝚚 (prefix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚖𝚘𝚗𝚐_𝚜𝚎𝚚 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚖𝚘𝚗𝚐_𝚟𝚊𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=0),

        𝚊𝚖𝚘𝚗𝚐_𝚟𝚊𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|),

        𝚊𝚛𝚒𝚝𝚑 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚛𝚒𝚝𝚑_𝚘𝚛 (contractible wrt [𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂1,𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂2]),

        𝚊𝚛𝚒𝚝𝚑_𝚜𝚕𝚒𝚍𝚒𝚗𝚐 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚁𝙴𝙻𝙾𝙿[<,] and

        𝚖𝚒𝚗𝚟𝚊𝚕(𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂.𝚟𝚊𝚛)0),

        𝚊𝚛𝚒𝚝𝚑_𝚜𝚕𝚒𝚍𝚒𝚗𝚐 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚜𝚜𝚒𝚐𝚗_𝚊𝚗𝚍_𝚌𝚘𝚞𝚗𝚝𝚜 (contractible wrt 𝙸𝚃𝙴𝙼𝚂 when 𝚁𝙴𝙻𝙾𝙿[<,]),

        𝚊𝚜𝚜𝚒𝚐𝚗_𝚊𝚗𝚍_𝚗𝚟𝚊𝚕𝚞𝚎𝚜 (contractible wrt 𝙸𝚃𝙴𝙼𝚂 when 𝚁𝙴𝙻𝙾𝙿[<,]),

        𝚊𝚝𝚖𝚘𝚜𝚝 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚝𝚖𝚘𝚜𝚝1 (contractible wrt 𝚂𝙴𝚃𝚂),

        𝚊𝚝𝚖𝚘𝚜𝚝_𝚗𝚟𝚊𝚕𝚞𝚎 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚊𝚝𝚖𝚘𝚜𝚝_𝚗𝚟𝚎𝚌𝚝𝚘𝚛 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂),

        𝚋𝚒𝚗_𝚙𝚊𝚌𝚔𝚒𝚗𝚐 (contractible wrt 𝙸𝚃𝙴𝙼𝚂),

        𝚋𝚒𝚗_𝚙𝚊𝚌𝚔𝚒𝚗𝚐_𝚌𝚊𝚙𝚊 (contractible wrt 𝙸𝚃𝙴𝙼𝚂),

        𝚌𝚊𝚕𝚎𝚗𝚍𝚊𝚛 (contractible wrt 𝙸𝙽𝚂𝚃𝙰𝙽𝚃𝚂),

        𝚌𝚑𝚊𝚗𝚐𝚎 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[,<,,>,] and 𝙽𝙲𝙷𝙰𝙽𝙶𝙴=0),

        𝚌𝚑𝚊𝚗𝚐𝚎 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[=,<,,>,] and

         𝙽𝙲𝙷𝙰𝙽𝙶𝙴=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂-1|),

        𝚌𝚘𝚕𝚘𝚞𝚛𝚎𝚍_𝚌𝚞𝚖𝚞𝚕𝚊𝚝𝚒𝚟𝚎 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚌𝚘𝚕𝚘𝚞𝚛𝚎𝚍_𝚌𝚞𝚖𝚞𝚕𝚊𝚝𝚒𝚟𝚎𝚜 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚌𝚘𝚖𝚙𝚊𝚛𝚎_𝚊𝚗𝚍_𝚌𝚘𝚞𝚗𝚝 (contractible wrt [𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂1,𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂2] when 𝙲𝙾𝚄𝙽𝚃[<,]),

        𝚌𝚘𝚗𝚝𝚊𝚒𝚗𝚜_𝚜𝚋𝚘𝚡𝚎𝚜 (suffix-contractible wrt 𝙾𝙱𝙹𝙴𝙲𝚃𝚂),

        𝚌𝚘𝚞𝚗𝚝 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚁𝙴𝙻𝙾𝙿[<,]),

        𝚌𝚘𝚞𝚗𝚝𝚜 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚁𝙴𝙻𝙾𝙿[<,]),

        𝚌𝚘𝚟𝚎𝚛𝚜_𝚜𝚋𝚘𝚡𝚎𝚜 (suffix-contractible wrt 𝙾𝙱𝙹𝙴𝙲𝚃𝚂),

        𝚌𝚞𝚖𝚞𝚕𝚊𝚝𝚒𝚟𝚎 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚌𝚞𝚖𝚞𝚕𝚊𝚝𝚒𝚟𝚎_𝚌𝚘𝚗𝚟𝚎𝚡 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚌𝚞𝚖𝚞𝚕𝚊𝚝𝚒𝚟𝚎_𝚙𝚛𝚘𝚍𝚞𝚌𝚝 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚌𝚞𝚖𝚞𝚕𝚊𝚝𝚒𝚟𝚎_𝚝𝚠𝚘_𝚍 (contractible wrt 𝚁𝙴𝙲𝚃𝙰𝙽𝙶𝙻𝙴𝚂),

        𝚌𝚞𝚖𝚞𝚕𝚊𝚝𝚒𝚟𝚎_𝚠𝚒𝚝𝚑_𝚕𝚎𝚟𝚎𝚕_𝚘𝚏_𝚙𝚛𝚒𝚘𝚛𝚒𝚝𝚢 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚌𝚞𝚖𝚞𝚕𝚊𝚝𝚒𝚟𝚎𝚜 (contractible wrt 𝚃𝙰𝚂𝙺𝚂 when 𝚁𝙴𝙻𝙾𝙿[] and 𝚖𝚒𝚗𝚟𝚊𝚕(𝚃𝙰𝚂𝙺𝚂.𝚑𝚎𝚒𝚐𝚑𝚝)0),

        𝚍𝚎𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚍𝚒𝚏𝚏𝚗 (contractible wrt 𝙾𝚁𝚃𝙷𝙾𝚃𝙾𝙿𝙴𝚂),

        𝚍𝚒𝚏𝚏𝚗_𝚌𝚘𝚕𝚞𝚖𝚗 (contractible wrt 𝙾𝚁𝚃𝙷𝙾𝚃𝙾𝙿𝙴𝚂),

        𝚍𝚒𝚏𝚏𝚗_𝚒𝚗𝚌𝚕𝚞𝚍𝚎 (contractible wrt 𝙾𝚁𝚃𝙷𝙾𝚃𝙾𝙿𝙴𝚂),

        𝚍𝚒𝚜𝚓𝚘𝚒𝚗𝚝 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂1),

        𝚍𝚒𝚜𝚓𝚘𝚒𝚗𝚝 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂2),

        𝚍𝚒𝚜𝚓𝚘𝚒𝚗𝚝_𝚜𝚋𝚘𝚡𝚎𝚜 (suffix-contractible wrt 𝙾𝙱𝙹𝙴𝙲𝚃𝚂),

        𝚍𝚒𝚜𝚓𝚘𝚒𝚗𝚝_𝚝𝚊𝚜𝚔𝚜 (contractible wrt 𝚃𝙰𝚂𝙺𝚂1),

        𝚍𝚒𝚜𝚓𝚘𝚒𝚗𝚝_𝚝𝚊𝚜𝚔𝚜 (contractible wrt 𝚃𝙰𝚂𝙺𝚂2),

        𝚍𝚒𝚜𝚓𝚞𝚗𝚌𝚝𝚒𝚟𝚎 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚍𝚒𝚜𝚓𝚞𝚗𝚌𝚝𝚒𝚟𝚎_𝚘𝚛_𝚜𝚊𝚖𝚎_𝚎𝚗𝚍 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚍𝚒𝚜𝚓𝚞𝚗𝚌𝚝𝚒𝚟𝚎_𝚘𝚛_𝚜𝚊𝚖𝚎_𝚜𝚝𝚊𝚛𝚝 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚍𝚘𝚖𝚊𝚒𝚗 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚎𝚚𝚞𝚊𝚕_𝚜𝚋𝚘𝚡𝚎𝚜 (suffix-contractible wrt 𝙾𝙱𝙹𝙴𝙲𝚃𝚂),

        𝚐𝚕𝚘𝚋𝚊𝚕_𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢 (contractible wrt 𝚅𝙰𝙻𝚄𝙴𝚂),

        𝚐𝚕𝚘𝚋𝚊𝚕_𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢_𝚕𝚘𝚠_𝚞𝚙 (contractible wrt 𝚅𝙰𝙻𝚄𝙴𝚂),

        𝚐𝚕𝚘𝚋𝚊𝚕_𝚌𝚘𝚗𝚝𝚒𝚐𝚞𝚒𝚝𝚢 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚐𝚘𝚕𝚘𝚖𝚋 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚒𝚗𝚜𝚒𝚍𝚎_𝚜𝚋𝚘𝚡𝚎𝚜 (suffix-contractible wrt 𝙾𝙱𝙹𝙴𝙲𝚃𝚂),

        𝚒𝚗𝚝_𝚟𝚊𝚕𝚞𝚎_𝚙𝚛𝚎𝚌𝚎𝚍𝚎 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚒𝚗𝚝_𝚟𝚊𝚕𝚞𝚎_𝚙𝚛𝚎𝚌𝚎𝚍𝚎_𝚌𝚑𝚊𝚒𝚗 (contractible wrt 𝚅𝙰𝙻𝚄𝙴𝚂),

        𝚒𝚗𝚝_𝚟𝚊𝚕𝚞𝚎_𝚙𝚛𝚎𝚌𝚎𝚍𝚎_𝚌𝚑𝚊𝚒𝚗 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕_𝚊𝚗𝚍_𝚌𝚘𝚞𝚗𝚝 (contractible wrt 𝙲𝙾𝙻𝙾𝚄𝚁𝚂),

        𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕_𝚊𝚗𝚍_𝚌𝚘𝚞𝚗𝚝 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕_𝚊𝚗𝚍_𝚜𝚞𝚖 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚔_𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝 (contractible wrt 𝚅𝙰𝚁𝚂),

        𝚔_𝚍𝚒𝚜𝚓𝚘𝚒𝚗𝚝 (contractible wrt 𝚂𝙴𝚃𝚂),

        𝚔_𝚜𝚊𝚖𝚎 (contractible wrt 𝚂𝙴𝚃𝚂),

        𝚔_𝚜𝚊𝚖𝚎_𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕 (contractible wrt 𝚂𝙴𝚃𝚂),

        𝚔_𝚜𝚊𝚖𝚎_𝚖𝚘𝚍𝚞𝚕𝚘 (contractible wrt 𝚂𝙴𝚃𝚂),

        𝚔_𝚜𝚊𝚖𝚎_𝚙𝚊𝚛𝚝𝚒𝚝𝚒𝚘𝚗 (contractible wrt 𝚂𝙴𝚃𝚂),

        𝚔_𝚞𝚜𝚎𝚍_𝚋𝚢 (contractible wrt 𝚂𝙴𝚃𝚂),

        𝚔_𝚞𝚜𝚎𝚍_𝚋𝚢_𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕 (contractible wrt 𝚂𝙴𝚃𝚂),

        𝚔_𝚞𝚜𝚎𝚍_𝚋𝚢_𝚖𝚘𝚍𝚞𝚕𝚘 (contractible wrt 𝚂𝙴𝚃𝚂),

        𝚔_𝚞𝚜𝚎𝚍_𝚋𝚢_𝚙𝚊𝚛𝚝𝚒𝚝𝚒𝚘𝚗 (contractible wrt 𝚂𝙴𝚃𝚂),

        𝚕𝚎𝚡_𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂),

        𝚕𝚎𝚡_𝚋𝚎𝚝𝚠𝚎𝚎𝚗 (suffix-contractible wrt [𝙻𝙾𝚆𝙴𝚁_𝙱𝙾𝚄𝙽𝙳,𝚅𝙴𝙲𝚃𝙾𝚁,𝚄𝙿𝙿𝙴𝚁_𝙱𝙾𝚄𝙽𝙳_𝙱𝙾𝚄𝙽𝙳]),

        𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚕𝚎𝚜𝚜 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂),

        𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚕𝚎𝚜𝚜𝚎𝚚 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂),

        𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚕𝚎𝚜𝚜𝚎𝚚 (suffix-contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂.𝚟𝚎𝚌),

        𝚕𝚎𝚡_𝚎𝚚𝚞𝚊𝚕 (contractible wrt [𝚅𝙴𝙲𝚃𝙾𝚁1,𝚅𝙴𝙲𝚃𝙾𝚁2]),

        𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚 (suffix-contractible wrt [𝚅𝙴𝙲𝚃𝙾𝚁1,𝚅𝙴𝙲𝚃𝙾𝚁2]),

        𝚕𝚎𝚡_𝚕𝚎𝚜𝚜𝚎𝚚 (suffix-contractible wrt [𝚅𝙴𝙲𝚃𝙾𝚁1,𝚅𝙴𝙲𝚃𝙾𝚁2]),

        𝚕𝚎𝚡_𝚕𝚎𝚜𝚜𝚎𝚚_𝚊𝚕𝚕𝚙𝚎𝚛𝚖 (suffix-contractible wrt [𝚅𝙴𝙲𝚃𝙾𝚁1,𝚅𝙴𝙲𝚃𝙾𝚁2]),

        𝚖𝚊𝚡_𝚘𝚌𝚌_𝚘𝚏_𝚌𝚘𝚗𝚜𝚎𝚌𝚞𝚝𝚒𝚟𝚎_𝚝𝚞𝚙𝚕𝚎𝚜_𝚘𝚏_𝚟𝚊𝚕𝚞𝚎𝚜 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂 when 𝙼𝙰𝚇=1),

        𝚖𝚊𝚡_𝚘𝚌𝚌_𝚘𝚏_𝚜𝚘𝚛𝚝𝚎𝚍_𝚝𝚞𝚙𝚕𝚎𝚜_𝚘𝚏_𝚟𝚊𝚕𝚞𝚎𝚜 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂 when 𝙼𝙰𝚇=1),

        𝚖𝚊𝚡_𝚘𝚌𝚌_𝚘𝚏_𝚝𝚞𝚙𝚕𝚎𝚜_𝚘𝚏_𝚟𝚊𝚕𝚞𝚎𝚜 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂 when 𝙼𝙰𝚇=1),

        𝚖𝚎𝚎𝚝_𝚜𝚋𝚘𝚡𝚎𝚜 (suffix-contractible wrt 𝙾𝙱𝙹𝙴𝙲𝚃𝚂),

        𝚖𝚞𝚕𝚝𝚒_𝚒𝚗𝚝𝚎𝚛_𝚍𝚒𝚜𝚝𝚊𝚗𝚌𝚎 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚖𝚞𝚕𝚝𝚒_𝚐𝚕𝚘𝚋𝚊𝚕_𝚌𝚘𝚗𝚝𝚒𝚐𝚞𝚒𝚝𝚢 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚗𝚊𝚗𝚍 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚅𝙰𝚁=0),

        𝚗𝚎𝚚𝚞𝚒𝚟𝚊𝚕𝚎𝚗𝚌𝚎 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝙴𝚀𝚄𝙸𝚅=1 and |𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|>0),

        𝚗𝚎𝚚𝚞𝚒𝚟𝚊𝚕𝚎𝚗𝚌𝚎 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝙴𝚀𝚄𝙸𝚅=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|),

        𝚗𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝙻=1 and |𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|>0),

        𝚗𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝙻=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|),

        𝚗𝚘_𝚙𝚎𝚊𝚔 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚗𝚘_𝚟𝚊𝚕𝚕𝚎𝚢 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚗𝚘𝚗_𝚘𝚟𝚎𝚛𝚕𝚊𝚙_𝚜𝚋𝚘𝚡𝚎𝚜 (suffix-contractible wrt 𝙾𝙱𝙹𝙴𝙲𝚃𝚂),

        𝚗𝚘𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚅𝙰𝚁=1),

        𝚗𝚘𝚝_𝚒𝚗 (contractible wrt 𝚅𝙰𝙻𝚄𝙴𝚂),

        𝚗𝚙𝚊𝚒𝚛 (contractible wrt 𝙿𝙰𝙸𝚁𝚂 when 𝙽𝙿𝙰𝙸𝚁𝚂=1 and |𝙿𝙰𝙸𝚁𝚂|>0),

        𝚗𝚙𝚊𝚒𝚛 (contractible wrt 𝙿𝙰𝙸𝚁𝚂 when 𝙽𝙿𝙰𝙸𝚁𝚂=|𝙿𝙰𝙸𝚁𝚂|),

        𝚗𝚟𝚊𝚕𝚞𝚎 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝙻=1 and |𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|>0),

        𝚗𝚟𝚊𝚕𝚞𝚎 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝙻=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|),

        𝚗𝚟𝚊𝚕𝚞𝚎_𝚘𝚗_𝚒𝚗𝚝𝚎𝚛𝚜𝚎𝚌𝚝𝚒𝚘𝚗 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂1 when 𝙽𝚅𝙰𝙻=0),

        𝚗𝚟𝚊𝚕𝚞𝚎_𝚘𝚗_𝚒𝚗𝚝𝚎𝚛𝚜𝚎𝚌𝚝𝚒𝚘𝚗 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂2 when 𝙽𝚅𝙰𝙻=0),

        𝚗𝚟𝚊𝚕𝚞𝚎𝚜 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚁𝙴𝙻𝙾𝙿[<,]),

        𝚗𝚟𝚊𝚕𝚞𝚎𝚜 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚁𝙴𝙻𝙾𝙿[=] and 𝙻𝙸𝙼𝙸𝚃=1 and |𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|>0),

        𝚗𝚟𝚊𝚕𝚞𝚎𝚜 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚁𝙴𝙻𝙾𝙿[=] and 𝙻𝙸𝙼𝙸𝚃=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|),

        𝚗𝚟𝚊𝚕𝚞𝚎𝚜_𝚎𝚡𝚌𝚎𝚙𝚝_0 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚁𝙴𝙻𝙾𝙿[<,]),

        𝚗𝚟𝚎𝚌𝚝𝚘𝚛 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂 when 𝙽𝚅𝙴𝙲=1 and |𝚅𝙴𝙲𝚃𝙾𝚁𝚂|>0),

        𝚗𝚟𝚎𝚌𝚝𝚘𝚛 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂 when 𝙽𝚅𝙴𝙲=|𝚅𝙴𝙲𝚃𝙾𝚁𝚂|,

        𝚗𝚟𝚎𝚌𝚝𝚘𝚛𝚜 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂 when 𝚁𝙴𝙻𝙾𝙿[<,]),

        𝚘𝚙𝚎𝚗_𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚘𝚙𝚎𝚗_𝚊𝚖𝚘𝚗𝚐 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝚅𝙰𝚁=0),

        𝚘𝚙𝚎𝚗_𝚊𝚝𝚖𝚘𝚜𝚝 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚘𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚅𝙰𝚁=0),

        𝚘𝚛𝚍𝚎𝚛𝚎𝚍_𝚊𝚝𝚖𝚘𝚜𝚝_𝚗𝚟𝚎𝚌𝚝𝚘𝚛 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂),

        𝚘𝚛𝚍𝚎𝚛𝚎𝚍_𝚐𝚕𝚘𝚋𝚊𝚕_𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢 (contractible wrt 𝚅𝙰𝙻𝚄𝙴𝚂),

        𝚘𝚛𝚍𝚎𝚛𝚎𝚍_𝚗𝚟𝚎𝚌𝚝𝚘𝚛 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂 when 𝙽𝚅𝙴𝙲=1 and |𝚅𝙴𝙲𝚃𝙾𝚁𝚂|>0),

        𝚘𝚛𝚍𝚎𝚛𝚎𝚍_𝚗𝚟𝚎𝚌𝚝𝚘𝚛 (contractible wrt 𝚅𝙴𝙲𝚃𝙾𝚁𝚂 when 𝙽𝚅𝙴𝙲=|𝚅𝙴𝙲𝚃𝙾𝚁𝚂|),

        𝚘𝚛𝚝𝚑_𝚕𝚒𝚗𝚔_𝚘𝚛𝚒_𝚜𝚒𝚣_𝚎𝚗𝚍 (contractible wrt 𝙾𝚁𝚃𝙷𝙾𝚃𝙾𝙿𝙴),

        𝚘𝚟𝚎𝚛𝚕𝚊𝚙_𝚜𝚋𝚘𝚡𝚎𝚜 (suffix-contractible wrt 𝙾𝙱𝙹𝙴𝙲𝚃𝚂),

        𝚙𝚊𝚝𝚝𝚎𝚛𝚗 (prefix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚙𝚊𝚝𝚝𝚎𝚛𝚗 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚙𝚎𝚊𝚔 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽=0),

        𝚙𝚎𝚛𝚒𝚘𝚍 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[=] and 𝙿𝙴𝚁𝙸𝙾𝙳=1),

        𝚙𝚎𝚛𝚒𝚘𝚍 (prefix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚙𝚎𝚛𝚒𝚘𝚍 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚙𝚎𝚛𝚒𝚘𝚍_𝚎𝚡𝚌𝚎𝚙𝚝_0 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[=] and 𝙿𝙴𝚁𝙸𝙾𝙳=1),

        𝚙𝚎𝚛𝚒𝚘𝚍_𝚎𝚡𝚌𝚎𝚙𝚝_0 (prefix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚙𝚎𝚛𝚒𝚘𝚍_𝚎𝚡𝚌𝚎𝚙𝚝_0 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚙𝚎𝚛𝚒𝚘𝚍_𝚟𝚎𝚌𝚝𝚘𝚛𝚜 (prefix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚙𝚎𝚛𝚒𝚘𝚍_𝚟𝚎𝚌𝚝𝚘𝚛𝚜 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚙𝚛𝚘𝚍𝚞𝚌𝚝_𝚌𝚝𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[<,] and

        𝚖𝚒𝚗𝚟𝚊𝚕(𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂.𝚟𝚊𝚛)>0),

        𝚛𝚊𝚗𝚐𝚎_𝚌𝚝𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[<,]),

        𝚜𝚊𝚖𝚎_𝚊𝚗𝚍_𝚐𝚕𝚘𝚋𝚊𝚕_𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢 (contractible wrt 𝚅𝙰𝙻𝚄𝙴𝚂),

        𝚜𝚊𝚖𝚎_𝚊𝚗𝚍_𝚐𝚕𝚘𝚋𝚊𝚕_𝚌𝚊𝚛𝚍𝚒𝚗𝚊𝚕𝚒𝚝𝚢_𝚕𝚘𝚠_𝚞𝚙 (contractible wrt 𝚅𝙰𝙻𝚄𝙴𝚂),

        𝚜𝚌𝚊𝚕𝚊𝚛_𝚙𝚛𝚘𝚍𝚞𝚌𝚝 (contractible wrt 𝙻𝙸𝙽𝙴𝙰𝚁𝚃𝙴𝚁𝙼 when 𝙲𝚃𝚁[<,],

        𝚖𝚒𝚗𝚟𝚊𝚕(𝙻𝙸𝙽𝙴𝙰𝚁𝚃𝙴𝚁𝙼.𝚌𝚘𝚎𝚏𝚏)0 and 𝚖𝚒𝚗𝚟𝚊𝚕(𝙻𝙸𝙽𝙴𝙰𝚁𝚃𝙴𝚁𝙼.𝚟𝚊𝚛)0),

        𝚜𝚎𝚝_𝚟𝚊𝚕𝚞𝚎_𝚙𝚛𝚎𝚌𝚎𝚍𝚎 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚕𝚒𝚍𝚒𝚗𝚐_𝚍𝚒𝚜𝚝𝚛𝚒𝚋𝚞𝚝𝚒𝚘𝚗 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚂𝙴𝚀=1),

        𝚜𝚕𝚒𝚍𝚒𝚗𝚐_𝚍𝚒𝚜𝚝𝚛𝚒𝚋𝚞𝚝𝚒𝚘𝚗 (prefix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚕𝚒𝚍𝚒𝚗𝚐_𝚍𝚒𝚜𝚝𝚛𝚒𝚋𝚞𝚝𝚒𝚘𝚗 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚕𝚒𝚍𝚒𝚗𝚐_𝚍𝚒𝚜𝚝𝚛𝚒𝚋𝚞𝚝𝚒𝚘𝚗 (contractible wrt 𝚅𝙰𝙻𝚄𝙴𝚂),

        𝚜𝚕𝚒𝚍𝚒𝚗𝚐_𝚜𝚞𝚖 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝚂𝙴𝚀=1),

        𝚜𝚕𝚒𝚍𝚒𝚗𝚐_𝚜𝚞𝚖 (prefix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚕𝚒𝚍𝚒𝚗𝚐_𝚜𝚞𝚖 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚕𝚒𝚍𝚒𝚗𝚐_𝚝𝚒𝚖𝚎_𝚠𝚒𝚗𝚍𝚘𝚠 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚜𝚕𝚒𝚍𝚒𝚗𝚐_𝚝𝚒𝚖𝚎_𝚠𝚒𝚗𝚍𝚘𝚠_𝚏𝚛𝚘𝚖_𝚜𝚝𝚊𝚛𝚝 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚜𝚕𝚒𝚍𝚒𝚗𝚐_𝚝𝚒𝚖𝚎_𝚠𝚒𝚗𝚍𝚘𝚠_𝚜𝚞𝚖 (contractible wrt 𝚃𝙰𝚂𝙺𝚂),

        𝚜𝚖𝚘𝚘𝚝𝚑 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝙲𝙷𝙰𝙽𝙶𝙴=0),

        𝚜𝚖𝚘𝚘𝚝𝚑 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽𝙲𝙷𝙰𝙽𝙶𝙴=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|-1),

        𝚜𝚘𝚏𝚝_𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝_𝚌𝚝𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚘𝚏𝚝_𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝_𝚟𝚊𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚝𝚛𝚒𝚌𝚝𝚕𝚢_𝚍𝚎𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚝𝚛𝚒𝚌𝚝𝚕𝚢_𝚒𝚗𝚌𝚛𝚎𝚊𝚜𝚒𝚗𝚐 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚞𝚖_𝚌𝚝𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[<,] and

        𝚖𝚒𝚗𝚟𝚊𝚕(𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂.𝚟𝚊𝚛)0),

        𝚜𝚞𝚖_𝚌𝚝𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[,>] and

        𝚖𝚊𝚡𝚟𝚊𝚕(𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂.𝚟𝚊𝚛)0),

        𝚜𝚞𝚖_𝚌𝚞𝚋𝚎𝚜_𝚌𝚝𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[<,] and

        𝚖𝚒𝚗𝚟𝚊𝚕(𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂.𝚟𝚊𝚛)0),

        𝚜𝚞𝚖_𝚌𝚞𝚋𝚎𝚜_𝚌𝚝𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[,>] and

        𝚖𝚊𝚡𝚟𝚊𝚕(𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂.𝚟𝚊𝚛)0),

        𝚜𝚞𝚖_𝚙𝚘𝚠𝚎𝚛𝚜4_𝚌𝚝𝚛 (𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂) when 𝙲𝚃𝚁[<,],

        𝚜𝚞𝚖_𝚙𝚘𝚠𝚎𝚛𝚜5_𝚌𝚝𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[<,] and

        𝚖𝚒𝚗𝚟𝚊𝚕(𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂.𝚟𝚊𝚛)0),

        𝚜𝚞𝚖_𝚙𝚘𝚠𝚎𝚛𝚜5_𝚌𝚝𝚛 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙲𝚃𝚁[,>] and

        𝚖𝚊𝚡𝚟𝚊𝚕(𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂.𝚟𝚊𝚛)0),

        𝚜𝚞𝚖_𝚙𝚘𝚠𝚎𝚛𝚜6_𝚌𝚝𝚛 (𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂) when 𝙲𝚃𝚁[<,],

        𝚜𝚞𝚖_𝚘𝚏_𝚒𝚗𝚌𝚛𝚎𝚖𝚎𝚗𝚝𝚜 (prefix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚞𝚖_𝚘𝚏_𝚒𝚗𝚌𝚛𝚎𝚖𝚎𝚗𝚝𝚜 (suffix-contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂),

        𝚜𝚞𝚖_𝚜𝚚𝚞𝚊𝚛𝚎𝚜_𝚌𝚝𝚛 (𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂) when 𝙲𝚃𝚁[<,],

        𝚝𝚠𝚒𝚗 (contractible wrt 𝙿𝙰𝙸𝚁𝚂),

        𝚞𝚜𝚎𝚍_𝚋𝚢 (𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂2),

        𝚞𝚜𝚎𝚍_𝚋𝚢_𝚒𝚗𝚝𝚎𝚛𝚟𝚊𝚕 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂2),

        𝚞𝚜𝚎𝚍_𝚋𝚢_𝚖𝚘𝚍𝚞𝚕𝚘 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂2),

        𝚞𝚜𝚎𝚍_𝚋𝚢_𝚙𝚊𝚛𝚝𝚒𝚝𝚒𝚘𝚗 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂2),

        𝚞𝚜𝚎𝚜 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂2),

        𝚟𝚊𝚕𝚕𝚎𝚢 (contractible wrt 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 when 𝙽=0),

        𝚟𝚎𝚌_𝚎𝚚_𝚝𝚞𝚙𝚕𝚎 (contractible wrt [𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂,𝚃𝚄𝙿𝙻𝙴]).

A contractible constraint is a constraint for which, given any satisfied ground instance, one can remove any item from one of its collection arguments, without affecting that the resulting constraint still holds, assuming all its restrictions hold. A typical example of a contractible constraint is the 𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝 constraint: given any ground satisfied instance, e.g., 𝚊𝚕𝚕𝚍𝚒𝚏𝚏𝚎𝚛𝚎𝚗𝚝(3,8,1), we can remove any value from its unique argument without affecting that the resulting constraint still holds. We generalise slightly the original definition of contractibility introduced by  [Maher09c] in the following ways:

  • The sequence of variables is replaced by a collection. Consequently, variables are replaced by items. For instance, in the context of the 𝚌𝚞𝚖𝚞𝚕𝚊𝚝𝚒𝚟𝚎(𝚃𝙰𝚂𝙺𝚂,𝙻𝙸𝙼𝙸𝚃) constraint, we can remove any task from 𝚃𝙰𝚂𝙺𝚂 from any satisfied instance without affecting that the resulting constraint still holds (e.g., if the resource limit 𝙻𝙸𝙼𝙸𝚃 is not exceeded at any point in time, this still is the case if we remove any task, i.e., since task heights are restricted to be non negative).

  • Since the constraint may have more than one argument, one has to explicitly specify the argument from which one may remove items.

  • Items cannot only be removed from the end of a collection like in  [Maher09c], but also from the beginning or from any part. Allowing to remove items from the beginning is called prefix-contractibility, while permitting to remove items from the end is called suffix-contractibility. Removing items from any part is just called contractibility. As an example, consider the 𝚊𝚖𝚘𝚗𝚐_𝚜𝚎𝚚(𝙻𝙾𝚆,𝚄𝙿,𝚂𝙴𝚀,𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂,𝚅𝙰𝙻𝚄𝙴𝚂) constraint which forces all sequences of 𝚂𝙴𝚀 consecutive variables of the collection 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 to be assigned at least 𝙻𝙾𝚆 and at most 𝚄𝙿 values from 𝚅𝙰𝙻𝚄𝙴𝚂. The constraint 𝚊𝚖𝚘𝚗𝚐_𝚜𝚎𝚚 is not contractible w.r.t. the collection 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂, since removing an item in the middle of 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 creates a new sequence for which the restriction with respect to 𝙻𝙾𝚆 and 𝚄𝙿 may not hold. However, if we restrict ourselves to removing just a prefix or suffix from 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂, then the corresponding 𝚊𝚖𝚘𝚗𝚐_𝚜𝚎𝚚 constraint still holds, since no new sequence is created.

  • A constraint may be contractible only if certain restrictions apply to some of its arguments. This is done by explicitly providing a list of restrictions, each restriction corresponding to one of the restrictions described in Section 2.2.3. We call this conditional contractibility. Given a source and a target constraint (i.e., the target constraint corresponds to the source constraint from which we remove some items in some arguments) all arguments of the target constraint should be identical to the arguments of the source constraint, except:

    • Argument corresponding to a collection from which we remove items.

    • Argument 𝚊𝚛𝚐 occurring in the list of conditional restrictions with of restriction of the form 𝚊𝚛𝚐=f(|c|), where c is an argument corresponding to a collection from which we remove items and f a function.

    In addition, all restrictions from the list of restrictions should apply both to the source and target constraints.

    We now provide two examples of conditional contractibility with respect to the 𝚊𝚖𝚘𝚗𝚐(𝙽𝚅𝙰𝚁,𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂,𝚅𝙰𝙻𝚄𝙴𝚂) constraint, which forces 𝙽𝚅𝙰𝚁 to be the number of variables of the collection 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 that are assigned a value in 𝚅𝙰𝙻𝚄𝙴𝚂.

    • In general 𝚊𝚖𝚘𝚗𝚐 is not contractible since removing an item from 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 may change the value of 𝙽𝚅𝙰𝚁. However, given a ground satisfied instance for which 𝙽𝚅𝙰𝚁 is set to 0, we can remove any item from 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 without affecting that the constraint still holds. In this context, the two arguments 𝙽𝚅𝙰𝚁 and 𝚅𝙰𝙻𝚄𝙴𝚂 are left unchanged within the source and the target constraint.

      As an illustration, consider the source constraint 𝚊𝚖𝚘𝚗𝚐(0,2,4,2,1,5) and the target constraint 𝚊𝚖𝚘𝚗𝚐(0,2,2,1,5). Since 𝙽𝚅𝙰𝚁 is set to 0 both in the source and the target constraint and since 𝚅𝙰𝙻𝚄𝙴𝚂 is set to the same list of values both in the source and the target constraint, we have that 𝚊𝚖𝚘𝚗𝚐(0,2,4,2,1,5) implies 𝚊𝚖𝚘𝚗𝚐(0,2,2,1,5).

    • Similarly, when 𝙽𝚅𝙰𝚁 is equal to |𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂|, all variables are assigned a value in 𝚅𝙰𝙻𝚄𝙴𝚂. In this context, we can remove any variable from 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 to get a new constraint that still holds, provided that the restriction 𝙽𝚅𝙰𝚁=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂| still holds. In this example only the argument 𝚅𝙰𝙻𝚄𝙴𝚂 is left unchanged between the source and the target constraint. 𝙽𝚅𝙰𝚁 changes since it occurs in a restriction of the form 𝙽𝚅𝙰𝚁=|𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂| in the list of conditional restrictions.

      As an illustration, consider the source constraint 𝚊𝚖𝚘𝚗𝚐(3,2,4,2,0,2,4,6,8) and the target constraint 𝚊𝚖𝚘𝚗𝚐(2,4,2,0,2,4,6,8). Since 𝙽𝚅𝙰𝚁 is set to the number of items of the 𝚅𝙰𝚁𝙸𝙰𝙱𝙻𝙴𝚂 collection both in the source and the target constraint, and since 𝚅𝙰𝙻𝚄𝙴𝚂 is set to the same list of values both in the source and the target constraint, we have that 𝚊𝚖𝚘𝚗𝚐(3,2,4,2,0,2,4,6,8) implies 𝚊𝚖𝚘𝚗𝚐(2,4,2,0,2,4,6,8).

  • Finally, a last extension corresponds to the fact that the sequence of variables from which we remove elements may be replaced by several collections. In this context, items are removed simultaneously from all collections from exactly the same set of positions. A set of collections is either defined by a list of collections, or by a collection and one of its attributes, which is itself a collection.

    As a first example, consider the 𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚(𝚅𝙴𝙲𝚃𝙾𝚁1,𝚅𝙴𝙲𝚃𝙾𝚁2) constraint, which given two vectors each defined by a collection of variables of the same length, forces that 𝚅𝙴𝙲𝚃𝙾𝚁1 is lexicographically greater than or equal to 𝚅𝙴𝙲𝚃𝙾𝚁2. We have that 𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚 is suffix-contractible with respect to 𝚅𝙴𝙲𝚃𝙾𝚁1 and 𝚅𝙴𝙲𝚃𝙾𝚁2. This means that we can remove the k (1k|𝚅𝙴𝙲𝚃𝙾𝚁1|) last items from collections 𝚅𝙴𝙲𝚃𝙾𝚁1 and 𝚅𝙴𝙲𝚃𝙾𝚁2. Note that the k items should be removed from both collections simultaneously. As an illustration, consider the source constraint 𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚(5,2,8,9,5,2,6,2) and the target constraint 𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚(5,2,8,5,2,6). Since 𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚 is suffix-contractible with respect to the two collections 𝚅𝙴𝙲𝚃𝙾𝚁1 and 𝚅𝙴𝙲𝚃𝙾𝚁2, we have that 𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚(5,2,8,9,5,2,6,2) implies 𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚(5,2,8,5,2,6).

    As a second example, consider the 𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚕𝚎𝚜𝚜𝚎𝚚(𝚅𝙴𝙲𝚃𝙾𝚁𝚂) constraint, which given a collection of vectors each of them defined by a collection of variables of the same length, forces the i 𝑡ℎ vector to be lexicographically less than or equal to the (i+1) 𝑡ℎ vector (1i<|𝚅𝙴𝙲𝚃𝙾𝚁𝚂|). We have that 𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚕𝚎𝚜𝚜𝚎𝚚 is suffix-contractible with respect to 𝚅𝙴𝙲𝚃𝙾𝚁𝚂.𝚟𝚎𝚌. This means that we can remove the k last components of each vectors of the 𝚅𝙴𝙲𝚃𝙾𝚁𝚂 collection. As in the previous example the k items should be removed from all collections simultaneously. As an illustration, consider the source constraint 𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚕𝚎𝚜𝚜𝚎𝚚(𝚟𝚎𝚌-5,2,3,9,𝚟𝚎𝚌-5,2,6,2,𝚟𝚎𝚌-5,2,6,2) and the target constraint 𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚕𝚎𝚜𝚜𝚎𝚚(𝚟𝚎𝚌-5,2,3,𝚟𝚎𝚌-5,2,6,𝚟𝚎𝚌-5,2,6). Since 𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚕𝚎𝚜𝚜𝚎𝚚 is suffix-contractible with respect to 𝚅𝙴𝙲𝚃𝙾𝚁𝚂.𝚟𝚎𝚌, we have that 𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚕𝚎𝚜𝚜𝚎𝚚(𝚟𝚎𝚌-5,2,3,9,𝚟𝚎𝚌-5,2,6,2,𝚟𝚎𝚌-5,2,6,2) implies 𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚕𝚎𝚜𝚜𝚎𝚚(𝚟𝚎𝚌-5,2,3,𝚟𝚎𝚌-5,2,6,𝚟𝚎𝚌-5,2,6).

The keyword extensible introduces a dual notion, where items can be added to a collection that is passed as an argument of a satisfied global constraint without affecting the fact that the resulting constraint is satisfied. Contractibility is a more common property than extensibility.