Differences

This shows you the differences between two versions of the page.

--- teaching:is:ind-solutions [2020/06/24 16:48]
Franconi Enrico [12.6]
+++ teaching:is:ind-solutions [2020/06/24 17:11] (current)
Franconi Enrico [12.9]
@@ Line 142: / Line 142: @@
      resolve with imm_west(r109,r111)
      substitution: {R/r111}
-  yes(r11) ⇐
+  yes(r111) ⇐
 ===== 12.8 =====
+(a)
+  f(X,X,c,X,c)
+(b)
+  yes(c(l,X1),L) ⇐ append(c(l,X1),c(L,nil),c(l,c(i,c(s,c(t,nil)))))
+<nowiki>(c)</nowiki>
+  append(c(l,X1),c(L,nil),c(l,c(i,c(s,c(t,nil))))) ⇐
+     append(X1,c(L,nil), c(l,c(i,c(s,c(t,nil)))))
 ===== 12.9 =====
+(a)
+  {Z/f(X),Y/g(b)}
+(b)
+  {W/f(t),X/t,Q/t}
+<nowiki>(c)</nowiki>
+  {P/val(X,bb),Z/val(X,bb)}
 ===== 12.14 =====
+(a) Here is a top-down derivation:
+  yes(Y) ⇐ adj(b,Y,c(a,c(b,c(b,c(a,emp))))).
+    choose clause 3, with { A/b,B/Y,L/c(a,c(b,c(b,c(a,emp)))),F/F1,E/E1 }
+  yes(Y) ⇐ ap(F1,c(b,c(Y,E1)),c(a,c(b,c(b,c(a,emp)))))
+    choose clause 2, under
+    { F1/c(a,T2),L/c(b,c(Y,E1)),H/a,R/c(b,c(b,c(a,emp))),T/T2 }
+  yes(Y) ⇐ ap(T2,c(b,c(Y,E1)),c(b,c(b,c(a,emp))))   (*)
+    choose clause 1 under { T2/emp,Y/b,E1/c(b,c(a,emp)) }
+  yes(b) ⇐
+(b) Yes, there is one more answer .
+  at (*)
+    choose clause 2 under
+    { T2/c(b,T3),L/c(b,c(Y,E1)),H/b,R/c(b,c(a,emp)),T/T3 }
+  yes(Y) <- ap(T3,c(b,c(Y,E1)),c(b,c(a,emp)))
+    choose clause 1 under { T3/emp,L/c(b,c(a,emp)),Y/a,E1/emp
+  yes(a) <-

FranconiSpace