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(assump, []): (re(a, b), re(a, c))). lemma(2, [], ap(ref_e(a), []):e(a, a)). lemma(3, [], ap(ref_e(b), []):e(b, b)). lemma(4, [], ap(ref_e(c), []):e(c, c)). lemma(5, [], ap(e_in_re(a, a), [2]):re(a, a)). lemma(6, [], ap(e_in_re(b, b), [3]):re(b, b)). lemma(7, [], ap(e_in_re(c, c), [4]):re(c, c)). lemma(8, [], ap(e_or_r(a, b), [1:1]): (e(a, b);r(a, b))). lemma(9, [e(a, b)], ap(sym_e(a, b), [e(a, b)]):e(b, a)). lemma(10, [e(a, b)], ap(congl(b, a, c), [9, 2:1]):re(b, c)). lemma(11, [e(a, b)], ap(goal_ax(c), [10, 7]):goal). lemma(12, [r(a, b)], ap(e_or_r(a, c), [2:1]): (e(a, c);r(a, c))). lemma(13, [e(a, c), r(a, b)], ap(sym_e(a, c), [e(a, c)]):e(c, a)). lemma(14, [e(a, c), r(a, b)], ap(congl(c, a, b), [13, 1:1]):re(c, b)). lemma(15, [e(a, c), r(a, b)], ap(goal_ax(b), [6, 14]):goal). lemma(16, [r(a, c), r(a, b)], ap(dp_r(a, b, b), [r(a, b), r(a, b)]): (dom(A), r(b, A), r(b, A))). lemma(17, [ (dom(par(0)), r(b, par(0)), r(b, par(0))), r(a, c), r(a, b)], ap(ref_e(par(0)), []):e(par(0), par(0))). lemma(18, [ (dom(par(0)), r(b, par(0)), r(b, par(0))), r(a, c), r(a, b)], ap(e_in_re(par(0), par(0)), [17]):re(par(0), par(0))). lemma(19, [ (dom(par(0)), r(b, par(0)), r(b, par(0))), r(a, c), r(a, b)], ap(r_in_re(b, par(0)), [r(b, par(0))]):re(b, par(0))). lemma(20, [ (dom(par(0)), r(b, par(0)), r(b, par(0))), r(a, c), r(a, b)], ap(dp_r(a, b, c), [r(a, b), r(a, c)]): (dom(A), r(b, A), r(c, A))). lemma(21, [ (dom(par(1)), r(b, par(1)), r(c, par(1))), (dom(par(0)), r(b, par(0)), r(b, par(0))), r(a, c), r(a, b)], ap(ref_e(par(1)), []):e(par(1), par(1))). lemma(22, [ (dom(par(1)), r(b, par(1)), r(c, par(1))), (dom(par(0)), r(b, par(0)), r(b, par(0))), r(a, c), r(a, b)], ap(e_in_re(par(1), par(1)), [21]):re(par(1), par(1))). lemma(23, [ (dom(par(1)), r(b, par(1)), r(c, par(1))), (dom(par(0)), r(b, par(0)), r(b, par(0))), r(a, c), r(a, b)], ap(r_in_re(b, par(1)), [r(b, par(1))]):re(b, par(1))). lemma(24, [ (dom(par(1)), r(b, par(1)), r(c, par(1))), (dom(par(0)), r(b, par(0)), r(b, par(0))), r(a, c), r(a, b)], ap(r_in_re(c, par(1)), [r(c, par(1))]):re(c, par(1))). lemma(25, [ (dom(par(1)), r(b, par(1)), r(c, par(1))), (dom(par(0)), r(b, par(0)), r(b, par(0))), r(a, c), r(a, b)], ap(goal_ax(par(1)), [23, 24]):goal). lemma(26, [ (dom(par(0)), r(b, par(0)), r(b, par(0))), r(a, c), r(a, b)], ap(ex_elim(20), 25):goal). lemma(27, [r(a, c), r(a, b)], ap(ex_elim(16), 26):goal). lemma(28, [r(a, b)], ap(or_elim(12), [15, 27]):goal). lemma(29, [], ap(or_elim(8), [11, 28]):goal). [1, 3, 4, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 20, 23, 24, 25, 26, 27, 28, 29]