-
Notifications
You must be signed in to change notification settings - Fork 2
/
TextFile1.txt
83 lines (83 loc) · 10.3 KB
/
TextFile1.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
Imp(And(set [a_1..n; m]), c), Imp(And(set [a; a_1..n]), c) -> [(Imp(a, m), Some(ind(tv1, tv2)), None)]
Imp(And(set [a; a_1..n]), c), Imp(a, m) -> [(Imp(And(set [a_1..n; m]), c), Some(abd(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p -> [(Imp(Inh(p, $1), Inh(s, $1)), Some(abd(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p -> [(Imp(Inh(s, $1), Inh(p, $1)), Some(ind(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p -> [(Equ(Inh(p, $1), Inh(s, $1)), Some(com(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p -> [(And(set [Inh(p, #2); Inh(s, #2)]), Some(int(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p,measure_time(i) -> [(PreImp(Seq([Inh(p, $1); i]), Inh(s, $1)), Some(abd(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p,measure_time(i) -> [(RetImp(Inh(s, $1), Seq([Inh(p, $1); i])), Some(ind(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p,measure_time(i) -> [(PreEqu(Seq([Inh(p, $1); i]), Inh(s, $1)), Some(com(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p,measure_time(i) -> [(Seq([Inh(p, #2); i; Inh(s, #2)]), Some(int(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p,concurrent(task,belief) -> [(ConImp(Inh(p, $1), Inh(s, $1)), Some(abd(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p,concurrent(task,belief) -> [(ConImp(Inh(s, $1), Inh(p, $1)), Some(ind(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p,concurrent(task,belief) -> [(ConEqu(Inh(p, $1), Inh(s, $1)), Some(com(tv1, tv2)), None)]
Inh(s, m), Inh(p, m) when s <> p,concurrent(task,belief) -> [(Par(set [Inh(p, #2); Inh(s, #2)]), Some(int(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p -> [(Imp(Inh($1, s), Inh($1, p)), Some(ind(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p -> [(Imp(Inh($1, p), Inh($1, s)), Some(abd(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p -> [(Equ(Inh($1, s), Inh($1, p)), Some(com(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p -> [(And(set [Inh(#2, p); Inh(#2, s)]), Some(int(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p,measure_time(i) -> [(PreImp(Seq([Inh($1, s); i]), Inh($1, p)), Some(ind(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p,measure_time(i) -> [(RetImp(Inh($1, p), Seq([Inh($1, s); i])), Some(abd(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p,measure_time(i) -> [(PreEqu(Seq([Inh($1, s); i]), Inh($1, p)), Some(com(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p,measure_time(i) -> [(Seq([Inh(#2, s); i; Inh(#2, p)]), Some(int(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p,concurrent((m --> p),(m --> s)) -> [(ConImp(Inh($1, s), Inh($1, p)), Some(ind(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p,concurrent((m --> p),(m --> s)) -> [(ConImp(Inh($1, p), Inh($1, s)), Some(abd(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p,concurrent((m --> p),(m --> s)) -> [(ConEqu(Inh($1, s), Inh($1, p)), Some(com(tv1, tv2)), None)]
Inh(m, s), Inh(m, p) when s <> p,concurrent((m --> p),(m --> s)) -> [(Par(set [Inh(#2, p); Inh(#2, s)]), Some(int(tv1, tv2)), None)]
Imp(a, Inh(m, p)), Inh(m, s) when a <> (m --> s) -> [(Imp(And(set [a; Inh($1, s)]), Inh($1, p)), Some(ind(tv1, tv2)), None)]
Imp(a, Inh(m, p)), Inh(m, s) when a <> (m --> s) -> [(And(set [Inh(#2, s); Imp(a, Inh(#2, p))]), Some(int(tv1, tv2)), None)]
And(set [a_1..n; Inh(m, p)]), Inh(m, s) when s <> p -> [(Imp(Inh($2, s), And(set [a_1..n; Inh($2, p)])), Some(ind(tv1, tv2)), None)]
And(set [a_1..n; Inh(m, p)]), Inh(m, s) when s <> p -> [(And(set [a_1..n; Inh(#2, p); Inh(#2, s)]), Some(int(tv1, tv2)), None)]
Imp(a, Inh(p, m)), Inh(s, m) when s <> p,a <> (s --> m) -> [(Imp(And(set [a; Inh(p, $1)]), Inh(s, $1)), Some(abd(tv1, tv2)), None)]
Imp(a, Inh(p, m)), Inh(s, m) when s <> p,a <> (s --> m) -> [(And(set [Inh(s, #2); Imp(a, Inh(p, #2))]), Some(int(tv1, tv2)), None)]
And(set [a_1..n; Inh(p, m)]), Inh(s, m) when s <> p -> [(Imp(Inh(s, $2), And(set [a_1..n; Inh(p, $2)])), Some(abd(tv1, tv2)), None)]
And(set [a_1..n; Inh(p, m)]), Inh(s, m) when s <> p -> [(And(set [a_1..n; Inh(p, #2); Inh(s, #2)]), Some(int(tv1, tv2)), None)]
And(set [a; a_1..n]), b when substitute_if_unifies(#,a,b) -> [(And(set [a_1..n]), Some(anonAna(tv1, tv2)), Some(desireStrong(tv1, tv2)))]
Imp(Inh(a, r), z), Imp(And(set [a_1..n; Inh(#2, b); Inh(#2, r)]), z) -> [(Inh(a, b), Some(abd(tv1, tv2)), None)]
Imp(Inh(a, r), z), Imp(And(set [Inh(#2, b); Inh(#2, r)]), z) -> [(Inh(a, b), Some(abd(tv1, tv2)), None)]
Inh(u, l), Imp(And(set [Inh(#1, l); Inh(#1, r)]), z) -> [(Imp(Inh(u, r), z), Some(ded(tv1, tv2)), None)]
Inh(u, l), Imp(And(set [a_1..n; Inh(#1, l); Inh(#1, r)]), z) when substitute(#1,u) -> [(Imp(And(set [a_1..n; Inh(u, r)]), z), Some(ded(tv1, tv2)), None)]
b, Imp(a, c) when substitute_if_unifies($,a,b),shift_occurrence_forward(a,==>) -> [(c, Some(ded(tv1, tv2)), None)]
b, Imp(c, a) when substitute_if_unifies($,a,b),shift_occurrence_backward(a,==>) -> [(c, Some(abd(tv1, tv2)), None)]
b, Equ(a, c) when substitute_if_unifies($,a,b),shift_occurrence_backward(c,<=>) -> [(c, Some(ded(tv1, tv2)), None)]
b, Equ(c, a) when substitute_if_unifies($,a,b),shift_occurrence_forward(c,<=>) -> [(c, Some(ded(tv1, tv2)), None)]
Inh(a, k), And(set [Inh(#1, l); Imp(Inh($2, k), And(set [a_1..n]))]) when substitute($2,a) -> [(And(set [a_1..n; Inh(#1, l)]), Some(ded(tv1, tv2)), None)]
Inh(a, k), Imp(Inh($1, l), And(set [a_1..n; Inh(#2, k)])) when substitute(#2,a) -> [(Imp(Inh($1, l), And(set [a_1..n])), Some(anonAna(tv1, tv2)), None)]
Imp(And(set [a_1..n; c]), z), Imp(And(set [b_1..m; c]), z) -> [(Imp(And(set [a_1..n]), And(set [b_1..m])), Some(ind(tv1, tv2)), None)]
Imp(And(set [a_1..n; c]), z), Imp(And(set [b_1..m; c]), z) -> [(Imp(And(set [b_1..m]), And(set [a_1..n])), Some(ind(tv1, tv2)), None)]
Imp(z, And(set [a_1..n; c])), Imp(z, And(set [b_1..m; c])) -> [(Imp(And(set [a_1..n]), And(set [b_1..m])), Some(abd(tv1, tv2)), None)]
Imp(z, And(set [a_1..n; c])), Imp(z, And(set [b_1..m; c])) -> [(Imp(And(set [b_1..m]), And(set [a_1..n])), Some(abd(tv1, tv2)), None)]
Inh(a, l), Imp(Inh(a, s), r) -> [(Imp(And(set [Inh(#1, l); Inh(#1, s)]), r), Some(ind(tv1, tv2)), None)]
Inh(a, l), Imp(And(set [a_1..n; Inh(a, s)]), r) when substitute(a,#1) -> [(Imp(And(set [a_1..n; Inh(#1, l); Inh(#1, s)]), r), Some(int(tv1, tv2)), None)]
x, Imp(bi, y) when substitute_if_unifies($,y,x),shift_occurrence_backward(bi,==>) -> [(bi, Some(abd(tv1, tv2)), Some(ded(tv1, tv2)))]
p, s when after(task,belief),measure_time(i),not_implication_or_equivalence(p),not_implication_or_equivalence(s) -> [(PreImp(Seq([s; i]), p), Some(ind(tv1, tv2)), None)]
p, s when after(task,belief),measure_time(i),not_implication_or_equivalence(p),not_implication_or_equivalence(s) -> [(RetImp(p, Seq([s; i])), Some(abd(tv1, tv2)), None)]
p, s when after(task,belief),measure_time(i),not_implication_or_equivalence(p),not_implication_or_equivalence(s) -> [(PreEqu(Seq([s; i]), p), Some(com(tv1, tv2)), None)]
p, s when after(task,belief),not_conjunction(p),not_conjunction(s),measure_time(i),not_implication_or_equivalence(p),not_implication_or_equivalence(s) -> [(Seq([s; i; p]), Some(int(tv1, tv2)), None)]
p, s when concurrent(task,belief),not_implication_or_equivalence(p),not_implication_or_equivalence(s) -> [(ConImp(s, p), Some(ind(tv1, tv2)), None)]
p, s when concurrent(task,belief),not_implication_or_equivalence(p),not_implication_or_equivalence(s) -> [(ConImp(p, s), Some(ind(tv1, tv2)), None)]
p, s when concurrent(task,belief),not_implication_or_equivalence(p),not_implication_or_equivalence(s) -> [(ConEqu(s, p), Some(com(tv1, tv2)), None)]
p, s when concurrent(task,belief),not_conjunction(p),not_conjunction(s),not_implication_or_equivalence(p),not_implication_or_equivalence(s) -> [(Par(set [p; s]), Some(int(tv1, tv2)), None)]
Inh(a, s), Inh(b, s) when task(?) -> [(Inh(a, b), None, None)]
Inh(a, s), Inh(b, s) when task(?) -> [(Inh(b, a), None, None)]
Sim(IntSet([a]), IntSet([b])), Sim(a, b) when task(?) -> [(Sim(IntSet([a]), IntSet([b])), Some(beliefId(tv1, tv2)), None)]
Sim(ExtSet([a]), ExtSet([b])), Sim(a, b) when task(?) -> [(Sim(ExtSet([a]), ExtSet([b])), Some(beliefId(tv1, tv2)), None)]
Inh(IntSet([a]), IntSet([b])), Sim(a, b) when task(?) -> [(Inh(IntSet([a]), IntSet([b])), Some(beliefId(tv1, tv2)), None)]
Inh(ExtSet([a]), ExtSet([b])), Sim(a, b) when task(?) -> [(Inh(ExtSet([a]), ExtSet([b])), Some(beliefId(tv1, tv2)), None)]
Inh(ExtInt(set [a_1..n; b]), ExtInt(set [a; a_1..n])), Inh(b, a) when task(?) -> [(Inh(ExtInt(set [a_1..n; b]), ExtInt(set [a; a_1..n])), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(IntInt(set [a_1..n; b]), IntInt(set [a; a_1..n])), Inh(b, a) when task(?) -> [(Inh(IntInt(set [a_1..n; b]), IntInt(set [a; a_1..n])), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(ExtDif(s, a), ExtDif(s, b)), Inh(b, a) when task(?) -> [(Inh(ExtDif(s, a), ExtDif(s, b)), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(IntDif(s, a), IntDif(s, b)), Inh(b, a) when task(?) -> [(Inh(IntDif(s, a), IntDif(s, b)), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(w, IntInt(set [a_1..n; b])), Inh(w, b) when task(?) -> [(Inh(w, IntInt(set [a_1..n; b])), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(ExtInt(set [a_1..n; b]), w), Inh(b, w) when task(?) -> [(Inh(ExtInt(set [a_1..n; b]), w), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(w, ExtDif(s, b)), Inh(w, b) when task(?) -> [(Inh(w, ExtDif(s, b)), Some(beliefStructuralDif(tv1, tv2)), None)]
Inh(IntDif(s, b), w), Inh(b, w) when task(?) -> [(Inh(IntDif(s, b), w), Some(beliefStructuralDif(tv1, tv2)), None)]
Inh(Prod([b; p), ?1), Inh(b, a) when task(?) -> [(Inh(Prod([b; p), Prod([a; p)), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(Prod([b; p), Prod([a; p)), Inh(b, a) when task(?) -> [(Inh(Prod([b; p), Prod([a; p)), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(IntImg([n; a; _]), ?1), Inh(n, r) when task(?) -> [(Inh(IntImg([n; a; _]), IntImg([r; a; _])), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(IntImg([n; a; _]), IntImg([r; a; _])), Inh(n, r) when task(?) -> [(Inh(IntImg([n; a; _]), IntImg([r; a; _])), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(ExtImg([n; _; b]), ?1), Inh(s, b) when task(?) -> [(Inh(ExtImg([n; _; b]), ExtImg([n; _; s])), Some(beliefStrucuralDed(tv1, tv2)), None)]
Inh(ExtImg([n; _; b]), ExtImg([n; _; s])), Inh(s, b) when task(?) -> [(Inh(ExtImg([n; _; b]), ExtImg([n; _; s])), Some(beliefStrucuralDed(tv1, tv2)), None)]
Not(a), a when task(?) -> [(Not(a), Some(beliefNeg(tv1, tv2)), None)]
a, Not(a) when task(?) -> [(a, Some(beliefNeg(tv1, tv2)), None)]
Or(set [a_1..n; b]), b when task(?) -> [(Or(set [a_1..n; b]), Some(beliefStrucuralDed(tv1, tv2)), None)]