% Background theory about lists with natural numbers list: type. %name list L. nil : list. ; : nat -> list -> list. %infix right 10 ;. % some abbreviations for numbers: 1 = (s z). 2 = (s (s z)). 3 = (s (s (s z))). 4 = (s (s (s (s z)))). 5 = (s (s (s (s (s z))))). % Horn Theory for append app: list -> list -> list -> type. a_nil: app nil L L. a_; : app (H ; L) L1 (H ; L2) <- app L L1 L2. %query 1 * D : app (1 ; 2 ; 3 ; nil) (4 ; 5 ; nil) (1 ; 2 ; 3 ; 4 ; 5 ; nil). % Horn Theory for delete delete: nat -> list -> list -> type. del_nil : delete X nil nil. del_x: delete X (X ; L) L' <- delete X L L'. del_y: delete X (Y ; L) (Y ; L') <- delete X L L'. % note: can delete multiple occurrences %query 1 * D : delete 5 (1 ; 2 ; 3 ; 4 ; 5 ; nil) (1 ; 2 ; 3 ; 4 ; nil). %query 1 * D : delete 1 (1 ; 2 ; 1 ; 3 ; 1 ; nil) (2 ; 3 ; nil).