(Bool for (Varlist (Set (Var k))) being (Type (Nat)) (Bool for (Varlist (Set (Var i1)) , (Varlist (Set (Var i2)))) being (Type (Integer)) (Bool st (Bool (Bool (Num 2) (<=) (Set (Var k))) & (Bool (Bool (Set (Var i1)) (in) (Set (Set (Var k)) (-SD))) & (Bool (Set (Var i2)) (in) (Set (Set (Var k)) (-SD_Sub))))) holds (Bool (Set (SDSub_Add_Data) "(" (Set "(" (Set (Var i1)) (+) (Set (Var i2)) ")") , (Set (Var k)) ")") (in) (Set (Set (Var k)) (-SD_Sub_S))))))