Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
lemma(1, [], ap(right_to_left(o), []): (p(o);dom(A), less(o, A), p(A))). lemma(2, [p(o)], ap(serial_less(o), []): (dom(A), less(o, A))). lemma(3, [ (dom(par(0)), less(o, par(0))), p(o)], ap(right_to_left(par(0)), []): (p(par(0));dom(A), less(par(0), A), p(A))). lemma(4, [p(par(0)), (dom(par(0)), less(o, par(0))), p(o)], ap(left_to_right(o, par(0)), [p(o), less(o, par(0)), p(par(0))]):false). lemma(5, [p(par(0)), (dom(par(0)), less(o, par(0))), p(o)], ap(false_ind(goal), [4]):goal). lemma(6, [ (dom(par(1)), less(par(0), par(1)), p(par(1))), (dom(par(0)), less(o, par(0))), p(o)], ap(transitive_less(o, par(0), par(1)), [less(o, par(0)), less(par(0), par(1))]):less(o, par(1))). lemma(7, [ (dom(par(1)), less(par(0), par(1)), p(par(1))), (dom(par(0)), less(o, par(0))), p(o)], ap(left_to_right(o, par(1)), [p(o), 6, p(par(1))]):false). lemma(8, [ (dom(par(1)), less(par(0), par(1)), p(par(1))), (dom(par(0)), less(o, par(0))), p(o)], ap(false_ind(goal), [7]):goal). lemma(9, [ (dom(par(0)), less(o, par(0))), p(o)], ap(or_elim(3), [5, 8]):goal). lemma(10, [p(o)], ap(ex_elim(2), 9):goal). lemma(11, [ (dom(par(0)), less(o, par(0)), p(par(0)))], ap(serial_less(par(0)), []): (dom(A), less(par(0), A))). lemma(12, [ (dom(par(1)), less(par(0), par(1))), (dom(par(0)), less(o, par(0)), p(par(0)))], ap(right_to_left(par(1)), []): (p(par(1));dom(A), less(par(1), A), p(A))). lemma(13, [p(par(1)), (dom(par(1)), less(par(0), par(1))), (dom(par(0)), less(o, par(0)), p(par(0)))], ap(left_to_right(par(0), par(1)), [p(par(0)), less(par(0), par(1)), p(par(1))]):false). lemma(14, [p(par(1)), (dom(par(1)), less(par(0), par(1))), (dom(par(0)), less(o, par(0)), p(par(0)))], ap(false_ind(goal), [13]):goal). lemma(15, [ (dom(par(2)), less(par(1), par(2)), p(par(2))), (dom(par(1)), less(par(0), par(1))), (dom(par(0)), less(o, par(0)), p(par(0)))], ap(transitive_less(o, par(0), par(1)), [less(o, par(0)), less(par(0), par(1))]):less(o, par(1))). lemma(16, [ (dom(par(2)), less(par(1), par(2)), p(par(2))), (dom(par(1)), less(par(0), par(1))), (dom(par(0)), less(o, par(0)), p(par(0)))], ap(transitive_less(par(0), par(1), par(2)), [less(par(0), par(1)), less(par(1), par(2))]):less(par(0), par(2))). lemma(17, [ (dom(par(2)), less(par(1), par(2)), p(par(2))), (dom(par(1)), less(par(0), par(1))), (dom(par(0)), less(o, par(0)), p(par(0)))], ap(left_to_right(par(0), par(2)), [p(par(0)), 16, p(par(2))]):false). lemma(18, [ (dom(par(2)), less(par(1), par(2)), p(par(2))), (dom(par(1)), less(par(0), par(1))), (dom(par(0)), less(o, par(0)), p(par(0)))], ap(false_ind(goal), [17]):goal). lemma(19, [ (dom(par(1)), less(par(0), par(1))), (dom(par(0)), less(o, par(0)), p(par(0)))], ap(or_elim(12), [14, 18]):goal). lemma(20, [ (dom(par(0)), less(o, par(0)), p(par(0)))], ap(ex_elim(11), 19):goal). lemma(21, [], ap(or_elim(1), [10, 20]):goal). [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 17, 18, 19, 20, 21]