MAYBE 0.07/0.19 MAYBE 0.07/0.19 0.07/0.19 Problem: 0.07/0.19 Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) 0.07/0.19 Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) 0.07/0.19 Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) 0.07/0.19 Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) 0.07/0.19 Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) 0.07/0.19 Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) 0.07/0.19 Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) 0.07/0.19 Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) 0.07/0.19 Term_sub(Term_var(x),Id()) -> Term_var(x) 0.07/0.19 Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m 0.07/0.19 Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) 0.07/0.19 Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) 0.07/0.19 Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) 0.07/0.19 Sum_sub(xi,Id()) -> Sum_term_var(xi) 0.07/0.19 Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) 0.07/0.19 Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) 0.07/0.19 Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) 0.07/0.19 Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 0.07/0.19 Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) 0.07/0.19 Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) 0.07/0.19 Concat(Id(),s) -> s 0.07/0.19 0.07/0.19 Proof: 0.07/0.19 Open 0.17/0.20 EOF