-
Notifications
You must be signed in to change notification settings - Fork 1
/
ex4b-parse.txt
194 lines (170 loc) · 5.63 KB
/
ex4b-parse.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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
PARSE Foo v Bar
Orig: [FoovBar] Binary [v]
LHS: [Foo] Unary [symbol]: [Foo]
RHS: [Bar] Unary [symbol]: [Bar]
PARSE Foo ^ (Bar v Baz)
Orig: [Foo^(BarvBaz)] Binary [^]
LHS: [Foo] Unary [symbol]: [Foo]
RHS: [(BarvBaz)] Unary [()]
Sub: [BarvBaz] Binary [v]
LHS: [Bar] Unary [symbol]: [Bar]
RHS: [Baz] Unary [symbol]: [Baz]
PARSE P ^ (Q ^ (R ^ (S ^ T)))
Orig: [P^(Q^(R^(S^T)))] Binary [^]
LHS: [P] Unary [symbol]: [P]
RHS: [(Q^(R^(S^T)))] Unary [()]
Sub: [Q^(R^(S^T))] Binary [^]
LHS: [Q] Unary [symbol]: [Q]
RHS: [(R^(S^T))] Unary [()]
Sub: [R^(S^T)] Binary [^]
LHS: [R] Unary [symbol]: [R]
RHS: [(S^T)] Unary [()]
Sub: [S^T] Binary [^]
LHS: [S] Unary [symbol]: [S]
RHS: [T] Unary [symbol]: [T]
PARSE (((P v Q) v R) v S) v T
Orig: [(((PvQ)vR)vS)vT] Binary [v]
LHS: [(((PvQ)vR)vS)] Unary [()]
Sub: [((PvQ)vR)vS] Binary [v]
LHS: [((PvQ)vR)] Unary [()]
Sub: [(PvQ)vR] Binary [v]
LHS: [(PvQ)] Unary [()]
Sub: [PvQ] Binary [v]
LHS: [P] Unary [symbol]: [P]
RHS: [Q] Unary [symbol]: [Q]
RHS: [R] Unary [symbol]: [R]
RHS: [S] Unary [symbol]: [S]
RHS: [T] Unary [symbol]: [T]
PARSE P => (Q => (R => (S => T)))
Orig: [P=>(Q=>(R=>(S=>T)))] Binary [=>]
LHS: [P] Unary [symbol]: [P]
RHS: [(Q=>(R=>(S=>T)))] Unary [()]
Sub: [Q=>(R=>(S=>T))] Binary [=>]
LHS: [Q] Unary [symbol]: [Q]
RHS: [(R=>(S=>T))] Unary [()]
Sub: [R=>(S=>T)] Binary [=>]
LHS: [R] Unary [symbol]: [R]
RHS: [(S=>T)] Unary [()]
Sub: [S=>T] Binary [=>]
LHS: [S] Unary [symbol]: [S]
RHS: [T] Unary [symbol]: [T]
PARSE ((P <=> Q) <=> ~R) <=> ~(S <=> ~(T <=> ~U))
Orig: [((P<=>Q)<=>~R)<=>~(S<=>~(T<=>~U))] Binary [<=>]
LHS: [((P<=>Q)<=>~R)] Unary [()]
Sub: [(P<=>Q)<=>~R] Binary [<=>]
LHS: [(P<=>Q)] Unary [()]
Sub: [P<=>Q] Binary [<=>]
LHS: [P] Unary [symbol]: [P]
RHS: [Q] Unary [symbol]: [Q]
RHS: [~R] Unary [~]
Sub: [R] Unary [symbol]: [R]
RHS: [~(S<=>~(T<=>~U))] Unary [~]
Sub: [(S<=>~(T<=>~U))] Unary [()]
Sub: [S<=>~(T<=>~U)] Binary [<=>]
LHS: [S] Unary [symbol]: [S]
RHS: [~(T<=>~U)] Unary [~]
Sub: [(T<=>~U)] Unary [()]
Sub: [T<=>~U] Binary [<=>]
LHS: [T] Unary [symbol]: [T]
RHS: [~U] Unary [~]
Sub: [U] Unary [symbol]: [U]
PARSE (P ^ Q) => (R <=> ~S)
Orig: [(P^Q)=>(R<=>~S)] Binary [=>]
LHS: [(P^Q)] Unary [()]
Sub: [P^Q] Binary [^]
LHS: [P] Unary [symbol]: [P]
RHS: [Q] Unary [symbol]: [Q]
RHS: [(R<=>~S)] Unary [()]
Sub: [R<=>~S] Binary [<=>]
LHS: [R] Unary [symbol]: [R]
RHS: [~S] Unary [~]
Sub: [S] Unary [symbol]: [S]
PARSE ((P v ~Q) <=> ((S ^ ~S) v Foo))
Orig: [((Pv~Q)<=>((S^~S)vFoo))] Unary [()]
Sub: [(Pv~Q)<=>((S^~S)vFoo)] Binary [<=>]
LHS: [(Pv~Q)] Unary [()]
Sub: [Pv~Q] Binary [v]
LHS: [P] Unary [symbol]: [P]
RHS: [~Q] Unary [~]
Sub: [Q] Unary [symbol]: [Q]
RHS: [((S^~S)vFoo)] Unary [()]
Sub: [(S^~S)vFoo] Binary [v]
LHS: [(S^~S)] Unary [()]
Sub: [S^~S] Binary [^]
LHS: [S] Unary [symbol]: [S]
RHS: [~S] Unary [~]
Sub: [S] Unary [symbol]: [S]
RHS: [Foo] Unary [symbol]: [Foo]
PARSE ~((P v ~Q) <=> (~(S ^ ~S) v Foo))
Orig: [~((Pv~Q)<=>(~(S^~S)vFoo))] Unary [~]
Sub: [((Pv~Q)<=>(~(S^~S)vFoo))] Unary [()]
Sub: [(Pv~Q)<=>(~(S^~S)vFoo)] Binary [<=>]
LHS: [(Pv~Q)] Unary [()]
Sub: [Pv~Q] Binary [v]
LHS: [P] Unary [symbol]: [P]
RHS: [~Q] Unary [~]
Sub: [Q] Unary [symbol]: [Q]
RHS: [(~(S^~S)vFoo)] Unary [()]
Sub: [~(S^~S)vFoo] Binary [v]
LHS: [~(S^~S)] Unary [~]
Sub: [(S^~S)] Unary [()]
Sub: [S^~S] Binary [^]
LHS: [S] Unary [symbol]: [S]
RHS: [~S] Unary [~]
Sub: [S] Unary [symbol]: [S]
RHS: [Foo] Unary [symbol]: [Foo]
PARSE ~~~((P v ~Q) <=> ~((~(S ^ ~S) v Foo)))
Orig: [~~~((Pv~Q)<=>~((~(S^~S)vFoo)))] Unary [~]
Sub: [~~((Pv~Q)<=>~((~(S^~S)vFoo)))] Unary [~]
Sub: [~((Pv~Q)<=>~((~(S^~S)vFoo)))] Unary [~]
Sub: [((Pv~Q)<=>~((~(S^~S)vFoo)))] Unary [()]
Sub: [(Pv~Q)<=>~((~(S^~S)vFoo))] Binary [<=>]
LHS: [(Pv~Q)] Unary [()]
Sub: [Pv~Q] Binary [v]
LHS: [P] Unary [symbol]: [P]
RHS: [~Q] Unary [~]
Sub: [Q] Unary [symbol]: [Q]
RHS: [~((~(S^~S)vFoo))] Unary [~]
Sub: [((~(S^~S)vFoo))] Unary [()]
Sub: [(~(S^~S)vFoo)] Unary [()]
Sub: [~(S^~S)vFoo] Binary [v]
LHS: [~(S^~S)] Unary [~]
Sub: [(S^~S)] Unary [()]
Sub: [S^~S] Binary [^]
LHS: [S] Unary [symbol]: [S]
RHS: [~S] Unary [~]
Sub: [S] Unary [symbol]: [S]
RHS: [Foo] Unary [symbol]: [Foo]
PARSE (((P))) ^ (((Q)))
Orig: [(((P)))^(((Q)))] Binary [^]
LHS: [(((P)))] Unary [()]
Sub: [((P))] Unary [()]
Sub: [(P)] Unary [()]
Sub: [P] Unary [symbol]: [P]
RHS: [(((Q)))] Unary [()]
Sub: [((Q))] Unary [()]
Sub: [(Q)] Unary [()]
Sub: [Q] Unary [symbol]: [Q]
PARSE (((P => Q) ^ ~(P => Q)) ^ (R v S)) <=> (Foo v Bar)
Orig: [(((P=>Q)^~(P=>Q))^(RvS))<=>(FoovBar)] Binary [<=>]
LHS: [(((P=>Q)^~(P=>Q))^(RvS))] Unary [()]
Sub: [((P=>Q)^~(P=>Q))^(RvS)] Binary [^]
LHS: [((P=>Q)^~(P=>Q))] Unary [()]
Sub: [(P=>Q)^~(P=>Q)] Binary [^]
LHS: [(P=>Q)] Unary [()]
Sub: [P=>Q] Binary [=>]
LHS: [P] Unary [symbol]: [P]
RHS: [Q] Unary [symbol]: [Q]
RHS: [~(P=>Q)] Unary [~]
Sub: [(P=>Q)] Unary [()]
Sub: [P=>Q] Binary [=>]
LHS: [P] Unary [symbol]: [P]
RHS: [Q] Unary [symbol]: [Q]
RHS: [(RvS)] Unary [()]
Sub: [RvS] Binary [v]
LHS: [R] Unary [symbol]: [R]
RHS: [S] Unary [symbol]: [S]
RHS: [(FoovBar)] Unary [()]
Sub: [FoovBar] Binary [v]
LHS: [Foo] Unary [symbol]: [Foo]
RHS: [Bar] Unary [symbol]: [Bar]