Abduction: earlier termination of the loop

[yutakang]

We should break out of the loop as soon as we complete the proof of final goal here.

[yutakang]

We need to replace fold with something else?

val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b to something like... val breakable_fold: ('a -> 'b -> ( 'b * bool) ) -> 'a list -> 'b -> ( 'b * bool ) where bool is used to indicate if the final goal is proved or not. That is, the condition to break out of the loop / fold.

[yutakang]

We can implement this with Synchronized.var and Par_List.find_some.

[yutakang]

Done.