%Patch files loaded: patch2 version 2.414 $$$pvs-strategies (defstep rewrite-destr (destr name &optional fnum occur) (let ((struct-name (format nil "~a_struct" name))) (then* (expand name fnum occur) (repeat* (rewrite destr fnum)) (rewrite name :DIR RL) (expand struct-name fnum occur) (assert))) "(rewrite-destr destr name &optional fnum occur): Applies the destructor rewriting rule to the coinductive definition name and expands the corresponding structure map" "~%By rewriting ~a for ~a and expanding the structure") $$$ax_seq.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % A COALGEBRAIC THEORY OF SEQUENCES IN PVS % % % % by BART JACOBS and ULRICH HENSEL % % % % (bart@cs.kun.nl and hensel@tcs.inf.tu-dresden.de) % % % % % % version 2.0, 24/6/98 % % % % (works in PVS version 2.414) % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Lift[X : TYPE] : DATATYPE BEGIN bot : bot? up(down : X) : up? END Lift Lift_prop[X : TYPE] : THEORY BEGIN IMPORTING Lift cover : LEMMA FORALL(z:Lift[X]) : z = bot OR (EXISTS(x:X) : z = up(x)) up_exist : LEMMA FORALL(z:Lift[X]) : up?(z) IFF (EXISTS(x:X) : z = up(x)) mono_up : LEMMA FORALL(x1,x2:X) : up(x1) = up(x2) IMPLIES x1 = x2 END Lift_prop Seq_defn[A : TYPE] : THEORY BEGIN IMPORTING Lift_prop Seq : TYPE struct_map_existence : AXIOM EXISTS(f:[Seq->Lift[[A,Seq]]]) : TRUE next : [Seq -> Lift[[A,Seq]]] END Seq_defn Seq_ax[A,X : TYPE] : THEORY BEGIN IMPORTING Seq_defn struct : VAR [X -> Lift[[A,X]]] struct_map?(struct) : PRED[[X -> Seq[A]]] = LAMBDA(f : [X -> Seq[A]]) : FORALL(x:X) : (bot?[[A,X]](struct(x)) IMPLIES bot?[[A,Seq[A]]](next(f(x)))) AND (up?[[A,X]](struct(x)) IMPLIES next(f(x)) = up[[A,Seq[A]]](proj_1(down(struct(x))), f(proj_2(down(struct(x)))))) seq_finality : AXIOM EXISTS(f:[X->Seq[A]]) : struct_map?(struct)(f) AND FORALL(g:[X->Seq[A]]) : struct_map?(struct)(g) IMPLIES g = f coreduce(struct) : {f:[X->Seq[A]] | struct_map?(struct)(f) AND FORALL(g:[X->Seq[A]]) : struct_map?(struct)(g) IMPLIES g = f} coreduce_struct_map : LEMMA struct_map?(struct)(coreduce(struct)) coreduce_unique : LEMMA FORALL(g:[X->Seq[A]]) : struct_map?(struct)(g) IMPLIES g = coreduce(struct) struct_map_unique : LEMMA FORALL(g,h:[X->Seq[A]]) : struct_map?(struct)(g) AND struct_map?(struct)(h) IMPLIES g = h next : LEMMA FORALL(x:X) : next(coreduce(struct)(x)) = IF bot?(struct(x)) THEN bot ELSE up(proj_1(down(struct(x))), coreduce(struct)(proj_2(down(struct(x))))) ENDIF END Seq_ax % Intermezzo, demonstrating the validity of the seq_finality axiom SeqImpl[A : TYPE] : THEORY BEGIN IMPORTING Lift Seq_impl : TYPE = { f : [nat -> Lift[A]] | FORALL(n : nat) : bot?(f(n)) IMPLIES bot?(f(n+1)) } shift : [Seq_impl -> Seq_impl] = LAMBDA(f : Seq_impl) : LAMBDA(n : nat) : f(n+1) next_impl : [Seq_impl -> Lift[[A, Seq_impl]]] = LAMBDA(f : Seq_impl) : IF bot?(f(0)) THEN bot[[A, Seq_impl]] ELSE up[[A, Seq_impl]](down[A](f(0)), shift(f)) ENDIF END SeqImpl SeqImplFinality[A, X : TYPE] : THEORY BEGIN IMPORTING Seq_ax[A, X], SeqImpl[A], Least_nat struct : VAR [X -> Lift[[A,X]]] n, m : VAR nat x : VAR X iter(struct, n)(x) : RECURSIVE Lift[[A, X]] = IF n = 0 THEN struct(x) ELSE IF bot?(iter(struct, n-1)(x)) THEN bot[[A, X]] ELSE struct(proj_2(down[[A, X]](iter(struct, n-1)(x)))) ENDIF ENDIF MEASURE n iter_exchange : LEMMA FORALL(n : nat) : up?[[A, X]](struct(x)) IMPLIES iter(struct, n)(proj_2(down[[A, X]](struct(x)))) = iter(struct, n+1)(x) cored(struct) : [X -> Seq_impl[A]] = LAMBDA(x : X) : LAMBDA(n : nat) : IF bot?(iter(struct, n)(x)) THEN bot[A] ELSE up[A](proj_1(down(iter(struct, n)(x)))) ENDIF struct_map_bot : LEMMA bot?[[A,X]](struct(x)) IMPLIES bot?[[A,Seq_impl[A]]](next_impl(cored(struct)(x))) struct_map_up : LEMMA up?[[A,X]](struct(x)) IMPLIES next_impl(cored(struct)(x)) = up[[A,Seq_impl[A]]](proj_1(down(struct(x))), cored(struct)(proj_2(down(struct(x))))) struct_map_unique : LEMMA FORALL(f : [X -> Seq_impl[A]]) : (FORALL(x : X) : (bot?[[A,X]](struct(x)) IMPLIES bot?[[A,Seq_impl[A]]](next_impl(f(x)))) AND (up?[[A,X]](struct(x)) IMPLIES next_impl(f(x)) = up[[A,Seq_impl[A]]](proj_1(down(struct(x))), f(proj_2(down(struct(x))))))) IMPLIES f = cored(struct) END SeqImplFinality % End of intermezzo Bisim[A,X1,X2 : TYPE] : THEORY BEGIN IMPORTING Seq_ax struct1 : VAR [X1 -> Lift[[A,X1]]] struct2 : VAR [X2 -> Lift[[A,X2]]] bisimulation?(struct1,struct2) : PRED[PRED[[X1,X2]]] = LAMBDA(R:PRED[[X1,X2]]) : FORALL(x1:X1,x2:X2) : R(x1,x2) IMPLIES IF bot?(struct1(x1)) THEN IF bot?(struct2(x2)) THEN TRUE ELSE FALSE ENDIF ELSE IF bot?(struct2(x2)) THEN FALSE ELSE proj_1(down(struct1(x1))) = proj_1(down(struct2(x2))) AND R(proj_2(down(struct1(x1))),proj_2(down(struct2(x2)))) ENDIF ENDIF bisim?(struct1,struct2) : PRED[[X1,X2]] = LAMBDA(x1:X1,x2:X2) : EXISTS(R:PRED[[X1,X2]]) : bisimulation?(struct1,struct2)(R) AND R(x1,x2) bisim_bisim : LEMMA bisimulation?(struct1,struct2)(bisim?(struct1,struct2)) incl(struct1,struct2)(R:(bisimulation?(struct1,struct2))) : [(R) -> [X1,X2]] = LAMBDA(z:(R)) : (proj_1(z),proj_2(z)) bisim_struct(struct1,struct2)(R:(bisimulation?(struct1,struct2))) : [(R) -> Lift[[A,(R)]]] = LAMBDA(z:(R)) : IF bot?(struct1(proj_1(incl(struct1,struct2)(R)(z)))) THEN bot[[A,(R)]] ELSE up[[A,(R)]]( proj_1(down(struct1(proj_1(incl(struct1,struct2)(R)(z))))), (proj_2(down(struct1(proj_1(incl(struct1,struct2)(R)(z))))), proj_2(down(struct2(proj_2(incl(struct1,struct2)(R)(z))))))) ENDIF bisim_struct_map : LEMMA FORALL(R:PRED[[X1,X2]]) : bisimulation?(struct1,struct2)(R) IMPLIES struct_map?(bisim_struct(struct1,struct2)(R))(LAMBDA(z:(R)) : coreduce(struct1)(proj_1(incl(struct1,struct2)(R)(z)))) AND struct_map?(bisim_struct(struct1,struct2)(R))(LAMBDA(z:(R)) : coreduce(struct2)(proj_2(incl(struct1,struct2)(R)(z)))) Kernel(struct1,struct2) : PRED[[X1,X2]] = LAMBDA(x1:X1,x2:X2) : coreduce(struct1)(x1) = coreduce(struct2)(x2) Kernel_bisim : LEMMA bisimulation?(struct1,struct2)(Kernel(struct1,struct2)) bisim_finality : LEMMA FORALL(x1:X1,x2:X2) : bisim?(struct1,struct2)(x1,x2) IFF Kernel(struct1,struct2)(x1,x2) END Bisim Seq_functoriality[A,B : TYPE] : THEORY BEGIN IMPORTING Seq_ax seq_map_struct(f:[A->B]) : [Seq[A] -> Lift[[B,Seq[A]]]] = LAMBDA(x:Seq[A]) : IF bot?(next(x)) THEN bot[[B,Seq[A]]] ELSE up[[B,Seq[A]]](f(proj_1(down[[A,Seq[A]]](next(x)))), proj_2(down[[A,Seq[A]]](next(x)))) ENDIF seq_map(f:[A->B]) : [Seq[A] -> Seq[B]] = coreduce(seq_map_struct(f)) END Seq_functoriality Least_nat : THEORY BEGIN least(p:(nonempty?[nat])) : {n:nat| p(n) AND FORALL(m:nat) : p(m) IMPLIES n<=m} END Least_nat Seq_prop[A : TYPE] : THEORY BEGIN IMPORTING Seq_ax, Least_nat, Bisim id_coreduce: LEMMA FORALL(x: Seq[A]): x = coreduce[A,Seq[A]](next[A])(x); next_inv_struct : [Lift[[A,Seq[A]]] -> Lift[[A,Lift[[A,Seq[A]]]]]] = LAMBDA(z:Lift[[A,Seq[A]]]) : IF bot?(z) THEN bot ELSE up(proj_1(down(z)), next(proj_2(down(z)))) ENDIF next_inv : [Lift[[A,Seq[A]]] -> Seq[A]] = coreduce(next_inv_struct) next_iso : LEMMA (FORALL(x:Lift[[A,Seq[A]]]) : next(next_inv(x)) = x) AND (FORALL(y:Seq[A]) : next_inv(next(y)) = y) final_bisim_finality : LEMMA FORALL(R:PRED[[Seq[A],Seq[A]]]) : bisimulation?(next,next)(R) IMPLIES FORALL(x,y:Seq[A]) : R(x,y) IMPLIES x = y empty_seq : Seq[A] = next_inv(bot[[A,Seq[A]]]) next_empty : LEMMA next(empty_seq) = bot empty_unique : LEMMA FORALL(x:Seq[A]) : bot?(next(x)) IMPLIES x = empty_seq cons_seq : [[A,Seq[A]] -> Seq[A]] = LAMBDA(a:A, x: Seq[A]) : next_inv(up(a,x)) next_cons : LEMMA FORALL(a:A, x: Seq[A]) : next(cons_seq(a,x)) = up(a,x) cons_unique : LEMMA FORALL(a:A, x,y: Seq[A]) : next(y) = up(a,x) IMPLIES y = cons_seq(a,x) not_bot_next : LEMMA FORALL(x:Seq[A]) : NOT bot?(next(x)) IMPLIES EXISTS(a:A, y:Seq[A]) : x = cons_seq(a,y) cons_list(l:list[A],x:Seq[A]) : RECURSIVE Seq[A] = CASES l OF null : x, cons(a,k) : cons_seq(a,cons_list(k,x)) ENDCASES MEASURE (LAMBDA(l:list[A],x:Seq[A]) : length(l)) cons_list_mono : LEMMA FORALL(x,y:Seq[A],l,k:list[A]) : length(l) = length(k) AND cons_list(l,x) = cons_list(k,y) IMPLIES l = k singleton_seq : [A -> Seq[A]] = LAMBDA(a:A) : cons_seq(a,empty_seq) const_seq_struct : [A -> Lift[[A,A]]] = LAMBDA(a:A) : up(a,a) const_seq : [A -> Seq[A]] = coreduce(const_seq_struct) at(x:Seq[A], n:nat) : RECURSIVE Lift[A] = IF n=0 THEN IF bot?(next(x)) THEN bot ELSE up(proj_1(down(next(x)))) ENDIF ELSE IF bot?(next(x)) THEN bot ELSE at(proj_2(down(next(x))),n-1) ENDIF ENDIF MEASURE (LAMBDA(x:Seq[A], n:nat) : n) at_empty : LEMMA FORALL(n:nat) : at(empty_seq,n) = bot at_cons : LEMMA FORALL(x:Seq[A], a:A, n:nat) : at(x,n) = at(cons_seq(a,x),n+1) at_singleton_seq : LEMMA FORALL(a:A,n:nat) : at(singleton_seq(a),n) = IF n = 0 THEN up(a) ELSE bot ENDIF at_const_seq : LEMMA FORALL(a:A,n:nat) : at(const_seq(a),n) = up(a) tail(x:Seq[A], n:nat) : RECURSIVE Seq[A] = IF n=0 THEN x ELSIF bot?(next(x)) THEN empty_seq ELSE tail(proj_2(down(next(x))),n-1) ENDIF MEASURE (LAMBDA(x:Seq[A], n:nat) : n) tail : [Seq[A] -> Seq[A]] = LAMBDA(x:Seq[A]) : tail(x,1) tail_empty : LEMMA FORALL(n:nat) : tail(empty_seq,n) = empty_seq tail_cons : LEMMA FORALL(x:Seq[A], a:A, n:nat) : tail(x,n) = tail(cons_seq(a,x),n+1) tail_list : LEMMA FORALL(x:Seq[A],l:list[A],n:nat) : tail(x,n) = tail(cons_list(l,x),n+length(l)) tail_succ : LEMMA FORALL(x:Seq[A], n:nat) : tail(x,n+1) = tail(tail(x,n),1) tail_tail : LEMMA FORALL(x:Seq[A], n,m:nat) : tail(tail(x,n),m) = tail(x,n+m) at_tail : LEMMA FORALL(x:Seq[A], n,m:nat) : at(tail(x,n),m) = at(x,n+m) cons_at_tail : LEMMA FORALL(x:Seq[A]) : bot?(at(x,0)) OR x = cons_seq(down(at(x,0)),tail(x,1)) at_bot_tail : LEMMA FORALL(x:Seq[A],n:nat) : bot?(at(x,n)) IMPLIES tail(x,n) = empty_seq tail_singleton_seq : LEMMA FORALL(a:A,n:nat) : tail(singleton_seq(a),n) = IF n = 0 THEN singleton_seq(a) ELSE empty_seq ENDIF tail_const_seq : LEMMA FORALL(a:A,n:nat) : tail(const_seq(a),n) = const_seq(a) at_eqn_rel : PRED[[Seq[A],Seq[A]]] = {z: [Seq[A], Seq[A]] | FORALL (n: nat): at(PROJ_1(z), n) = at(PROJ_2(z), n)} at_eqn_rel_bisim : LEMMA bisimulation?(next[A],next[A])(at_eqn_rel) at_eqn : LEMMA FORALL(x,y:Seq[A]) : (FORALL(n:nat) : at(x,n) = at(y,n)) IMPLIES x = y list_incl_struct : [list[A] -> Lift[[A,list[A]]]] = LAMBDA(l:list[A]) : CASES l OF null : bot[[A,list[A]]], cons(a,l1) : up(a,l1) ENDCASES list_incl : [list[A] -> Seq[A]] = coreduce(list_incl_struct) list_incl_null : LEMMA list_incl(null) = empty_seq list_incl_cons : LEMMA FORALL(a:A, l:list[A]) : list_incl(cons(a,l)) = cons_seq(a,list_incl(l)) list_incl_list : LEMMA FORALL(l:list[A]) : list_incl(l) = cons_list(l,empty_seq) at_list_incl_up : LEMMA FORALL(l:list[A],n:nat) : n < length(l) IMPLIES up?(at(list_incl(l),n)) at_cons_list : LEMMA FORALL(x:Seq[A],l:list[A],n:nat) : at(cons_list(l,x),n) = IF n < length(l) THEN at(list_incl(l),n) ELSE at(x, n - length(l)) ENDIF cons_list_append : LEMMA FORALL(x:Seq[A],l,k:list[A]) : cons_list(l,cons_list(k,x)) = cons_list(append(l,k),x) finite? : PRED[Seq[A]] = LAMBDA(x:Seq[A]) : EXISTS(l:list[A]) : list_incl(l) = x finite_cons : LEMMA FORALL(x:Seq[A]) : finite?(x) IMPLIES FORALL(a:A) : finite?(cons_seq(a,x)) finite_list : LEMMA FORALL(x:Seq[A]) : finite?(x) IMPLIES FORALL(l:list[A]) : finite?(cons_list(l,x)) inf_incl_struct : [[nat->A] -> Lift[[A,[nat->A]]]] = LAMBDA(f : [nat->A]) : up(f(0), LAMBDA(n:nat) : f(n+1)) inf_incl : [[nat->A] -> Seq[A]] = coreduce(inf_incl_struct) infinite? : PRED[Seq[A]] = LAMBDA(x:Seq[A]) : EXISTS(f:[nat->A]) : inf_incl(f) = x infinite_cons : LEMMA FORALL(x:Seq[A]) : infinite?(x) IMPLIES FORALL(a:A) : infinite?(cons_seq(a,x)) infinite_list : LEMMA FORALL(x:Seq[A]) : infinite?(x) IMPLIES FORALL(l:list[A]) : infinite?(cons_list(l,x)) at_inf_incl : LEMMA FORALL(f:[nat->A],n:nat) : at(inf_incl(f),n) = up(f(n)) inf_incl_mono : LEMMA FORALL(f,g:[nat->A]) : inf_incl(f) = inf_incl(g) IMPLIES f = g finite?_length_at : LEMMA FORALL(l:list[A]) : bot?(at(list_incl(l),length(l))) at_up_to(x:Seq[A], n:nat) : RECURSIVE list[A] = IF bot?(next(x)) THEN null ELSE IF n=0 THEN null ELSE cons(proj_1(down(next(x))), at_up_to(proj_2(down(next(x))),n-1)) ENDIF ENDIF MEASURE (LAMBDA(x:Seq[A],n:nat) : n) at_up_to_empty : LEMMA FORALL(n:nat) : at_up_to(empty_seq,n) = null at_up_to_cons : LEMMA FORALL(x:Seq[A],a:A,n:nat) : at_up_to(cons_seq(a,x),n) = IF n=0 THEN null ELSE cons(a,at_up_to(x,n-1)) ENDIF at_up_to_list : LEMMA FORALL(x:Seq[A],l:list[A]) : at_up_to(cons_list(l,x),length(l)) = l length_at_up_to : LEMMA FORALL(x:Seq[A],n:nat) : (n /= 0 IMPLIES NOT bot?(at(x,n-1))) IMPLIES length(at_up_to(x,n)) = n at_up_to_at : LEMMA FORALL(x:Seq[A],n,m:nat) : at(list_incl(at_up_to(x,n)),m) = IF m < n THEN at(x,m) ELSE bot ENDIF at_up_to_eqn : LEMMA FORALL(x,y:Seq[A]) : (FORALL(n:nat) : at_up_to(x,n) = at_up_to(y,n)) IMPLIES x = y at_up_to_at_up_to : LEMMA FORALL(x:Seq[A],n,m:nat) : at_up_to(list_incl(at_up_to(x,n)),m) = at_up_to(x,min(n,m)) cons_list_at_up_to : LEMMA FORALL(x:Seq[A],n:nat) : cons_list(at_up_to(x,n),tail(x,n)) = x sublist : [[Seq[A],nat,nat] -> list[A]] = LAMBDA(x:Seq[A],n:nat,m:nat) : at_up_to(tail(x,n),m) sublist_nonnull : LEMMA FORALL(x:Seq[A],n:nat,m:nat) : (m > 0 AND up?(at(x,n))) IMPLIES NOT sublist(x,n,m) = null at_sublist : LEMMA FORALL(x:Seq[A],n,m,k:nat) : at(list_incl(sublist(x,n,m)),k) = IF k < m THEN at(x,n+k) ELSE bot ENDIF tail_sublist : LEMMA FORALL(x:Seq[A],n,m,k:nat) : tail(list_incl(sublist(x,n,m)),k) = IF k < m THEN list_incl(sublist(x,n+k,m-k)) ELSE empty_seq ENDIF at_up_to_sublist : LEMMA FORALL(x:Seq[A],n,m:nat) : append(at_up_to(x,n),sublist(x,n,m)) = at_up_to(x,n+m) cons_list_at_up_to_sublist_tail : LEMMA FORALL(x:Seq[A],n,m:nat) : cons_list(at_up_to(x,n),cons_list(sublist(x,n,m),tail(x,n+m))) = x list_incl_mono : LEMMA FORALL(l,k:list[A]) : list_incl(l) = list_incl(k) IMPLIES l = k at_list : LEMMA FORALL(x:Seq[A],n:nat) : bot?(at(x,n)) IMPLIES EXISTS(l:list[A]) : list_incl(l) = x finite?_at : LEMMA FORALL(x:Seq[A]) : finite?(x) IFF EXISTS(n:nat) : bot?(at(x,n)) infinite?_at : LEMMA FORALL(x:Seq[A]) : infinite?(x) IFF FORALL(n:nat) : NOT bot?(at(x,n)) finite_tail : LEMMA FORALL(x:Seq[A]) : finite?(x) IMPLIES FORALL(n:nat) : finite?(tail(x,n)) infinite_tail : LEMMA FORALL(x:Seq[A]) : infinite?(x) IMPLIES FORALL(n:nat) : infinite?(tail(x,n)) fin_inf : LEMMA FORALL(x:Seq[A]) : finite?(x) XOR infinite?(x) END Seq_prop Final_invariant[A : TYPE] : THEORY BEGIN IMPORTING Seq_prop invariant? : PRED[PRED[Seq[A]]] = LAMBDA(P:PRED[Seq[A]]) : FORALL(x:Seq[A]) : P(x) IMPLIES P(tail(x)) gi : [PRED[Seq[A]] -> PRED[Seq[A]]] = LAMBDA(P:PRED[Seq[A]]) : {x:Seq[A] | FORALL(n:nat) : P(tail(x,n))} li : [PRED[Seq[A]] -> PRED[Seq[A]]] = LAMBDA(P:PRED[Seq[A]]) : {x:Seq[A] | EXISTS(y:Seq[A],n:nat) : P(y) AND x = tail(y,n)} gi_invariant : LEMMA FORALL(P:PRED[Seq[A]]) : invariant?(gi(P)) li_invariant : LEMMA FORALL(P:PRED[Seq[A]]) : invariant?(li(P)) gi_invariant_char : LEMMA FORALL(P:PRED[Seq[A]]) : invariant?(P) IFF (FORALL(x:Seq[A]) : P(x) IMPLIES gi(P)(x)) li_invariant_char : LEMMA FORALL(P:PRED[Seq[A]]) : invariant?(P) IFF (FORALL(x:Seq[A]) : li(P)(x) IMPLIES P(x)) gi_monotone : LEMMA FORALL(P,Q:PRED[Seq[A]]) : (FORALL(x:Seq[A]) : P(x) IMPLIES Q(x)) IMPLIES (FORALL(x:Seq[A]) : gi(P)(x) IMPLIES gi(Q)(x)) li_monotone : LEMMA FORALL(P,Q:PRED[Seq[A]]) : (FORALL(x:Seq[A]) : P(x) IMPLIES Q(x)) IMPLIES (FORALL(x:Seq[A]) : li(P)(x) IMPLIES li(Q)(x)) gi_greatest : LEMMA FORALL(P,Q:PRED[Seq[A]]) : invariant?(Q) AND (FORALL(x:Seq[A]) : Q(x) IMPLIES P(x)) IMPLIES (FORALL(x:Seq[A]) : Q(x) IMPLIES gi(P)(x)) li_least : LEMMA FORALL(P,Q:PRED[Seq[A]]) : invariant?(Q) AND (FORALL(x:Seq[A]) : P(x) IMPLIES Q(x)) IMPLIES (FORALL(x:Seq[A]) : li(P)(x) IMPLIES Q(x)) END Final_invariant Invariant[A,X : TYPE] : THEORY BEGIN IMPORTING Final_invariant struct : VAR [X -> Lift[[A,X]]] invariant?(struct) : PRED[PRED[X]] = LAMBDA(P:PRED[X]) : FORALL(x:X) : P(x) AND up?(struct(x)) IMPLIES P(proj_2(down(struct(x)))) invariant_struct(struct)(P:(invariant?(struct))) : [(P) -> Lift[[A,(P)]]] = LAMBDA(x:(P)) : IF bot?(struct(x)) THEN bot[[A,(P)]] ELSE up[[A,(P)]](proj_1(down(struct(x))),proj_2(down(struct(x)))) ENDIF invariant_struct_map : LEMMA FORALL(P:PRED[X]) : invariant?(struct)(P) IMPLIES struct_map?(invariant_struct(struct)(P))(LAMBDA(x:(P)) : coreduce(struct)(x)) struct_gi_greatest : LEMMA FORALL(P:PRED[X],Q:PRED[Seq[A]]) : (invariant?(struct)(P) AND FORALL(x:X) : P(x) IMPLIES Q(coreduce(struct)(x))) IMPLIES (FORALL(x:X) : P(x) IMPLIES gi(Q)(coreduce(struct)(x))) END Invariant Seq_comp[A:TYPE]: THEORY BEGIN IMPORTING Seq_prop comp_struct : [[Seq[A],Seq[A]] -> Lift[[A,[Seq[A],Seq[A]]]]] = LAMBDA(x,y:Seq[A]) : IF bot?(next(x)) THEN IF bot?(next(y)) THEN bot[[A,[Seq[A],Seq[A]]]] ELSE up[[A,[Seq[A],Seq[A]]]](proj_1(down[[A,Seq[A]]](next(y))), (empty_seq, proj_2(down[[A,Seq[A]]](next(y))))) ENDIF ELSE up[[A,[Seq[A],Seq[A]]]](proj_1(down[[A,Seq[A]]](next(x))), (proj_2(down[[A,Seq[A]]](next(x))), y)) ENDIF comp : [[Seq[A],Seq[A]] -> Seq[A]] = coreduce(comp_struct) comp_empty1 : LEMMA FORALL(x:Seq[A]) : comp(empty_seq,x) = x comp_empty2 : LEMMA FORALL(x:Seq[A]) : comp(x,empty_seq) = x comp_assoc : LEMMA FORALL(x,y,z:Seq[A]) : comp(x,comp(y,z)) = comp(comp(x,y),z) comp_cons : LEMMA FORALL(a:A,x,y:Seq[A]) : comp(cons_seq(a,x),y) = cons_seq(a,comp(x,y)) comp_cons_list : LEMMA FORALL(x,y:Seq[A],l:list[A]) : comp(cons_list(l,x),y) = cons_list(l,comp(x,y)) comp_list : LEMMA FORALL(l:list[A],x:Seq[A]) : comp(list_incl(l),x) = cons_list(l,x) comp_append : LEMMA FORALL(l,k:list[A]) : list_incl(append(l,k)) = comp(list_incl(l),list_incl(k)) infinite_comp1 : LEMMA FORALL(x,y:Seq[A]) : infinite?(x) IMPLIES comp(x,y) = x infinite_comp2 : LEMMA FORALL(x,y:Seq[A]) : infinite?(y) IMPLIES infinite?(comp(x,y)) finite_comp : LEMMA FORALL(x,y:Seq[A]) : finite?(comp(x,y)) IMPLIES (finite?(x) AND finite?(y)) comp_at_tail : LEMMA FORALL(x:Seq[A],n:nat) : comp(list_incl(at_up_to(x,n)),tail(x,n)) = x END Seq_comp PrefixOrd[A : TYPE] : THEORY BEGIN IMPORTING Seq_comp prefix : PRED[[Seq[A],Seq[A]]] = LAMBDA(x,y:Seq[A]) : EXISTS(z:Seq[A]) : comp(x,z) = y prefix_refl : LEMMA reflexive?(prefix) prefix_trans : LEMMA transitive?(prefix) prefix_antisym : LEMMA antisymmetric?(prefix) prefix_poset : LEMMA partial_order?(prefix) prefix_empty : LEMMA FORALL(x:Seq[A]) : prefix(empty_seq,x) prefix_at_up_to : LEMMA FORALL(x:Seq[A],n:nat) : prefix(list_incl(at_up_to(x,n)),x) prefix_infinite : LEMMA FORALL(x,y:Seq[A]) : (infinite?(x) AND prefix(x,y)) IMPLIES x = y prefix_finite : LEMMA FORALL(x,y:Seq[A]) : (finite?(y) AND prefix(x,y)) IMPLIES finite?(x) prefix_tail : LEMMA FORALL(x,y:Seq[A]) : prefix(x,y) IMPLIES FORALL(n:nat) : prefix(tail(x,n),tail(y,n)) simulation? : PRED[PRED[[Seq[A],Seq[A]]]] = LAMBDA(R:PRED[[Seq[A],Seq[A]]]) : FORALL(x,y:Seq[A]) : R(x,y) IMPLIES (up?(next(x)) IMPLIES (up?(next(y)) AND proj_1(down(next(x))) = proj_1(down(next(y))) AND R(proj_2(down(next(x))),proj_2(down(next(y)))))) prefix_simulation : LEMMA FORALL(x,y:Seq[A]) : prefix(x,y) IFF EXISTS(R:PRED[[Seq[A],Seq[A]]]) : simulation?(R) AND R(x,y) prefix_at : LEMMA FORALL(x,y:Seq[A]) : prefix(x,y) IFF (FORALL(n:nat) : up?(at(x,n)) IMPLIES (up?(at(y,n)) AND down(at(x,n)) = down(at(y,n)))) consistent_prefix : LEMMA FORALL(x,y,z:Seq[A]) : (prefix(x,z) AND prefix(y,z)) IMPLIES (prefix(x,y) OR prefix(y,x)) END PrefixOrd Ascending_chains[X : TYPE, <= : PRED[[X,X]]] : THEORY BEGIN ASSUMING poset : ASSUMPTION partial_order?(<=) ENDASSUMING AChains? : PRED[[nat->X]] = LAMBDA(f:[nat->X]) : FORALL(n:nat) : f(n) <= f(n+1) achains_asc : LEMMA FORALL(f:(AChains?),n,m:nat) : n <= m IMPLIES f(n) <= f(m) upperbound? : [(AChains?) -> PRED[X]] = LAMBDA(f:(AChains?)) : LAMBDA(x:X) : FORALL(n:nat) : f(n) <= x least_upperbound? : [(AChains?) -> PRED[X]] = LAMBDA(f:(AChains?)) : LAMBDA(x:X) : upperbound?(f)(x) AND FORALL(y:X) : upperbound?(f)(y) IMPLIES x <= y least_upperbound_unique : LEMMA FORALL(f:(AChains?),x,y:X) : (least_upperbound?(f)(x) AND least_upperbound?(f)(y)) IMPLIES x=y bounded? : PRED[(AChains?)] = LAMBDA(f:(AChains?)) : EXISTS(x:X) : upperbound?(f)(x) END Ascending_chains Seq_alg_cpo[A : TYPE] : THEORY BEGIN IMPORTING PrefixOrd, Ascending_chains achain_tail : LEMMA FORALL(f:(AChains?[Seq[A],prefix[A]]),n:nat) : AChains?[Seq[A],prefix[A]](LAMBDA(m:nat) : tail(f(m),n)) seq_achains_asc : LEMMA FORALL(f:(AChains?[Seq[A],prefix[A]]),n,m,k:nat) : (n <= m AND up?(at(f(n),k))) IMPLIES (up?(at(f(m),k)) AND down(at(f(n),k)) = down(at(f(m),k))) lub_struct : [(AChains?[Seq[A],prefix[A]]) -> Lift[[A,(AChains?[Seq[A],prefix[A]])]]] = LAMBDA(f:(AChains?[Seq[A],prefix[A]])) : IF FORALL(n:nat) : bot?(next(f(n))) THEN bot[[A,(AChains?[Seq[A],prefix[A]])]] ELSE up[[A,(AChains?[Seq[A],prefix[A]])]] (proj_1(down(next(f(least({n:nat|NOT bot?(next(f(n)))}))))), LAMBDA(n:nat) : tail(f(n),1)) ENDIF lub : [(AChains?[Seq[A],prefix[A]]) -> Seq[A]] = coreduce(lub_struct) tail_cont : LEMMA FORALL(f:(AChains?[Seq[A],prefix[A]]),m:nat) : tail(lub(f),m) = lub(LAMBDA(n:nat) : tail(f(n),m)) seq_lub : LEMMA FORALL(f:(AChains?[Seq[A],prefix[A]])) : least_upperbound?[Seq[A],prefix[A]](f)(lub(f)) at_lub : LEMMA FORALL(f:(AChains?[Seq[A],prefix[A]]),y:Seq[A]) : y = lub(f) IFF (FORALL(a:A,n:nat) : at(y,n) = up(a) IFF EXISTS(m:nat) : at(f(m),n) = up(a)) at_up_to_achain : LEMMA FORALL(x:Seq[A]) : AChains?[Seq[A], prefix[A]]( LAMBDA (n: nat): list_incl[A](at_up_to[A](x, n))) lub_at_up_to : LEMMA FORALL(x:Seq[A]) : x = lub(LAMBDA(n:nat) : list_incl(at_up_to(x,n))) at_up_to_compact : LEMMA FORALL(x:Seq[A],n:nat,f:(AChains?[Seq[A],prefix[A]])) : (n /= 0 IMPLIES NOT bot?(at(x,n-1))) IMPLIES (prefix(list_incl(at_up_to(x,n)),lub(f)) IMPLIES EXISTS(m:nat) : prefix(list_incl(at_up_to(x,n)),f(m))) finite_compact : LEMMA FORALL(x:Seq[A]) : finite?(x) IFF FORALL(f:(AChains?[Seq[A],prefix[A]])) : prefix(x,lub(f)) IMPLIES EXISTS(m:nat) : prefix(x,f(m)) admissable? : PRED[PRED[Seq[A]]] = LAMBDA(p:PRED[Seq[A]]) : FORALL(f:(AChains?[Seq[A],prefix[A]])) : (FORALL(n:nat) : p(f(n))) IMPLIES p(lub(f)) admissable_holds : LEMMA FORALL(p:PRED[Seq[A]]) : (admissable?(p) AND FORALL(l:list[A]) : p(list_incl(l))) IMPLIES FORALL(x:Seq[A]) : p(x) END Seq_alg_cpo Seq_map_id[A : TYPE] : THEORY BEGIN IMPORTING Seq_prop, Seq_functoriality seq_map_id : LEMMA FORALL(x:Seq[A]) : seq_map(id[A])(x) = x END Seq_map_id Seq_map_comp[A,B,C : TYPE] : THEORY BEGIN IMPORTING Seq_prop, Seq_functoriality, Seq_comp seq_map_comp : LEMMA FORALL(f:[A->B],g:[B->C],x:Seq[A]) : seq_map(g o f)(x) = seq_map(g)(seq_map(f)(x)) END Seq_map_comp Seq_map_prop[A,B : TYPE] : THEORY BEGIN IMPORTING Seq_prop, Seq_functoriality, Seq_comp, Seq_map_id, Seq_map_comp seq_map_empty : LEMMA FORALL(f:[A->B]) : seq_map(f)(empty_seq) = empty_seq seq_map_cons : LEMMA FORALL(f:[A->B],a:A,x:Seq[A]) : seq_map(f)(cons_seq(a,x)) = cons_seq(f(a),seq_map(f)(x)) seq_map_cons_list : LEMMA FORALL(f:[A->B],l:list[A],x:Seq[A]) : seq_map(f)(cons_list(l,x)) = cons_list(map(f)(l),seq_map(f)(x)) seq_map_list : LEMMA FORALL(f:[A->B],l:list[A]) : seq_map(f)(list_incl(l)) = list_incl(map(f)(l)) comp_seq_map : LEMMA FORALL(f:[A->B], x,y:Seq[A]) : comp(seq_map(f)(x),seq_map(f)(y)) = seq_map(f)(comp(x,y)) at_seq_map : LEMMA FORALL(f:[A->B],x:Seq[A],n:nat) : (up?(at(x,n)) IFF up?(at(seq_map(f)(x),n))) AND (up?(at(x,n)) IMPLIES down(at(seq_map(f)(x),n)) = f(down(at(x,n)))) tail_seq_map : LEMMA FORALL(f:[A->B],x:Seq[A],n:nat) : tail(seq_map(f)(x),n) = seq_map(f)(tail(x,n)) seq_map_pres_inj : LEMMA FORALL(f:[A->B]) : injective?(f) IMPLIES injective?(seq_map(f)) seq_map_finite : LEMMA FORALL(x:Seq[A],f:[A->B]) : finite?(x) IFF finite?(seq_map(f)(x)) seq_map_infinite : LEMMA FORALL(x:Seq[A],f:[A->B]) : infinite?(x) IFF infinite?(seq_map(f)(x)) seq_map_singleton_seq : LEMMA FORALL(f:[A->B],a:A) : seq_map(f)(singleton_seq(a)) = singleton_seq(f(a)) seq_map_const_seq : LEMMA FORALL(f:[A->B],a:A) : seq_map(f)(const_seq(a)) = const_seq(f(a)) at_up_to_seq_map : LEMMA FORALL(f:[A->B],x:Seq[A],n:nat) : at_up_to(seq_map(f)(x),n) = map(f)(at_up_to(x,n)) sublist_seq_map : LEMMA FORALL(f:[A->B],x:Seq[A],n,m:nat) : sublist(seq_map(f)(x),n,m) = map(f)(sublist(x,n,m)) END Seq_map_prop Seq_filter[A : TYPE]: THEORY BEGIN IMPORTING Seq_comp, Seq_map_prop list_filter(p:PRED[A],l:list[A]) : RECURSIVE list[A] = CASES l OF null : null, cons(a,k) : IF p(a) THEN cons(a,list_filter(p,k)) ELSE list_filter(p,k) ENDIF ENDCASES MEASURE (LAMBDA(p:PRED[A],l:list[A]) : length(l)) holds_first_at : [[PRED[A],Seq[A]] -> Lift[nat]] = LAMBDA(p:PRED[A],x:Seq[A]) : IF (FORALL(n:nat) : up?(at(x,n)) IMPLIES NOT p(down(at(x,n)))) THEN bot[nat] ELSE up[nat](least({ n : nat | up?(at(x,n)) AND p(down(at(x,n)))})) ENDIF at_holds_first_at : LEMMA FORALL(p:PRED[A],x:Seq[A],n:nat) : holds_first_at(p,x) = up[nat](n) IMPLIES NOT bot?(at(x,n)) AND p(down(at(x,n))) AND FORALL(m:nat) : NOT bot?(at(x,m)) AND p(down(at(x,m))) IMPLIES n <= m holds_first_at_empty : LEMMA FORALL(p:PRED[A]) : holds_first_at(p, empty_seq) = bot[nat] holds_first_at_cons : LEMMA FORALL(p:PRED[A], x:Seq[A], a:A) : holds_first_at(p,cons_seq(a,x)) = IF p(a) THEN up[nat](0) ELSIF bot?(holds_first_at(p,x)) THEN bot[nat] ELSE up[nat](1 + down[nat](holds_first_at(p,x))) ENDIF filter_struct : [[PRED[A],Seq[A]] -> Lift[[A,[PRED[A],Seq[A]]]]] = LAMBDA(p:PRED[A], x:Seq[A]) : IF bot?(holds_first_at(p,x)) THEN bot[[A,[PRED[A],Seq[A]]]] ELSE up[[A,[PRED[A],Seq[A]]]](down[A](at(x, down[nat](holds_first_at(p,x)))), (p, tail(x, 1+down[nat](holds_first_at(p,x))))) ENDIF filter : [[PRED[A],Seq[A]] -> Seq[A]] = coreduce(filter_struct) head_filter : LEMMA FORALL(p:PRED[A],x:Seq[A],n:nat) : holds_first_at(p,x) = up[nat](n) IMPLIES (up?(at(filter(p,x),0)) AND at(filter(p,x),0) = at(x,n) AND tail(filter(p,x),1) = filter(p,tail(x,n+1))) holds_immediately : LEMMA FORALL(p:PRED[A],x:Seq[A]) : (up?(at(x,0)) AND p(down[A](at(x,0)))) IMPLIES (up?[A](at(filter(p,x),0)) AND at(filter(p,x),0) = at(x,0) AND tail(filter(p,x),1) = filter(p,tail(x,1))) filter_empty : LEMMA FORALL(p:PRED[A]) : filter(p,empty_seq) = empty_seq filter_cons : LEMMA FORALL(p:PRED[A], x:Seq[A], a:A) : filter(p,cons_seq(a,x)) = IF p(a) THEN cons_seq(a,filter(p,x)) ELSE filter(p,x) ENDIF list_filter_incl : LEMMA FORALL(l:list[A],p:PRED[A]) : list_incl(list_filter(p,l)) = filter(p,list_incl(l)) filter_singleton_seq : LEMMA FORALL(a:A,p:PRED[A]) : filter(p,singleton_seq(a)) = IF p(a) THEN singleton_seq(a) ELSE empty_seq ENDIF filter_const_seq : LEMMA FORALL(a:A,p:PRED[A]) : filter(p,const_seq(a)) = IF p(a) THEN const_seq(a) ELSE empty_seq ENDIF finite_filter : LEMMA FORALL(x:Seq[A],p:PRED[A]) : finite?(x) IMPLIES finite?(filter(p,x)) filter_comp : LEMMA FORALL(l:list[A],x:Seq[A],p:PRED[A]) : filter(p,comp(list_incl(l),x)) = comp(filter(p,list_incl(l)),filter(p,x)) filter_idempotent : LEMMA FORALL(x:Seq[A],p:PRED[A]) : filter(p,filter(p,x)) = filter(p,x) at_filter : LEMMA FORALL(p:PRED[A],x:Seq[A],n:nat,a:A) : at(filter(p,x),n) = up[A](a) IMPLIES p(a) AND EXISTS(m:nat) : m >= n AND at(x,m) = up[A](a) at_holds : LEMMA FORALL(p:PRED[A],x:Seq[A],n:nat,a:A) : (at(x,n) = up[A](a) AND p(a)) IMPLIES EXISTS(m:nat) : m <= n AND at(filter(p,x),m) = up[A](a) filter_from_tail : LEMMA FORALL(p:PRED[A],x:Seq[A],n:nat) : holds_first_at(p,x) = up[nat](n) IMPLIES filter(p,x) = filter(p,tail(x,n)) filter_and_tail : LEMMA FORALL(p,q:PRED[A],x:Seq[A],n:nat) : holds_first_at((LAMBDA(a:A) : p(a) AND q(a)),x) = up[nat](n) IMPLIES filter(p,filter(q,x)) = filter(p,filter(q,tail(x,n))) filter_and : LEMMA FORALL(x:Seq[A],p,q:PRED[A]) : filter(p,filter(q,x)) = filter((LAMBDA(a:A) : p(a) AND q(a)),x) filter_pred_struct(p:PRED[A]) : [Seq[A] -> Lift[[(p),Seq[A]]]] = LAMBDA(x:Seq[A]) : IF bot?(holds_first_at(p,x)) THEN bot[[(p),Seq[A]]] ELSE up[[(p),Seq[A]]](down[A](at(x,down[nat](holds_first_at(p,x)))), tail(x,1+down[nat](holds_first_at(p,x)))) ENDIF filter_pred(p:PRED[A]) : [Seq[A] -> Seq[(p)]] = coreduce(filter_pred_struct(p)) pred_incl(p:PRED[A]) : [(p) -> A] = LAMBDA(x:(p)) : x seq_pred_incl(p:PRED[A]) : [Seq[(p)] -> Seq[A]] = seq_map(pred_incl(p)) seq_pred_incl_inj : LEMMA FORALL(p:PRED[A]) : injective?(seq_pred_incl(p)) at_filter_pred : LEMMA FORALL(p:PRED[A],x:Seq[A],n:nat) : (bot?(at(filter(p,x),n)) IMPLIES bot?(at(filter_pred(p)(x),n))) AND (up?(at(filter(p,x),n)) IMPLIES (up?(at(filter_pred(p)(x),n)) AND down[A](at(filter(p,x),n)) = down[A](at(filter_pred(p)(x),n)))) filter_pred_filter : LEMMA FORALL(p:PRED[A],x:Seq[A]) : seq_pred_incl(p)(filter_pred(p)(x)) = filter(p,x) END Seq_filter Seq_filter_map[A,B :TYPE] : THEORY BEGIN IMPORTING Seq_filter, Seq_map_prop holds_first_at_map: LEMMA FORALL (f: [A -> B], p: PRED[B], x: Seq[A], n: nat): holds_first_at((p o f), x) = up(n) IFF holds_first_at( p, seq_map(f)(x)) = up(n) filter_map_bot : LEMMA FORALL (f: [A -> B], p: PRED[B], x: Seq[A]): bot?(next(x)) IMPLIES bot?(next(seq_map(f)(filter((p o f),x)))) AND bot?(next(filter(p,seq_map(f)(x)))) filter_map_up1 : LEMMA FORALL (f: [A -> B], p: PRED[B], x: Seq[A]): NOT (bot?(next(seq_map(f)(filter((p o f),x))))) IMPLIES EXISTS (n: nat): holds_first_at((p o f), x) = up(n) filter_map_up2 : LEMMA FORALL (f: [A -> B], p: PRED[B], x: Seq[A]): NOT (bot?(next(filter(p,seq_map(f)(x))))) IMPLIES EXISTS (n: nat): holds_first_at(p, seq_map(f)(x)) = up(n) filter_map_next1 : LEMMA FORALL (f: [A -> B], p: PRED[B], x: Seq[A], n: nat): holds_first_at((p o f), x) = up(n) IMPLIES proj_2(down(next(seq_map(f)(filter((p o f),x))))) = seq_map(f)(filter((p o f),tail(x, n+1))) filter_map_next2 : LEMMA FORALL (f: [A -> B], p: PRED[B], x: Seq[A], n: nat): holds_first_at(p, seq_map(f)(x)) = up(n) IMPLIES proj_2(down(next(filter(p,seq_map(f)(x))))) = filter(p, seq_map(f)(tail(x, n+1))) filter_map : LEMMA FORALL (f: [A -> B], p: PRED[B], x: Seq[A]): filter(p,seq_map(f)(x)) = seq_map(f)(filter((p o f),x)) filter_pred_map : LEMMA FORALL (f: [A -> B], p: PRED[B], q: PRED[A], x: Seq[A], g:[(q)->(p)]): q = p o f AND f o pred_incl(q) = pred_incl(p) o g IMPLIES filter_pred(p)(seq_map(f)(x)) = seq_map(g)(filter_pred(q)(x)) END Seq_filter_map Flattening[A: TYPE] : THEORY BEGIN IMPORTING Seq_filter, Seq_map_prop list_flatten : [list[list[A]] -> list[A]] = reduce(null,append) flatten_struct : [Seq[list[A]] -> Lift[[A,Seq[list[A]]]]] = LAMBDA(x:Seq[list[A]]) : LET y = holds_first_at((LAMBDA(l:list[A]) : NOT l=null),x) IN IF bot?(y) THEN bot[[A,Seq[list[A]]]] ELSE up[[A,Seq[list[A]]]](car(down[list[A]](at(x, down[nat](y)))), cons_seq(cdr(down[list[A]](at(x, down[nat](y)))), tail(x, 1 + down[nat](y)))) ENDIF flatten : [Seq[list[A]] -> Seq[A]] = coreduce(flatten_struct) head_flatten : LEMMA FORALL(x:Seq[list[A]],n:nat) : holds_first_at((LAMBDA(l:list[A]) : NOT l=null),x) = up(n) IMPLIES (at(flatten(x),0) = up(car(down(at(x,n)))) AND tail(flatten(x),1) = flatten(cons_seq(cdr(down(at(x,n))),tail(x,n+1)))) flatten_immediately : LEMMA FORALL(x:Seq[list[A]]) : (up?(at(x,0)) AND NOT down(at(x,0)) = null) IMPLIES (at(flatten(x),0) = up(car(down(at(x,0)))) AND tail(flatten(x),1) = flatten(cons_seq(cdr(down(at(x,0))),tail(x,1)))) flatten_from_tail : LEMMA FORALL(x:Seq[list[A]],n:nat) : holds_first_at((LAMBDA(l:list[A]) : NOT l=null),x) = up(n) IMPLIES flatten(x) = flatten(tail(x,n)) flatten_empty : LEMMA flatten(empty_seq) = empty_seq flatten_null : LEMMA FORALL(x:Seq[list[A]]) : flatten(cons_seq(null,x)) = flatten(x) flatten_cons : LEMMA FORALL(x:Seq[list[A]],a:A,l:list[A]) : flatten(cons_seq(cons(a,l),x)) = cons_seq(a,flatten(cons_seq(l,x))) flatten_list : LEMMA FORALL(x:Seq[list[A]],l:list[A]) : flatten(cons_seq(l,x)) = cons_list(l,flatten(x)) flatten_comp : LEMMA FORALL(x:Seq[list[A]],l:list[list[A]]) : flatten(comp(list_incl(l),x)) = comp(list_incl(list_flatten(l)),flatten(x)) flatten_list_incl : LEMMA FORALL(x:list[list[A]]) : flatten(list_incl(x)) = list_incl(list_flatten(x)) flatten_singleton_seq : LEMMA FORALL(l:list[A]) : flatten(singleton_seq(l)) = list_incl(l) flatten_filter_null : LEMMA FORALL(x:Seq[list[A]]) : flatten(x) = flatten(filter((LAMBDA(l:list[A]) : NOT l=null),x)) at_flatten_nonnull : LEMMA FORALL(x:Seq[list[A]]) : (FORALL(n:nat) : up?(at(x,n)) IMPLIES NOT down(at(x,n)) = null) IMPLIES FORALL(a:A,n:nat) : at(flatten(x),n) = up(a) IMPLIES EXISTS(m,k:nat) : up?(at(x,m)) AND at(list_incl(down(at(x,m))),k) = up(a) at_flatten : LEMMA FORALL(x:Seq[list[A]],a:A,n:nat) : at(flatten(x),n) = up(a) IMPLIES EXISTS(m,k:nat) : up?(at(x,m)) AND at(list_incl(down(at(x,m))),k) = up(a) at_list_occurs : LEMMA FORALL(x:Seq[list[A]],n:nat) : up?(at(x,n)) IMPLIES EXISTS(m:nat) : down(at(x,n)) = at_up_to(tail(flatten(x),m),length(down(at(x,n)))) filter_flatten_tail : LEMMA FORALL(x:Seq[list[A]],p:PRED[A],n:nat) : holds_first_at((LAMBDA(l:list[A]) : NOT l=null), seq_map(LAMBDA(l:list[A]) : list_filter(p,l))(x)) = up(n) IMPLIES filter(p,flatten(x)) = filter(p,flatten(tail(x,n))) filter_flatten : LEMMA FORALL(x:Seq[list[A]],p:PRED[A]) : filter(p,flatten(x)) = flatten(seq_map(LAMBDA(l:list[A]) : list_filter(p,l))(x)) SAChain : PRED[[nat->nat]] = LAMBDA(g:[nat->nat]) : g(0) = 0 AND FORALL(n:nat) : g(n+1) > g(n) sum_sachain : LEMMA FORALL(g:(SAChain),n:nat) : SAChain(LAMBDA(x:nat) : g(x+n) - g(n)) chop : [[Seq[A],(SAChain)] -> Seq[list[A]]] = LAMBDA(y:Seq[A],g:(SAChain)) : inf_incl(LAMBDA(n:nat) : sublist(y,g(n),g(n+1)-g(n))) next_chop : LEMMA FORALL(y:Seq[A],g:(SAChain)) : next(chop(y,g)) = up(at_up_to(y,g(1)), chop(tail(y,g(1)),LAMBDA(x:nat) : g(x+1) - g(1))) cum_sum(g:(SAChain),n:nat) : RECURSIVE nat = IF n = 0 THEN 0 ELSE g(1) + cum_sum(LAMBDA(x:nat) : g(x+1) - g(1),n-1) ENDIF MEASURE (LAMBDA(g:(SAChain),n:nat) : n) cum_sum_growth : LEMMA FORALL(g:(SAChain),n:nat) : n < cum_sum(g,n+1) flatten_chop_list : LEMMA FORALL(y:Seq[A],g:(SAChain),n:nat) : flatten(chop(y,g)) = cons_list(at_up_to(y,cum_sum(g,n)), flatten(chop(tail(y,cum_sum(g,n)),LAMBDA(x:nat) : g(x+n) - g(n)))) flatten_chop : LEMMA FORALL(y:Seq[A],g:(SAChain)) : flatten(chop(y,g)) = y END Flattening Flatten_naturality[A,B : TYPE] : THEORY BEGIN IMPORTING Flattening, Seq_map_prop flatten_nat : LEMMA FORALL(f:[A->B],x:Seq[list[A]]) : flatten(seq_map(map(f))(x)) = seq_map(f)(flatten(x)) END Flatten_naturality Seq_strength[A,B: TYPE]: THEORY BEGIN IMPORTING Seq_prop strength_struct: [[Seq[A],B] -> Lift[[[A,B],[Seq[A],B]]]]= LAMBDA (x:Seq[A],b:B): IF bot?(next(x)) THEN bot ELSE up(((proj_1(down(next(x))),b),(proj_2(down(next(x))),b))) ENDIF; seq_strength: [[Seq[A],B] -> Seq[[A,B]]] = coreduce(strength_struct); strength_empty: LEMMA FORALL (b:B) : seq_strength(empty_seq,b) = empty_seq ; strength_cons: LEMMA FORALL (x: Seq[A], a:A, b:B): seq_strength(cons_seq(a, x),b)= cons_seq((a,b),seq_strength(x,b)); END Seq_strength Seq_strength_nat[A,B,C,D: TYPE]: THEORY BEGIN IMPORTING Seq_strength, Seq_map_prop seq_strength_nat: LEMMA FORALL (f:[A->C], g:[B -> D]): seq_map((LAMBDA (x:[A,B]): (f(proj_1(x)),g(proj_2(x))))) o seq_strength[A,B] = seq_strength[C,D] o (LAMBDA (x:[Seq[A],B]): (seq_map(f)(proj_1(x)),g(proj_2(x)))) END Seq_strength_nat Seq_coherence[A,B,C : TYPE] : THEORY BEGIN IMPORTING Seq_strength, Seq_strength_nat seq_strength_assoc: LEMMA FORALL (l:Seq[A],b:B, c:C): seq_strength[A,[B,C]](l,(b,c)) = seq_map(LAMBDA (x: [A,B], c:C): (proj_1(x),(proj_2(x),c))) (seq_strength(seq_strength(l,b),c)); seq_strength_proj: LEMMA FORALL (l: Seq[A], b:B): seq_map((LAMBDA (x: [A,B]) : proj_1(x)))(seq_strength(l,b)) = l; END Seq_coherence final_obj: DATATYPE BEGIN star : star? END final_obj Seq_shape[A:TYPE] : THEORY BEGIN IMPORTING Seq_strength, Seq_map_prop, final_obj shape: [Seq[A] -> Seq[final_obj]] = seq_map[A,final_obj](LAMBDA (a: A) : star); shape_empty: LEMMA shape(empty_seq[A]) = empty_seq[final_obj] shape_cons : LEMMA FORALL (a:A, l:Seq[A]): shape(cons_seq(a, l)) = cons_seq(star, shape(l)) END Seq_shape Seq_zip[A,B: TYPE] : THEORY BEGIN IMPORTING Seq_strength, Seq_map_prop, Seq_shape equal_shape: PRED[[Seq[A],Seq[B]]] = {l:Seq[A], k:Seq[B] | shape(l) = shape(k)} next_equal_bot : LEMMA FORALL (x: (equal_shape)): bot?(next(proj_1(x))) IFF bot?(next(proj_2(x))) next_equal_shape : LEMMA FORALL (x: (equal_shape)): (bot?(next(proj_1(x))) AND bot?(next(proj_2(x)))) OR equal_shape(proj_2(down(next(proj_1(x)))), proj_2(down(next(proj_2(x))))); zip_struct: [(equal_shape) -> Lift[[[A, B], (equal_shape)]]] = LAMBDA (x: (equal_shape)): LET l = PROJ_1(x), k = PROJ_2(x) IN IF bot?(next(l)) THEN bot ELSE up[[[A,B],(equal_shape)]] ((PROJ_1(down(next(l))), PROJ_1(down(next(k)))), (PROJ_2(down(next(l))), PROJ_2(down(next(k))))) ENDIF; zip: [(equal_shape) -> Seq[[A,B]]] = coreduce(zip_struct); zip_empty_left: LEMMA FORALL (x: (equal_shape)): bot?(next(proj_1(x))) IMPLIES bot?(next(zip(x))) zip_empty_right: LEMMA FORALL (x: (equal_shape)): bot?(next(proj_2(x))) IMPLIES bot?(next(zip(x))) zip_cons_left: LEMMA FORALL (x: (equal_shape)): NOT bot?(next(proj_1(x))) IMPLIES zip(x) = cons_seq((proj_1(down(next(proj_1(x)))), proj_1(down(next(proj_2(x))))), zip(proj_2(down(next(proj_1(x)))), proj_2(down(next(proj_2(x)))))); zip_cons_right: LEMMA FORALL (x: (equal_shape)): NOT bot?(next(proj_2(x))) IMPLIES zip(x) = cons_seq((proj_1(down(next(proj_1(x)))), proj_1(down(next(proj_2(x))))), zip(proj_2(down(next(proj_1(x)))), proj_2(down(next(proj_2(x)))))); zip_cons : LEMMA FORALL (l: Seq[A], k: Seq[B], a: A, b: B): equal_shape(l,k) IMPLIES zip(cons_seq(a,l), cons_seq(b,k)) = cons_seq((a,b),zip(l,k)); zip_inv: [Seq[[A,B]] -> (equal_shape)] = LAMBDA (l:Seq[[A,B]]) : (seq_map((LAMBDA (x:[A,B]):proj_1(x)))(l), seq_map((LAMBDA(x:[A,B]):proj_2(x)))(l)); zip_inv_cons :LEMMA FORALL (x: [A,B], l: Seq[[A,B]]) : zip_inv(cons_seq(x,l)) = (cons_seq(proj_1(x), proj_1(zip_inv(l))), cons_seq(proj_2(x), proj_2(zip_inv(l)))); zip_iso_left: LEMMA FORALL (x: (equal_shape)): zip_inv(zip(x)) = x; zip_iso_right: LEMMA FORALL (l: Seq[[A,B]]): zip(zip_inv(l)) = l; zip_mono: LEMMA FORALL (x,y: (equal_shape)): zip(x) = zip(y) IMPLIES x=y END Seq_zip $$$ax_seq.prf (|Lift|)(|Lift_prop| (|cover| "" (SKOSIMP*) (("" (INST 2 "down(z!1)") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))) (|up_exist| "" (SKOSIMP*) (("" (PROP) (("1" (INST 1 "down(z!1)") (("1" (ASSERT) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))) ("2" (SKOSIMP*) (("2" (ASSERT) NIL))))))) (|mono_up| "" (SKOSIMP*) (("" (CASE "x1!1 = down(up(x1!1))") (("1" (CASE "x2!1 = down(up(x2!1))") (("1" (REPLACE -1 1 LR) (("1" (REPLACE -2 1 LR) (("1" (REPLACE -3 1 LR) (("1" (PROPAX) NIL))))))) ("2" (ASSERT) NIL))) ("2" (ASSERT) NIL))))))(|Seq_defn|)(|Seq_ax| (|coreduce_TCC1| "" (LEMMA "seq_finality") (("" (INST + "LAMBDA(struct: [X -> Lift[[A, X]]]): choose( {f: [X -> Seq[A]] | struct_map?(struct)(f) AND FORALL (g: [X -> Seq[A]]): struct_map?(struct)(g) IMPLIES g = f})") (("" (SKOSIMP*) (("" (INST?) (("" (SKOSIMP*) (("" (EXPAND "nonempty?") (("" (EXPAND "empty?") (("" (INST -1 "f!1") (("" (EXPAND "member") (("" (ASSERT) NIL))))))))))))))))))) (|coreduce_struct_map| "" (SKOSIMP*) (("" (TYPEPRED "coreduce(struct!1)") (("" (PROPAX) NIL))))) (|coreduce_unique| "" (SKOSIMP*) (("" (TYPEPRED "coreduce(struct!1)") (("" (GRIND) NIL))))) (|struct_map_unique| "" (SKOSIMP*) (("" (ASSERT) (("" (LEMMA "coreduce_unique") (("" (INST -1 "struct!1" "_") (("" (INST-CP -1 "g!1") (("" (ASSERT) (("" (INST -1 "h!1") (("" (ASSERT) NIL))))))))))))))) (|next_TCC1| "" (GRIND) NIL) (|next| "" (LEMMA "coreduce_struct_map") (("" (SKOSIMP*) (("" (INST?) (("" (EXPAND "struct_map?") (("" (INST?) (("" (GRIND) NIL))))))))))))(|SeqImpl| (|shift_TCC1| "" (SKOSIMP*) (("" (TYPEPRED "f!1") (("" (INST -1 "n!1+1") (("" (ASSERT) NIL))))))) (|next_impl_TCC1| "" (SUBTYPE-TCC) NIL))(|SeqImplFinality| (|iter_TCC1| "" (SUBTYPE-TCC) NIL) (|iter_TCC2| "" (TERMINATION-TCC) NIL) (|iter_TCC3| "" (SUBTYPE-TCC) NIL) (|iter_exchange| "" (INDUCT "n") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "iter" 1) (("2" (INST?) (("2" (GRIND) NIL))))))))) (|cored_TCC1| "" (SUBTYPE-TCC) NIL) (|cored_TCC2| "" (SKOSIMP*) (("" (LIFT-IF 1) (("" (PROP) (("1" (ASSERT) NIL) ("2" (HIDE 2) (("2" (LIFT-IF -1) (("2" (PROP) (("1" (HIDE -2) (("1" (EXPAND "iter" 1) (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))))) (|struct_map_bot| "" (SKOSIMP*) (("" (EXPAND "next_impl") (("" (LIFT-IF) (("" (PROP) (("1" (BETA) (("1" (PROPAX) NIL))) ("2" (HIDE 2) (("2" (EXPAND "cored") (("2" (EXPAND "iter") (("2" (ASSERT) NIL))))))))))))))) (|struct_map_up| "" (SKOSIMP*) (("" (EXPAND "next_impl") (("" (LIFT-IF) (("" (PROP) (("1" (HIDE 1) (("1" (EXPAND "cored") (("1" (EXPAND "iter") (("1" (ASSERT) NIL))))))) ("2" (EXPAND "cored" 2 1) (("2" (EXPAND "iter") (("2" (LIFT-IF) (("2" (PROP) (("1" (HIDE 1 2) (("1" (ASSERT) NIL))) ("2" (CASE "shift(cored(struct!1)(x!1)) = cored(struct!1)(PROJ_2(down(struct!1(x!1))))") (("1" (ASSERT) NIL) ("2" (HIDE 3) (("2" (EXPAND "shift") (("2" (EXPAND "cored") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (USE "iter_exchange") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (PROPAX) NIL))))))) ("2" (SKOSIMP*) (("2" (ASSERT) NIL))) ("3" (SKOSIMP*) (("3" (ASSERT) NIL))))))))))) ("3" (PROPAX) NIL))))))))))))))))))) (|struct_map_unique| "" (SKOSIMP*) (("" (CASE "FORALL(n:nat, x:X) : f!1(x)(n) = cored(struct!1)(x)(n)") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (INST?) NIL))))) ("2" (HIDE 2) (("2" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "cored") (("1" (EXPAND "iter") (("1" (LIFT-IF) (("1" (PROP) (("1" (INST?) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "next_impl") (("1" (PROPAX) NIL))))))))) ("2" (INST?) (("2" (FLATTEN) (("2" (ASSERT) (("2" (EXPAND "next_impl") (("2" (HIDE -1) (("2" (LIFT-IF) (("2" (PROP) (("1" (HIDE -1 1 2) (("1" (ASSERT) NIL))) ("2" (LEMMA "mono_up[[A, Seq_impl[A]]]") (("2" (INST?) (("1" (PROP) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("2" (ASSERT) NIL))))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "cored" 1) (("2" (EXPAND "iter" 1) (("2" (LIFT-IF) (("2" (PROP) (("1" (BETA) (("1" (ASSERT) (("1" (HIDE -3) (("1" (EXPAND "cored") (("1" (TYPEPRED "f!1(x!1)") (("1" (INST?) (("1" (PROP) (("1" (HIDE -2 -3) (("1" (LEMMA "Lift_bot_extensionality[A]") (("1" (CASE "bot?[A](f!1(x!1)(1 + j!1))") (("1" (ASSERT) NIL) ("2" (PROPAX) NIL))))))) ("2" (INST?) (("2" (LIFT-IF) (("2" (PROP) (("2" (REPLACE -2) (("2" (BETA) (("2" (PROPAX) NIL))))))))))))))))))))))))) ("2" (CASE "FORALL(m,k:nat, x:X) : up?(iter(struct!1,m)(x)) IMPLIES f!1(proj_2(down(iter(struct!1,m)(x))))(k) = f!1(x)(m+k+1)") (("1" (LIFT-IF 2) (("1" (PROP) (("1" (INST -4 "PROJ_2(down[[A, X]](iter(struct!1, j!1)(x!1)))") (("1" (FLATTEN) (("1" (HIDE -5) (("1" (ASSERT) (("1" (EXPAND "next_impl") (("1" (LIFT-IF -4) (("1" (PROP) (("1" (INST -4 "j!1" "0" "x!1") (("1" (PROP) (("1" (REPLACE -1) (("1" (HIDE -1 -3 -4 -5 2) (("1" (CASE "bot?[A](f!1(x!1)(1 + 0 + j!1))") (("1" (ASSERT) NIL) ("2" (PROPAX) NIL))))))) ("2" (ASSERT) NIL))))) ("2" (HIDE -2 -3 -4 1 2 3) (("2" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) NIL))) ("2" (INST -3 "PROJ_2(down[[A, X]](iter(struct!1, j!1)(x!1)))") (("1" (FLATTEN) (("1" (HIDE -3) (("1" (ASSERT) (("1" (EXPAND "next_impl") (("1" (LIFT-IF) (("1" (PROP) (("1" (HIDE -1 -3 -4 1 2 3) (("1" (ASSERT) NIL))) ("2" (LEMMA "mono_up[[A, Seq_impl[A]]]") (("2" (INST?) (("1" (PROP) (("1" (HIDE -2) (("1" (CASE "down[A](f!1(PROJ_2(down[[A, X]](iter(struct!1, j!1)(x!1))))(0)) = PROJ_1(down(struct!1(PROJ_2(down[[A, X]](iter(struct!1, j!1)(x!1))))))") (("1" (HIDE -2) (("1" (REPLACE -1 3 RL) (("1" (HIDE -1) (("1" (INST -1 "j!1" "0" "x!1") (("1" (PROP) (("1" (REPLACE -1) (("1" (HIDE -1 -2 2 4) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))) ("2" (ASSERT) NIL))))))))))) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL))))))) ("2" (ASSERT) NIL))))))))))))))))) ("2" (ASSERT) NIL))))))) ("2" (HIDE -1 2 3) (("2" (INDUCT "m") (("1" (SKOSIMP*) (("1" (EXPAND "iter") (("1" (INST -2 "x!2") (("1" (FLATTEN) (("1" (HIDE -2) (("1" (ASSERT) (("1" (EXPAND "next_impl") (("1" (LIFT-IF -2) (("1" (PROP) (("1" (HIDE -1 -3 1) (("1" (ASSERT) NIL))) ("2" (LEMMA "mono_up[[A, Seq_impl[A]]]") (("2" (INST?) (("1" (PROP) (("1" (CASE "shift(f!1(x!2)) = f!1(PROJ_2(down(struct!1(x!2))))") (("1" (REPLACE -1 2 RL) (("1" (EXPAND "shift") (("1" (PROPAX) NIL))))) ("2" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "iter" 1) (("2" (EXPAND "iter" -2) (("2" (LIFT-IF -2) (("2" (ASSERT) (("2" (PROP) (("2" (LIFT-IF 2) (("2" (PROP) (("2" (INST -3 "PROJ_2(down[[A, X]](iter(struct!1, j!2)(x!2)))") (("1" (FLATTEN) (("1" (HIDE -3) (("1" (ASSERT) (("1" (EXPAND "next_impl") (("1" (LIFT-IF -3) (("1" (SPLIT -3) (("1" (FLATTEN) (("1" (HIDE -1 -3 -4 1 2 3) (("1" (ASSERT) NIL))))) ("2" (FLATTEN) (("2" (LEMMA "mono_up[[A, Seq_impl[A]]]") (("2" (INST?) (("1" (PROP) (("1" (CASE "shift(f!1(PROJ_2(down[[A, X]](iter(struct!1, j!2)(x!2))))) = f!1(PROJ_2(down(struct!1(PROJ_2(down[[A, X]](iter(struct!1, j!2)(x!2)))))))") (("1" (HIDE -2) (("1" (REPLACE -1 3 RL) (("1" (HIDE -1) (("1" (HIDE -1) (("1" (EXPAND "shift") (("1" (INST -2 "k!1+1" "x!2") (("1" (PROP) (("1" (REPLACE -1) (("1" (HIDE -1 -2 1 2 4) (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))))))))))) ("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))(|Bisim| (|bisimulation?_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|bisimulation?_TCC2| "" (GRIND) NIL) (|bisim_bisim| "" (SKOSIMP*) (("" (EXPAND "bisimulation?") (("" (SKOSIMP*) (("" (EXPAND "bisim?") (("" (SKOSIMP*) (("" (CASE "bisimulation?(struct1!1, struct2!1)(R!1)") (("1" (EXPAND "bisimulation?" -1) (("1" (INST?) (("1" (ASSERT) (("1" (PROP) (("1" (INST 1 "R!1") (("1" (ASSERT) NIL))))))))))) ("2" (PROPAX) NIL))))))))))))) (|bisim_struct_TCC1| "" (GRIND) NIL) (|bisim_struct_TCC2| "" (GRIND) (("" (CASE "z!1 = (PROJ_1(z!1), PROJ_2(z!1))") (("1" (REPLACE -1 1 RL) (("1" (PROPAX) NIL))) ("2" (ASSERT) (("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))) (|bisim_struct_TCC3| "" (SKOSIMP*) (("" (TYPEPRED "R!1") (("" (EXPAND "bisimulation?") (("" (INST -1 "proj_1(z!1)" "proj_2(z!1)") (("" (ASSERT) (("" (TYPEPRED "z!1") (("" (CASE "z!1 = (PROJ_1(z!1), PROJ_2(z!1))") (("1" (REPLACE -1 -2 LR) (("1" (ASSERT) (("1" (EXPAND "incl") (("1" (ASSERT) NIL))))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))))))) (|bisim_struct_map| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "struct_map?") (("1" (CASE "bisimulation?(struct1!1, struct2!1)(R!1)") (("1" (EXPAND "bisimulation?" -1) (("1" (SKOSIMP*) (("1" (TYPEPRED "x!1") (("1" (INST -2 "proj_1(x!1)" "proj_2(x!1)") (("1" (ASSERT) (("1" (EXPAND "bisim_struct") (("1" (ASSERT) (("1" (EXPAND "incl") (("1" (REWRITE "next") (("1" (ASSERT) (("1" (CASE "bot?(struct1!1(PROJ_1(x!1)))") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))))) ("2" (PROPAX) NIL))))) ("2" (EXPAND "struct_map?") (("2" (CASE "bisimulation?(struct1!1, struct2!1)(R!1)") (("1" (EXPAND "bisimulation?" -1) (("1" (SKOSIMP*) (("1" (TYPEPRED "x!1") (("1" (INST -2 "proj_1(x!1)" "proj_2(x!1)") (("1" (ASSERT) (("1" (EXPAND "bisim_struct") (("1" (ASSERT) (("1" (EXPAND "incl") (("1" (REWRITE "next") (("1" (ASSERT) (("1" (CASE "bot?(struct1!1(PROJ_1(x!1)))") (("1" (ASSERT) (("1" (LIFT-IF) (("1" (ASSERT) (("1" (PROP) (("1" (ASSERT) (("1" (CASE "x!1 = (PROJ_1(x!1), PROJ_2(x!1)) ") (("1" (REPLACE -1 3 RL) (("1" (PROPAX) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))))) ("2" (ASSERT) (("2" (LIFT-IF) (("2" (PROP) (("1" (ASSERT) (("1" (CASE "x!1 = (PROJ_1(x!1), PROJ_2(x!1)) ") (("1" (REPLACE -1 2 RL) (("1" (PROPAX) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))) ("2" (ASSERT) NIL) ("3" (ASSERT) (("3" (CASE "x!1 = (PROJ_1(x!1), PROJ_2(x!1)) ") (("1" (REPLACE -1 3 RL) (("1" (PROPAX) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))))))))))))))))))))))))) ("2" (PROPAX) NIL))))))))) (|Kernel_bisim| "" (SKOSIMP*) (("" (EXPAND "bisimulation?") (("" (EXPAND "Kernel") (("" (SKOSIMP*) (("" (CASE "next(coreduce(struct1!1)(x1!1)) = next(coreduce(struct2!1)(x2!1))") (("1" (REWRITE "next") (("1" (REWRITE "next") (("1" (ASSERT) (("1" (LIFT-IF) (("1" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (ASSERT) (("3" (LEMMA "mono_up[[A,Seq[A]]]") (("3" (INST?) (("3" (ASSERT) NIL))))))) ("4" (ASSERT) (("4" (LEMMA "mono_up[[A,Seq[A]]]") (("4" (INST?) (("4" (ASSERT) NIL))))))))))))))))) ("2" (HIDE 2) (("2" (ASSERT) NIL))))))))))))) (|bisim_finality| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "bisim?") (("1" (SKOSIMP*) (("1" (LEMMA "struct_map_unique[A,(R!1)]") (("1" (LEMMA "bisim_struct_map") (("1" (INST?) (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) (("1" (PROP) (("1" (EXPAND "Kernel") (("1" (EXPAND "incl") (("1" (CASE "(LAMBDA (z: (R!1)): coreduce(struct1!1)(PROJ_1(z)))(x1!1,x2!1) = coreduce(struct1!1)(x1!1)") (("1" (REPLACE -2 -1 LR) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL))))))))))))))))))))))))) ("2" (EXPAND "bisim?") (("2" (INST + "Kernel(struct1!1, struct2!1)") (("2" (PROP) (("2" (LEMMA "Kernel_bisim") (("2" (GRIND) NIL))))))))))))))(|Seq_functoriality| (|seq_map_struct_TCC1| "" (SUBTYPE-TCC) NIL))(|Least_nat| (|least_TCC1| "" (INST + "LAMBDA(p: (nonempty?[nat])) : choose({n: nat | p(n) AND FORALL (m: nat): p(m) IMPLIES n <= m})") (("" (SKOSIMP*) (("" (EXPAND "nonempty?") (("" (TYPEPRED "p!1") (("" (EXPAND "empty?") (("" (EXPAND "nonempty?") (("" (EXPAND "empty?") (("" (SKOSIMP*) (("" (LEMMA "wf_nat") (("" (EXPAND "well_founded?") (("" (INST?) (("" (PROP) (("1" (SKOSIMP*) (("1" (INST -3 "y!1") (("1" (EXPAND "member") (("1" (SKOSIMP*) (("1" (TYPEPRED "y!1") (("1" (INST -2 "m!1") (("1" (ASSERT) NIL))))))))))))) ("2" (INST 1 "x!1") (("2" (ASSERT) (("2" (EXPAND "member") (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))(|Seq_prop| (|id_coreduce| "" (SKOSIMP) (("" (CASE "struct_map?(next)(LAMBDA(x:Seq[A]):x)") (("1" (LEMMA "coreduce_unique" ("g" "LAMBDA (x: Seq[A]):x")) (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1 :DIR RL) (("1" (ASSERT) NIL))))))))))) ("2" (EXPAND "struct_map?") (("2" (SKOSIMP) (("2" (PROP) (("2" (CASE "(PROJ_1(down(next(x!2))), PROJ_2(down(next(x!2))))=down(next(x!2))") (("1" (REPLACE -1 * LR) (("1" (APPLY-EXTENSIONALITY) NIL))) ("2" (APPLY-EXTENSIONALITY) NIL) ("3" (PROPAX) NIL))))))))))))) (|next_inv_struct_TCC1| "" (SUBTYPE-TCC) NIL) (|next_iso| "" (PROP) (("1" (SKOSIMP) (("1" (EXPAND "next_inv") (("1" (REWRITE "next") (("1" (CASE "bot?(x!1) OR up?(x!1)") (("1" (SPLIT) (("1" (GRIND) NIL) ("2" (GRIND) (("2" (APPLY-EXTENSIONALITY) (("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY) (("2" (HIDE 2) (("2" (NAME-REPLACE "k" "PROJ_2(down(x!1))") (("2" (REWRITE "id_coreduce" :SUBST ("x" "k")) (("2" (CASE "coreduce(next_inv_struct)(next(coreduce[A, Seq[A]](next[A])(k)))= (lambda (x: Seq[A]): coreduce(next_inv_struct)(next(x)))(k)") (("1" (REPLACE -1) (("1" (CASE "struct_map?(next)((LAMBDA (x: Seq[A]): coreduce(next_inv_struct)(next(x))))") (("1" (LEMMA "coreduce_unique[A,Seq[A]]") (("1" (INST?) (("1" (PROP) (("1" (REPLACE -1) (("1" (PROPAX) NIL))))))))) ("2" (HIDE 2) (("2" (GRIND) (("1" (REWRITE "next") (("1" (ASSERT) NIL))) ("2" (REWRITE "next") NIL))))))))) ("2" (ASSERT) (("2" (LEMMA "id_coreduce") (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))))))))))) ("2" (GRIND) NIL))))))))) ("2" (SKOSIMP) (("2" (REWRITE "id_coreduce") (("2" (LEMMA "id_coreduce") (("2" (INST?) (("2" (CASE "next_inv(next(coreduce[A, Seq[A]](next[A])(y!1)))=(lambda (x:Seq[A]):next_inv(next(coreduce[A, Seq[A]](next[A])(x))))(y!1)") (("1" (REPLACE -1) (("1" (LEMMA "coreduce_unique[A,Seq[A]]") (("1" (HIDE -2) (("1" (INST?) (("1" (INST * "(LAMBDA (x: Seq[A]): next_inv(next(coreduce[A, Seq[A]](next[A])(x))))") (("1" (PROP) (("1" (REPLACE -1) (("1" (PROPAX) NIL))) ("2" (HIDE 2) (("2" (EXPAND "struct_map?") (("2" (SKOSIMP) (("2" (GROUND) (("1" (REWRITE "next") (("1" (EXPAND "next_inv") (("1" (REWRITE "next") (("1" (EXPAND "next_inv_struct") (("1" (PROPAX) NIL))))))))) ("2" (REWRITE "next") (("2" (EXPAND "next_inv") (("2" (REWRITE "next") (("2" (EXPAND "next_inv_struct") (("2" (PROPAX) NIL))))))))))))))))))))))))))))) ("2" (ASSERT) NIL))))))))))))) (|final_bisim_finality| "" (SKOSIMP*) (("" (LEMMA "bisim_finality[A,Seq[A],Seq[A]]") (("" (INST -1 "next" "next" "x!1" "y!1") (("" (PROP) (("1" (EXPAND "Kernel") (("1" (LEMMA "id_coreduce") (("1" (INST-CP -1 "x!1") (("1" (INST -1 "y!1") (("1" (ASSERT) NIL))))))))) ("2" (EXPAND "bisim?") (("2" (INST 2 "R!1") (("2" (ASSERT) NIL))))))))))))) (|next_empty| "" (EXPAND "empty_seq") (("" (LEMMA "next_iso") (("" (PROP) (("" (INST?) NIL))))))) (|empty_unique| "" (SKOSIMP*) (("" (LEMMA "next_iso") (("" (PROP) (("" (EXPAND "empty_seq") (("" (CASE "next(x!1) = bot") (("1" (REPLACE -1 1 RL) (("1" (GRIND) NIL))) ("2" (ASSERT) NIL))))))))))) (|next_cons| "" (SKOSIMP*) (("" (EXPAND "cons_seq") (("" (LEMMA "next_iso") (("" (PROP) (("" (INST?) NIL))))))))) (|cons_unique| "" (SKOSIMP*) (("" (EXPAND "cons_seq") (("" (REPLACE -1 1 RL) (("" (HIDE -1) (("" (LEMMA "next_iso") (("" (PROP) (("" (INST? -2) (("" (ASSERT) NIL))))))))))))))) (|not_bot_next| "" (SKOSIMP*) (("" (LEMMA "up_exist[[A,Seq[A]]]") (("" (INST?) (("" (ASSERT) (("" (SKOSIMP*) (("" (INST 2 "proj_1(x!2)" "proj_2(x!2)") (("" (EXPAND "cons_seq") (("" (LEMMA "next_iso") (("" (PROP) (("" (INST? -2) (("" (ASSERT) NIL))))))))))))))))))))) (|cons_list_TCC1| "" (TERMINATION-TCC) NIL) (|cons_list_mono| "" (INDUCT "l") (("1" (SKOSIMP*) (("1" (EXPAND "cons_list") (("1" (ASSERT) (("1" (EXPAND "length") (("1" (ASSERT) NIL))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "cons_list" -3) (("2" (EXPAND "length" -2) (("2" (ASSERT) (("2" (CASE "k!1 = cons(car(k!1),cdr(k!1))") (("1" (REPLACE -1) (("1" (ASSERT) (("1" (CASE "next(cons_seq(cons1_var!1, cons_list(cons2_var!1, x!1))) = next(cons_seq(car(k!1), cons_list(cdr(k!1), y!1)))") (("1" (REWRITE "next_cons") (("1" (REWRITE "next_cons") (("1" (LEMMA "mono_up[[A,Seq[A]]]") (("1" (INST?) (("1" (ASSERT) (("1" (FLATTEN -1) (("1" (INST?) (("1" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) NIL))))))) ("2" (ASSERT) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))) ("3" (ASSERT) NIL))))))))))))) (|at_TCC1| "" (SKOSIMP*) (("" (LEMMA "cover[[A, Seq[A]]]") (("" (GRIND) NIL))))) (|at_TCC2| "" (SKOSIMP*) (("" (LEMMA "cover[[A, Seq[A]]]") (("" (INST?) (("" (ASSERT) NIL))))))) (|at_TCC3| "" (SUBTYPE-TCC) NIL) (|at_TCC4| "" (TERMINATION-TCC) NIL) (|at_empty| "" (SKOSIMP*) (("" (EXPAND "at") (("" (EXPAND "empty_seq") (("" (LEMMA "next_iso") (("" (PROP) (("" (CASE "bot?(next(next_inv(bot[[A, Seq[A]]])))") (("1" (ASSERT) NIL) ("2" (HIDE 2) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))) (|at_cons| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (EXPAND "at") (("1" (PROPAX) NIL))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "at" 1) (("2" (LIFT-IF) (("2" (PROP) (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (EXPAND "at") (("1" (PROPAX) NIL))))))) ("2" (LIFT-IF) (("2" (PROP) (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))) ("2" (INST?) (("2" (NAME "n" "at(x!1,j!1)") (("2" (REPLACE -1) (("2" (EXPAND "at" -2) (("2" (ASSERT) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (NAME "m" "at(PROJ_2(down(next(x!1))), j!1)") (("2" (REPLACE -1) (("2" (EXPAND "at" 2) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))) (|at_singleton_seq| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at") (("1" (EXPAND "singleton_seq") (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))))))) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (EXPAND "singleton_seq" 1) (("2" (EXPAND "at" 1) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (REWRITE "at_empty") NIL))))))))))))))) (|at_const_seq| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at") (("1" (EXPAND "const_seq") (("1" (REWRITE "next") (("1" (EXPAND "const_seq_struct") (("1" (PROPAX) NIL))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "at" 1) (("2" (EXPAND "const_seq" 1) (("2" (REWRITE "next") (("2" (EXPAND "const_seq_struct") (("2" (INST?) (("2" (EXPAND "const_seq") (("2" (EXPAND "const_seq_struct") (("2" (PROPAX) NIL))))))))))))))))))) (|tail_empty| "" (INDUCT "n") (("1" (EXPAND "tail") (("1" (PROPAX) NIL))) ("2" (SKOSIMP*) (("2" (EXPAND "tail" 1) (("2" (REWRITE "next_empty") (("2" (ASSERT) NIL))))))))) (|tail_cons| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "tail") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (EXPAND "tail") (("1" (PROPAX) NIL))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "tail" 1) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (LIFT-IF) (("2" (PROP) (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (LEMMA "tail_empty") (("1" (INST?) (("1" (ASSERT) NIL))))))))))))) ("2" (LEMMA "cons_unique") (("2" (LEMMA "up_exist[[A,Seq[A]]]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (ASSERT) (("2" (INST?) (("2" (INST -2 "proj_1(x!2)" "proj_2(x!2)") (("2" (ASSERT) (("2" (REPLACE -2) (("2" (INST? -3) NIL))))))))))))))))))))))))))))))))))))) (|tail_list| "" (INDUCT "l") (("1" (SKOSIMP*) (("1" (EXPAND "cons_list") (("1" (EXPAND "length") (("1" (PROPAX) NIL))))))) ("2" (SKOSIMP*) (("2" (EXPAND "cons_list" 1) (("2" (EXPAND "length" 1) (("2" (LEMMA "tail_cons") (("2" (INST?) (("2" (REPLACE -1 * RL) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))) (|tail_succ| "" (INDUCT "n") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "tail" 1 1) (("2" (EXPAND "tail" 1 3) (("2" (LIFT-IF) (("2" (PROP) (("1" (REWRITE "tail_empty") NIL) ("2" (GRIND) NIL))))))))))))) (|tail_tail| "" (INDUCT "m") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (LEMMA "tail_succ") (("2" (INST-CP -1 "tail(x!1,n!1)" "j!1") (("2" (REPLACE -2) (("2" (INST -1 "x!1" "n!1+j!1") (("2" (REPLACE -1) (("2" (INST -3 "x!1" "n!1") (("2" (ASSERT) NIL))))))))))))))))) (|at_tail| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "tail") (("1" (PROPAX) NIL))))) ("2" (SKOSIMP*) (("2" (NAME "aap" "at(tail(x!1, j!1 + 1), m!1)") (("2" (REPLACE -1) (("2" (EXPAND "tail" -1) (("2" (EXPAND "at" 1) (("2" (LIFT-IF) (("2" (PROP) (("1" (REWRITE "at_empty") (("1" (ASSERT) NIL))) ("2" (LEMMA "not_bot_next") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))) (|cons_at_tail_TCC1| "" (SUBTYPE-TCC) NIL) (|cons_at_tail| "" (SKOSIMP*) (("" (EXPAND "at") (("" (CASE "bot?(next(x!1))") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (EXPAND "tail") (("2" (EXPAND "tail") (("2" (ASSERT) (("2" (LEMMA "not_bot_next") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (ASSERT) (("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))))))))))))))))))))))))))) (|at_bot_tail| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at") (("1" (EXPAND "tail") (("1" (LIFT-IF) (("1" (PROP) (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "at" -2) (("2" (LIFT-IF -2) (("2" (PROP) (("1" (LEMMA "empty_unique") (("1" (INST -1 "x!1") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (REWRITE "tail_empty") NIL))))))))) ("2" (EXPAND "tail" 2) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))) (|tail_singleton_seq| "" (SKOSIMP*) (("" (LIFT-IF) (("" (PROP) (("1" (EXPAND "tail") (("1" (ASSERT) NIL))) ("2" (EXPAND "tail") (("2" (ASSERT) (("2" (EXPAND "singleton_seq") (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (REWRITE "tail_empty") NIL))))))))))))))))) (|tail_const_seq| "" (INDUCT "n") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "tail" 1) (("2" (EXPAND "const_seq" 1 1) (("2" (EXPAND "const_seq" 1 1) (("2" (REWRITE "next") (("2" (EXPAND "const_seq_struct") (("2" (INST?) (("2" (EXPAND "const_seq") (("2" (ASSERT) (("2" (EXPAND "const_seq_struct") (("2" (PROPAX) NIL))))))))))))))))))))))) (|at_eqn_rel_bisim| "" (EXPAND "bisimulation?") (("" (EXPAND "at_eqn_rel") (("" (SKOSIMP*) (("" (CASE "bot?(next[A](x1!1))") (("1" (ASSERT) (("1" (INST -2 "0") (("1" (EXPAND "at") (("1" (ASSERT) (("1" (LIFT-IF) (("1" (PROP) (("1" (ASSERT) NIL))))))))))))) ("2" (ASSERT) (("2" (PROP) (("1" (INST -2 "0") (("1" (EXPAND "at") (("1" (LIFT-IF) (("1" (PROP) (("1" (ASSERT) NIL))))))))) ("2" (INST -1 "0") (("2" (EXPAND "at") (("2" (LEMMA "mono_up[A]") (("2" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))) ("3" (SKOSIMP*) (("3" (LEMMA "not_bot_next") (("3" (INST-CP -1 "x2!1") (("3" (ASSERT) (("3" (INST -1 "x1!1") (("3" (ASSERT) (("3" (SKOSIMP*) (("3" (REPLACE -1) (("3" (REPLACE -2) (("3" (REWRITE "next_cons") (("3" (REWRITE "next_cons") (("3" (ASSERT) (("3" (INST -3 "n!1+1") (("3" (LEMMA "at_cons") (("3" (INST-CP -1 "y!1" "a!1" "n!1") (("3" (INST -1 "y!2" "a!2" "n!1") (("3" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))) (|at_eqn| "" (LEMMA "bisim_finality[A,Seq[A],Seq[A]]") (("" (INST -1 "next[A]" "next[A]" "_" "_") (("" (SKOSIMP*) (("" (INST -1 "x!1" "y!1") (("" (LEMMA "at_eqn_rel_bisim") (("" (CASE "bisim?(next[A], next[A])(x!1, y!1)") (("1" (ASSERT) (("1" (EXPAND "Kernel") (("1" (LEMMA "id_coreduce") (("1" (INST-CP -1 "x!1") (("1" (INST -1 "y!1") (("1" (ASSERT) NIL))))))))))) ("2" (EXPAND "bisim?") (("2" (INST 1 "at_eqn_rel") (("2" (PROP) (("1" (EXPAND "at_eqn_rel") (("1" (PROPAX) NIL))) ("2" (EXPAND "at_eqn_rel") (("2" (PROPAX) NIL))))))))))))))))))))) (|list_incl_null| "" (EXPAND "list_incl") (("" (LEMMA "empty_unique") (("" (INST?) (("" (ASSERT) (("" (REWRITE "next") (("" (LIFT-IF) (("" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (EXPAND "list_incl_struct") (("2" (PROPAX) NIL))))))))))))))))))) (|list_incl_cons| "" (SKOSIMP*) (("" (EXPAND "list_incl") (("" (LEMMA "next_iso") (("" (PROP) (("" (HIDE -1) (("" (INST-CP -1 "coreduce(list_incl_struct)(cons(a!1, l!1))") (("" (INST -1 "cons_seq(a!1, coreduce(list_incl_struct)(l!1))") (("" (REWRITE "next_cons") (("" (REPLACE -1 1 RL) (("" (HIDE -1) (("" (REWRITE "next") (("" (NAME "aap" "list_incl_struct(cons(a!1, l!1))") (("" (REPLACE -1 -2 LR) (("" (EXPAND "list_incl_struct" -1) (("" (ASSERT) (("" (REPLACE -1 -2 RL) (("" (ASSERT) NIL))))))))))))))))))))))))))))))))) (|list_incl_list| "" (INDUCT "l") (("1" (REWRITE "list_incl_null") (("1" (GRIND) NIL))) ("2" (SKOSIMP*) (("2" (REWRITE "list_incl_cons") (("2" (EXPAND "cons_list" 1) (("2" (ASSERT) NIL))))))))) (|at_list_incl_up| "" (INDUCT "l") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (REWRITE "list_incl_cons") (("2" (EXPAND "length" -2) (("2" (CASE "n!1=0") (("1" (REPLACE -1) (("1" (EXPAND "at" 1) (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))))) ("2" (LEMMA "at_cons") (("2" (INST -1 "list_incl(cons2_var!1)" "cons1_var!1" "n!1-1") (("1" (INST -2 "n!1-1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))) ("2" (ASSERT) NIL))))))))))))))) (|at_cons_list_TCC1| "" (SUBTYPE-TCC) NIL) (|at_cons_list| "" (INDUCT "l") (("1" (SKOSIMP*) (("1" (EXPAND "cons_list") (("1" (EXPAND "length") (("1" (PROPAX) NIL))))))) ("2" (SKOSIMP*) (("2" (EXPAND "cons_list" 1) (("2" (LIFT-IF 1) (("2" (PROP) (("1" (EXPAND "length" -1) (("1" (CASE "n!1=0") (("1" (REPLACE -1) (("1" (EXPAND "at" 1) (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (REWRITE "list_incl_cons") (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))))))))))) ("2" (REWRITE "list_incl_cons") (("2" (LEMMA "at_cons") (("2" (INST-CP -1 "list_incl(cons2_var!1)" "cons1_var!1" "n!1-1") (("1" (ASSERT) (("1" (INST -1 "cons_list(cons2_var!1, x!1)" "cons1_var!1" "n!1-1") (("1" (INST -4 "x!1" "n!1-1") (("1" (ASSERT) NIL))))))) ("2" (ASSERT) NIL))))))))))) ("2" (EXPAND "length" 1) (("2" (EXPAND "length" 2) (("2" (INST -1 "x!1" "n!1-1") (("1" (ASSERT) (("1" (LEMMA "at_cons") (("1" (INST -1 "cons_list(cons2_var!1, x!1)" "cons1_var!1" "n!1-1") (("1" (ASSERT) NIL))))))) ("2" (ASSERT) NIL))))))))))))))) ("3" (ASSERT) (("3" (SKOSIMP*) (("3" (ASSERT) NIL))))))) (|cons_list_append| "" (INDUCT "l") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "cons_list" 1 1) (("2" (EXPAND "append" 1) (("2" (EXPAND "cons_list" 1 3) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))) (|finite_cons| "" (SKOSIMP*) (("" (EXPAND "finite?") (("" (SKOSIMP*) (("" (INST 1 "cons(a!1,l!1)") (("" (REWRITE "list_incl_cons") (("" (ASSERT) NIL))))))))))) (|finite_list| "" (SKOLEM!) (("" (PROP) (("" (INDUCT "l") (("1" (EXPAND "cons_list") (("1" (PROPAX) NIL))) ("2" (SKOSIMP*) (("2" (LEMMA "finite_cons") (("2" (EXPAND "cons_list" 1) (("2" (INST?) (("2" (ASSERT) (("2" (INST?) NIL))))))))))))))))) (|infinite_cons| "" (SKOSIMP*) (("" (EXPAND "infinite?") (("" (SKOSIMP*) (("" (INST 1 "LAMBDA(n:nat) : IF n=0 THEN a!1 ELSE f!1(n-1) ENDIF") (("1" (CASE "next(inf_incl(LAMBDA (n: nat): IF n = 0 THEN a!1 ELSE f!1(n - 1) ENDIF)) = next(cons_seq(a!1, x!1))") (("1" (HIDE -2) (("1" (LEMMA "next_iso") (("1" (PROP) (("1" (HIDE -1) (("1" (INST-CP -1 "inf_incl(LAMBDA (n: nat): IF n = 0 THEN a!1 ELSE f!1(n - 1) ENDIF)") (("1" (INST -1 "cons_seq(a!1, x!1)") (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (ASSERT) NIL))))))))))))) ("2" (HIDE 2) (("2" (EXPAND "inf_incl") (("2" (REWRITE "next") (("2" (REWRITE "next_cons") (("2" (EXPAND "inf_incl_struct" 1 1) (("2" (EXPAND "inf_incl_struct" 1 1) (("2" (EXPAND "inf_incl_struct" 1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (CASE "f!1 = LAMBDA (n: nat): f!1(n)") (("1" (REPLACE -1 1 RL) (("1" (PROPAX) NIL))) ("2" (HIDE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))))))))))))) ("3" (SKOSIMP*) (("3" (ASSERT) NIL))))) ("2" (ASSERT) (("2" (SKOSIMP*) (("2" (ASSERT) NIL))))))))))))) (|infinite_list| "" (SKOLEM!) (("" (PROP) (("" (INDUCT "l") (("1" (EXPAND "cons_list") (("1" (PROPAX) NIL))) ("2" (SKOSIMP*) (("2" (EXPAND "cons_list" 1) (("2" (LEMMA "infinite_cons") (("2" (INST?) (("2" (ASSERT) (("2" (INST?) NIL))))))))))))))))) (|at_inf_incl| "" (INDUCT "n") (("1" (EXPAND "at") (("1" (SKOSIMP*) (("1" (EXPAND "inf_incl") (("1" (REWRITE "next") (("1" (EXPAND "inf_incl_struct") (("1" (PROPAX) NIL))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "at" 1) (("2" (EXPAND "inf_incl" 1) (("2" (REWRITE "next") (("2" (EXPAND "inf_incl_struct") (("2" (INST -1 "LAMBDA (n: nat): f!1(1 + n)") (("2" (ASSERT) (("2" (EXPAND "inf_incl") (("2" (EXPAND "inf_incl_struct") (("2" (PROPAX) NIL))))))))))))))))))))) (|inf_incl_mono| "" (SKOSIMP*) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (LEMMA "at_inf_incl") (("" (INST-CP -1 "f!1" "x!1") (("" (INST -1 "g!1" "x!1") (("" (REPLACE -3) (("" (REPLACE -1) (("" (LEMMA "mono_up[A]") (("" (INST?) (("" (ASSERT) NIL))))))))))))))))))) (|finite?_length_at| "" (INDUCT "l") (("1" (REWRITE "list_incl_null") (("1" (REWRITE "at_empty") (("1" (ASSERT) NIL))))) ("2" (SKOSIMP*) (("2" (REWRITE "list_incl_cons") (("2" (EXPAND "length" 1) (("2" (LEMMA "at_cons") (("2" (INST?) (("2" (REPLACE -1 1 RL) (("2" (PROPAX) NIL))))))))))))))) (|at_up_to_empty| "" (SKOSIMP*) (("" (EXPAND "at_up_to") (("" (REWRITE "next_empty") (("" (ASSERT) NIL))))))) (|at_up_to_cons_TCC1| "" (SUBTYPE-TCC) NIL) (|at_up_to_cons| "" (SKOSIMP*) (("" (EXPAND "at_up_to" 1 1) (("" (REWRITE "next_cons") (("" (ASSERT) NIL))))))) (|at_up_to_list| "" (INDUCT "l") (("1" (SKOSIMP*) (("1" (EXPAND "cons_list") (("1" (EXPAND "length") (("1" (EXPAND "at_up_to") (("1" (PROPAX) NIL))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "cons_list" 1) (("2" (EXPAND "length" 1) (("2" (EXPAND "at_up_to" 1) (("2" (ASSERT) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))) (|length_at_up_to_TCC1| "" (SUBTYPE-TCC) NIL) (|length_at_up_to| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at") (("1" (EXPAND "at_up_to") (("1" (EXPAND "length") (("1" (PROPAX) NIL))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "at_up_to" 1) (("2" (EXPAND "length" 1) (("2" (ASSERT) (("2" (CASE "bot?(next(x!1))") (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (REWRITE "at_empty") (("1" (ASSERT) NIL))))))))))) ("2" (ASSERT) (("2" (INST -1 "PROJ_2(down(next(x!1)))") (("2" (ASSERT) (("2" (PROP) (("2" (EXPAND "at" 3) (("2" (ASSERT) NIL))))))))))))))))))))) ("3" (SKOSIMP*) (("3" (ASSERT) NIL))))) (|at_up_to_at| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at") (("1" (EXPAND "at_up_to") (("1" (LIFT-IF) (("1" (PROP) (("1" (ASSERT) (("1" (REWRITE "list_incl_null") (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))))) ("2" (REWRITE "list_incl_null") (("2" (REWRITE "next_empty") (("2" (ASSERT) NIL))))))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "at_up_to" 1) (("2" (CASE "bot?(next(x!1))") (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (REWRITE "list_incl_null") (("1" (REWRITE "at_empty") (("1" (ASSERT) NIL))))))))))))) ("2" (LEMMA "not_bot_next") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (REWRITE "list_incl_cons") (("2" (LIFT-IF) (("2" (PROP) (("1" (CASE "m!1=0") (("1" (REPLACE -1) (("1" (EXPAND "at") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))))))))) ("2" (LEMMA "at_cons") (("2" (INST-CP -1 "y!1" "a!1" "m!1-1") (("1" (INST -1 "list_incl(at_up_to(y!1, j!1))" "a!1" "m!1-1") (("1" (ASSERT) (("1" (REPLACE -1 * RL) (("1" (REPLACE -2 * RL) (("1" (INST -5 "y!1" "m!1-1") (("1" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))) ("2" (ASSERT) NIL))))))) ("2" (LEMMA "at_cons") (("2" (INST -1 "list_incl(at_up_to(y!1, j!1))" "a!1" "m!1-1") (("1" (REPLACE -1 * RL) (("1" (INST -3 "y!1" "m!1-1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))))))))))))))))))))))))) (|at_up_to_eqn| "" (SKOSIMP*) (("" (LEMMA "at_eqn") (("" (INST?) (("" (PROP) (("" (SKOSIMP*) (("" (INST -1 "n!1+1") (("" (LEMMA "at_up_to_at") (("" (INST-CP -1 "x!1" "n!1+1" "n!1") (("" (INST -1 "y!1" "n!1+1" "n!1") (("" (ASSERT) NIL))))))))))))))))))) (|at_up_to_at_up_to| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "min") (("1" (EXPAND "at_up_to" 1 2) (("1" (EXPAND "at_up_to" 1 2) (("1" (REWRITE "list_incl_null") (("1" (REWRITE "at_up_to_empty") NIL))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "min") (("2" (LIFT-IF 1) (("2" (PROP) (("1" (EXPAND "at_up_to" 1 2) (("1" (LIFT-IF) (("1" (PROP) (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (REWRITE "at_up_to_empty") (("1" (REWRITE "list_incl_null") (("1" (REWRITE "at_up_to_empty") NIL))))))))))))) ("2" (ASSERT) (("2" (REWRITE "list_incl_cons") (("2" (REWRITE "at_up_to_cons") (("2" (CASE "m!1 = 0") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (EXPAND "at_up_to") (("1" (PROPAX) NIL))))))) ("2" (ASSERT) (("2" (INST -2 "PROJ_2(down(next(x!1)))" "m!1-1") (("2" (ASSERT) (("2" (REPLACE -2) (("2" (EXPAND "at_up_to" 3 2) (("2" (PROPAX) NIL))))))))))))))))))))))))) ("2" (EXPAND "at_up_to" 2 2) (("2" (LIFT-IF) (("2" (PROP) (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (REWRITE "at_up_to_empty") (("1" (REWRITE "list_incl_null") (("1" (REWRITE "at_up_to_empty") NIL))))))))))))) ("2" (REWRITE "list_incl_cons") (("2" (REWRITE "at_up_to_cons") (("2" (ASSERT) (("2" (INST -1 "PROJ_2(down(next(x!1)))" "m!1-1") (("2" (REPLACE -1) (("2" (ASSERT) (("2" (EXPAND "at_up_to" 2 2) (("2" (PROPAX) NIL))))))))))))))))))))))))))))))) (|cons_list_at_up_to| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at_up_to") (("1" (EXPAND "tail") (("1" (EXPAND "cons_list") (("1" (PROPAX) NIL))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "at_up_to" 1) (("2" (EXPAND "tail" 1) (("2" (CASE "bot?(next(x!1))") (("1" (ASSERT) (("1" (EXPAND "cons_list") (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (ASSERT) (("2" (LEMMA "not_bot_next") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (EXPAND "cons_list" 2) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))) (|sublist_nonnull| "" (SKOSIMP*) (("" (EXPAND "sublist") (("" (EXPAND "at_up_to") (("" (ASSERT) (("" (LIFT-IF) (("" (PROP) (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) (("1" (LEMMA "at_tail") (("1" (INST -1 "x!1" "n!1" "0") (("1" (REPLACE -2) (("1" (REWRITE "at_empty") (("1" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) NIL))))))))))))) (|at_sublist| "" (SKOSIMP*) (("" (EXPAND "sublist") (("" (REWRITE "at_up_to_at") (("" (REWRITE "at_tail") NIL))))))) (|tail_sublist_TCC1| "" (SUBTYPE-TCC) NIL) (|tail_sublist| "" (LEMMA "at_eqn") (("" (SKOSIMP*) (("" (INST -1 "tail(list_incl(sublist(x!1, n!1, m!1)), k!1)" "IF k!1 < m!1 THEN list_incl(sublist(x!1, n!1 + k!1, m!1 - k!1)) ELSE empty_seq ENDIF") (("1" (ASSERT) (("1" (PROP) (("1" (HIDE 2) (("1" (SKOSIMP*) (("1" (REWRITE "at_tail") (("1" (EXPAND "sublist") (("1" (REWRITE "at_up_to_at") (("1" (REWRITE "at_tail") (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (REWRITE "at_up_to_at") (("1" (REWRITE "at_empty") (("1" (REWRITE "at_tail") (("1" (ASSERT) NIL))))) ("2" (REWRITE "at_empty") NIL))))))))))))))))))))))) ("2" (ASSERT) (("2" (HIDE 2) (("2" (PROP) (("2" (ASSERT) NIL))))))))))))) (|at_up_to_sublist| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at_up_to" 1 1) (("1" (EXPAND "append") (("1" (EXPAND "sublist") (("1" (EXPAND "tail") (("1" (PROPAX) NIL))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "at_up_to" 1) (("2" (CASE "bot?(next(x!1))") (("1" (ASSERT) (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (EXPAND "sublist" 1) (("1" (REWRITE "tail_empty") (("1" (REWRITE "at_up_to_empty") (("1" (EXPAND "append") (("1" (PROPAX) NIL))))))))))))))))))) ("2" (ASSERT) (("2" (EXPAND "append" 2) (("2" (EXPAND "sublist" 2) (("2" (EXPAND "tail" 2) (("2" (INST -1 "PROJ_2(down(next(x!1)))" "m!1") (("2" (EXPAND "sublist") (("2" (ASSERT) NIL))))))))))))))))))))) (|cons_list_at_up_to_sublist_tail| "" (SKOSIMP*) (("" (REWRITE "cons_list_append") (("" (REWRITE "at_up_to_sublist") (("" (REWRITE "cons_list_at_up_to") NIL))))))) (|list_incl_mono| "" (INDUCT "l") (("1" (SKOSIMP*) (("1" (REWRITE "list_incl_null") (("1" (CASE "next(empty_seq) = next(list_incl(k!1))") (("1" (REWRITE "next_empty") (("1" (EXPAND "list_incl") (("1" (REWRITE "next") (("1" (EXPAND "list_incl_struct") (("1" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))))))) ("2" (SKOSIMP*) (("2" (EXPAND "list_incl" -2 2) (("2" (CASE "next(list_incl(cons(cons1_var!1, cons2_var!1))) = next(coreduce(list_incl_struct)(k!1))") (("1" (HIDE -3) (("1" (REWRITE "list_incl_cons") (("1" (REWRITE "next_cons") (("1" (REWRITE "next") (("1" (EXPAND "list_incl_struct" -1 2) (("1" (ASSERT) (("1" (CASE "bot?(list_incl_struct(k!1))") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (CASE "k!1 = null") (("1" (REPLACE -1) (("1" (EXPAND "list_incl_struct") (("1" (PROPAX) NIL))))) ("2" (CASE "cons?(k!1)") (("1" (ASSERT) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (LEMMA "mono_up[[A,Seq[A]]]") (("1" (INST?) (("1" (ASSERT) (("1" (PROP) (("1" (CASE "k!1 = cons(car(k!1),cdr(k!1))") (("1" (REPLACE -1) (("1" (EXPAND "list_incl_struct" -3 2) (("1" (INST -6 "cdr(k!1)") (("1" (ASSERT) (("1" (GRIND) NIL))))))))) ("2" (ASSERT) (("2" (GRIND) (("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))))))))))) ("2" (GRIND) NIL))))))))))))))))))))) ("2" (ASSERT) NIL))))))))) (|at_list| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at") (("1" (LIFT-IF) (("1" (PROP) (("1" (HIDE -2) (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (INST 1 "null") (("1" (REWRITE "list_incl_null") NIL))))))))))))) ("2" (ASSERT) NIL))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "at" -2) (("2" (LIFT-IF) (("2" (PROP) (("1" (LEMMA "empty_unique") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (INST + "null") (("1" (REWRITE "list_incl_null") NIL))))))))))) ("2" (LEMMA "not_bot_next") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (INST -3 "y!1") (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (INST 2 "cons(a!1,l!1)") (("2" (REWRITE "list_incl_cons") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))) (|finite?_at| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "finite?") (("1" (SKOSIMP*) (("1" (INST + "length(l!1)") (("1" (LEMMA "finite?_length_at") (("1" (GRIND) NIL))))))))) ("2" (LEMMA "at_list") (("2" (SKOSIMP*) (("2" (INST?) (("2" (ASSERT) (("2" (GRIND) NIL))))))))))))) (|infinite?_at| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "infinite?") (("1" (SKOLEM! -1) (("1" (REPLACE -1 1 RL) (("1" (HIDE -1) (("1" (LEMMA "at_inf_incl") (("1" (INST?) (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) NIL))))))))))))))))) ("2" (EXPAND "infinite?") (("2" (INST + "LAMBDA(n:nat) : down(at(x!1,n))") (("1" (LEMMA "at_eqn") (("1" (INST?) (("1" (PROP) (("1" (HIDE 2) (("1" (LEMMA "at_inf_incl") (("1" (INST?) (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (ASSERT) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (INST?) (("1" (ASSERT) NIL))))))))))))))) ("2" (HIDE 2) (("2" (GRIND) NIL))))))))))) ("2" (HIDE 2) (("2" (GRIND) NIL))))))) ("2" (GRIND) NIL))))))))) (|finite_tail| "" (SKOSIMP*) (("" (LEMMA "finite?_at") (("" (INST-CP -1 "x!1") (("" (INST -1 "tail(x!1, n!1)") (("" (ASSERT) (("" (SKOSIMP*) (("" (INST 1 "n!2") (("" (REWRITE "at_tail") (("" (LEMMA "at_tail") (("" (INST -1 "x!1" "n!2" "n!1") (("" (REPLACE -1 1 RL) (("" (LEMMA "at_bot_tail") (("" (INST?) (("" (ASSERT) (("" (REPLACE -1) (("" (REWRITE "at_empty") (("" (ASSERT) NIL))))))))))))))))))))))))))))))))) (|infinite_tail| "" (SKOSIMP*) (("" (LEMMA "infinite?_at") (("" (INST-CP -1 "x!1") (("" (INST -1 "tail(x!1, n!1)") (("" (ASSERT) (("" (SKOSIMP*) (("" (REWRITE "at_tail") (("" (INST -2 "n!1+n!2") NIL))))))))))))))) (|fin_inf| "" (SKOSIMP*) (("" (LEMMA "finite?_at") (("" (LEMMA "infinite?_at") (("" (INST?) (("" (INST?) (("" (EXPAND "XOR") (("" (EXPAND "/=") (("" (IFF) (("" (GROUND) (("1" (SKOSIMP*) (("1" (INST?) NIL))) ("2" (SKOSIMP*) (("2" (INST?) NIL))))))))))))))))))))))(|Final_invariant| (|gi_invariant| "" (SKOSIMP*) (("" (EXPAND "invariant?") (("" (SKOSIMP*) (("" (EXPAND "gi") (("" (SKOSIMP*) (("" (EXPAND "tail" 1 2) (("" (REWRITE "tail_tail") (("" (INST?) NIL))))))))))))))) (|li_invariant| "" (SKOSIMP*) (("" (EXPAND "invariant?") (("" (SKOSIMP*) (("" (EXPAND "li") (("" (SKOSIMP*) (("" (EXPAND "tail" 1 1) (("" (REPLACE -2) (("" (REWRITE "tail_tail") (("" (INST 1 "y!1" "n!1+1") (("" (ASSERT) NIL))))))))))))))))))) (|gi_invariant_char| "" (SKOSIMP*) (("" (PROP) (("1" (SKOSIMP*) (("1" (EXPAND "invariant?") (("1" (EXPAND "gi") (("1" (INDUCT "n") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (INST -2 "tail(x!1, j!1)") (("2" (ASSERT) (("2" (EXPAND "tail" -2 1) (("2" (REWRITE "tail_tail") NIL))))))))))))))))) ("2" (EXPAND "invariant?") (("2" (SKOSIMP*) (("2" (EXPAND "tail" 1) (("2" (INST?) (("2" (ASSERT) (("2" (EXPAND "gi") (("2" (INST?) NIL))))))))))))))))) (|li_invariant_char| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "invariant?") (("1" (SKOSIMP*) (("1" (EXPAND "li") (("1" (SKOSIMP*) (("1" (CASE "forall(n:nat) : P!1(tail(y!1,n))") (("1" (REPLACE -4) (("1" (INST?) NIL))) ("2" (HIDE -3 2) (("2" (INDUCT "n") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (INST -2 "tail(y!1, j!1)") (("2" (ASSERT) (("2" (EXPAND "tail" -2 1) (("2" (REWRITE "tail_tail") NIL))))))))))))))))))))))) ("2" (EXPAND "invariant?") (("2" (SKOSIMP*) (("2" (INST -1 "tail(x!1)") (("2" (ASSERT) (("2" (EXPAND "tail") (("2" (EXPAND "li") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))) (|gi_monotone| "" (SKOSIMP*) (("" (EXPAND "gi") (("" (SKOSIMP*) (("" (INST -2 "n!1") (("" (INST?) (("" (ASSERT) NIL))))))))))) (|li_monotone| "" (SKOSIMP*) (("" (EXPAND "li") (("" (SKOSIMP*) (("" (REPLACE -3) (("" (HIDE -3) (("" (INST -1 "y!1") (("" (ASSERT) (("" (INST 1 "y!1" "n!1") (("" (ASSERT) NIL))))))))))))))))) (|gi_greatest| "" (SKOSIMP*) (("" (LEMMA "gi_monotone") (("" (INST?) (("" (ASSERT) (("" (PROP) (("" (INST?) (("" (ASSERT) (("" (LEMMA "gi_invariant_char") (("" (INST -1 "Q!1") (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL))))))))))))))))))))))) (|li_least| "" (SKOSIMP*) (("" (LEMMA "li_monotone") (("" (INST?) (("" (PROP) (("" (LEMMA "li_invariant_char") (("" (INST -1 "Q!1") (("" (ASSERT) (("" (INST?) (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL))))))))))))))))))))))(|Invariant| (|invariant?_TCC1| "" (SUBTYPE-TCC) NIL) (|invariant_struct_TCC1| "" (SUBTYPE-TCC) NIL) (|invariant_struct_TCC2| "" (SUBTYPE-TCC) NIL) (|invariant_struct_map| "" (SKOSIMP*) (("" (EXPAND "invariant?") (("" (EXPAND "struct_map?") (("" (SKOSIMP*) (("" (REWRITE "next") (("" (EXPAND "invariant_struct") (("" (ASSERT) (("" (CASE "bot?(struct!1(x!1))") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))) (|struct_gi_greatest| "" (SKOSIMP*) (("" (LEMMA "gi_greatest[A]") (("" (INST -1 "Q!1" "LAMBDA(x:Seq[A]) : EXISTS(y:X) : x = coreduce(struct!1)(y) AND P!1(y)") (("" (ASSERT) (("" (PROP) (("1" (INST -1 "coreduce(struct!1)(x!1)") (("1" (PROP) (("1" (INST?) (("1" (ASSERT) NIL))))))) ("2" (HIDE 2) (("2" (EXPAND "invariant?") (("2" (SKOSIMP*) (("2" (EXPAND "tail") (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (EXPAND "tail") (("2" (REWRITE "next") (("2" (ASSERT) (("2" (CASE "bot?(struct!1(y!1))") (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) (("1" (CASE "bot?(next(coreduce(struct!1)(y!1)) )") (("1" (LEMMA "empty_unique[A]") (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (REWRITE "next") (("2" (ASSERT) NIL))))))))))) ("2" (ASSERT) (("2" (EXPAND "tail") (("2" (INST?) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (REPLACE -1) (("3" (INST?) (("3" (ASSERT) NIL))))))))))))))))))))(|Seq_comp| (|comp_struct_TCC1| "" (SUBTYPE-TCC) NIL) (|comp_struct_TCC2| "" (SUBTYPE-TCC) NIL) (|comp_empty1| "" (LEMMA "id_coreduce[A]") (("" (LEMMA "coreduce_unique[A,Seq[A]]") (("" (INST?) (("" (INST -1 "LAMBDA(x:Seq[A]):comp(empty_seq,x)") (("" (ASSERT) (("" (PROP) (("1" (SKOSIMP*) (("1" (INST -2 "x!1") (("1" (REPLACE -1 -2 RL) (("1" (ASSERT) NIL))))))) ("2" (HIDE 2) (("2" (HIDE -1) (("2" (EXPAND "struct_map?") (("2" (SKOSIMP*) (("2" (PROP) (("1" (LEMMA "empty_unique[A]") (("1" (INST -1 "x!1") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (EXPAND "comp") (("1" (REWRITE "next") (("1" (EXPAND "comp_struct") (("1" (PROPAX) NIL))))))))))))))) ("2" (ASSERT) (("2" (LEMMA "not_bot_next[A]") (("2" (INST -1 "x!1") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (HIDE -2) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (EXPAND "comp" 1 1) (("2" (REWRITE "next") (("2" (ASSERT) (("2" (EXPAND "comp" 1 1) (("2" (EXPAND "comp_struct" 1 1) (("2" (REWRITE "next_empty") (("2" (ASSERT) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (EXPAND "comp_struct" 1 1) (("2" (REWRITE "next_empty") (("2" (ASSERT) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (EXPAND "comp_struct" 1 2) (("2" (REWRITE "next_empty") (("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|comp_empty2| "" (LEMMA "final_bisim_finality[A]") (("" (INST -1 "LAMBDA(y,x:Seq[A]) : y = comp(x,empty_seq)") (("" (PROP) (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) NIL))))))) ("2" (HIDE 2) (("2" (EXPAND "bisimulation?") (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (EXPAND "comp") (("2" (REWRITE "next") (("2" (NAME "ape" "comp_struct(x2!1, empty_seq)") (("2" (REPLACE -1) (("2" (EXPAND "comp_struct" -1) (("2" (REWRITE "next_empty") (("2" (ASSERT) (("2" (LIFT-IF) (("2" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL) ("4" (ASSERT) NIL) ("5" (ASSERT) NIL) ("6" (ASSERT) NIL) ("7" (ASSERT) (("7" (REPLACE -1 1 RL) (("7" (ASSERT) NIL))))) ("8" (ASSERT) (("8" (REPLACE -1 1 RL) (("8" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))) (|comp_assoc| "" (LEMMA "final_bisim_finality[A]") (("" (INST -1 "LAMBDA(u,v: Seq[A]) : EXISTS(x,y,z:Seq[A]) : u = comp(x, comp(y, z)) AND v = comp(comp(x, y), z)") (("" (PROP) (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (INST -1 "comp(x!1, comp(y!1, z!1))" "comp(comp(x!1, y!1), z!1)") (("1" (PROP) (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL))))))))))))) ("2" (HIDE 2) (("2" (EXPAND "bisimulation?") (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (REPLACE -2) (("2" (HIDE -1 -2) (("2" (EXPAND "comp") (("2" (REWRITE "next") (("2" (REWRITE "next") (("2" (NAME "ape" "comp_struct(x!1, coreduce(comp_struct)(y!1, z!1))") (("2" (REPLACE -1) (("2" (NAME "dog" "comp_struct(coreduce(comp_struct)(x!1, y!1), z!1)") (("2" (REPLACE -1) (("2" (EXPAND "comp_struct" -2 1) (("2" (EXPAND "comp_struct" -1 1) (("2" (REWRITE "next") (("2" (REWRITE "next") (("2" (CASE "bot?(next(x!1))") (("1" (ASSERT) (("1" (NAME "cow" "comp_struct(x!1, y!1)") (("1" (REPLACE -1) (("1" (EXPAND "comp_struct" -1) (("1" (CASE "bot?(next(y!1))") (("1" (ASSERT) (("1" (NAME "horse" "comp_struct(y!1, z!1)") (("1" (REPLACE -1) (("1" (EXPAND "comp_struct" -1) (("1" (CASE "bot?(next(z!1))") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (REPLACE -1 * RL) (("2" (ASSERT) (("2" (REPLACE -5 * RL) (("2" (REPLACE -6 * RL) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (LEMMA "comp_empty1") (("2" (INST -1 "empty_seq") (("2" (EXPAND "comp" -1) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (REPLACE -1 * RL) (("2" (ASSERT) (("2" (NAME "horse" "comp_struct(y!1, z!1)") (("2" (REPLACE -1) (("2" (EXPAND "comp_struct" -1) (("2" (ASSERT) (("2" (REPLACE -1 * RL) (("2" (ASSERT) (("2" (REPLACE -4 * RL) (("2" (ASSERT) (("2" (REPLACE -5 * RL) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (NAME "cow" "comp_struct(x!1, y!1)") (("2" (REPLACE -1) (("2" (EXPAND "comp_struct" -1) (("2" (ASSERT) (("2" (REPLACE -1 * RL) (("2" (ASSERT) (("2" (ASSERT) (("2" (REPLACE -2 * RL) (("2" (ASSERT) (("2" (REPLACE -3 * RL) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|comp_cons| "" (SKOSIMP*) (("" (CASE "next(comp(cons_seq(a!1, x!1), y!1)) = next(cons_seq(a!1, comp(x!1, y!1)))") (("1" (LEMMA "next_iso[A]") (("1" (PROP) (("1" (INST-CP -2 "comp(cons_seq(a!1, x!1), y!1)") (("1" (INST -2 "cons_seq(a!1, comp(x!1, y!1))") (("1" (ASSERT) NIL))))))))) ("2" (HIDE 2) (("2" (EXPAND "comp") (("2" (REWRITE "next_cons") (("2" (REWRITE "next") (("2" (NAME "ape" "coreduce(comp_struct)") (("2" (REPLACE -1) (("2" (EXPAND "comp_struct" 1) (("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))))))))))))))))))) (|comp_cons_list| "" (INDUCT "l") (("1" (SKOSIMP*) (("1" (EXPAND "cons_list") (("1" (PROPAX) NIL))))) ("2" (SKOSIMP*) (("2" (EXPAND "cons_list" 1) (("2" (REWRITE "comp_cons") (("2" (GRIND) NIL))))))))) (|comp_list| "" (SKOSIMP*) (("" (LEMMA "list_incl_list[A]") (("" (INST?) (("" (REPLACE -1) (("" (REWRITE "comp_cons_list") (("" (REWRITE "comp_empty1") NIL))))))))))) (|comp_append| "" (INDUCT "l") (("1" (SKOSIMP*) (("1" (REWRITE "list_incl_null") (("1" (REWRITE "comp_empty1") (("1" (EXPAND "append") (("1" (PROPAX) NIL))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "append" 1) (("2" (REWRITE "list_incl_cons") (("2" (REWRITE "list_incl_cons") (("2" (REWRITE "comp_cons") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))) (|infinite_comp1| "" (LEMMA "final_bisim_finality[A]") (("" (INST -1 "LAMBDA(u,v:Seq[A]) : infinite?(v) AND EXISTS(w:Seq[A]) : u = comp(v,w)") (("" (ASSERT) (("" (PROP) (("1" (SKOSIMP*) (("1" (INST -1 "comp(x!1,y!1)" "x!1") (("1" (ASSERT) (("1" (INST?) NIL))))))) ("2" (HIDE 2) (("2" (EXPAND "bisimulation?") (("2" (SKOSIMP*) (("2" (REPLACE -2) (("2" (HIDE -2) (("2" (CASE "bot?(next(x2!1))") (("1" (ASSERT) (("1" (LEMMA "empty_unique[A]") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1 -2 1) (("1" (LEMMA "fin_inf[A]") (("1" (INST?) (("1" (EXPAND "XOR") (("1" (HIDE -2) (("1" (EXPAND "finite?") (("1" (SKOSIMP*) (("1" (GROUND) (("1" (INST + "null") (("1" (REWRITE "list_incl_null") NIL))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (EXPAND "comp" 2 1) (("2" (EXPAND "comp" 2 1) (("2" (REWRITE "next") (("2" (EXPAND "comp_struct") (("2" (EXPAND "infinite?") (("2" (SKOSIMP*) (("2" (PROP) (("1" (INST 1 "LAMBDA(n:nat) : f!1(n+1)") (("1" (EXPAND "inf_incl") (("1" (REPLACE -1 * RL) (("1" (REWRITE "next") (("1" (ASSERT) (("1" (EXPAND "inf_incl_struct") (("1" (PROPAX) NIL))))))))))))) ("2" (INST 1 "w!1") (("2" (LEMMA "not_bot_next[A]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (REWRITE "next_cons") (("2" (REWRITE "comp_cons") (("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|infinite_comp2| "" (SKOSIMP*) (("" (CASE "infinite?(x!1)") (("1" (LEMMA "infinite_comp1") (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (LEMMA "fin_inf[A]") (("2" (INST?) (("2" (ASSERT) (("2" (EXPAND "XOR") (("2" (PROP) (("2" (IFF) (("2" (ASSERT) (("2" (HIDE 1) (("2" (EXPAND "finite?") (("2" (SKOSIMP*) (("2" (REPLACE -1 1 RL) (("2" (HIDE -1) (("2" (REWRITE "comp_list") (("2" (LEMMA "infinite_list[A]") (("2" (INST?) (("2" (ASSERT) (("2" (INST?) NIL))))))))))))))))))))))))))))))))))))) (|finite_comp| "" (SKOSIMP*) (("" (LEMMA "fin_inf[A]") (("" (INST-CP -1 "x!1") (("" (INST-CP -1 "y!1") (("" (INST -1 "comp(x!1, y!1)") (("" (EXPAND "XOR") (("" (PROP) (("1" (IFF) (("1" (ASSERT) (("1" (LEMMA "infinite_comp1") (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (IFF) (("2" (ASSERT) (("2" (LEMMA "infinite_comp2") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))) (|comp_at_tail| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at_up_to") (("1" (EXPAND "tail") (("1" (REWRITE "list_incl_null") (("1" (REWRITE "comp_empty1") NIL))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "at_up_to" 1) (("2" (EXPAND "tail" 1) (("2" (CASE "bot?(next(x!1))") (("1" (ASSERT) (("1" (REWRITE "list_incl_null") (("1" (REWRITE "comp_empty1") (("1" (LEMMA "empty_unique[A]") (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (ASSERT) (("2" (REWRITE "list_incl_cons") (("2" (REWRITE "comp_cons") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (REPLACE -1) (("2" (LEMMA "not_bot_next[A]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))(|PrefixOrd| (|prefix_refl| "" (EXPAND "reflexive?") (("" (SKOSIMP*) (("" (EXPAND "prefix") (("" (INST 1 "empty_seq") (("" (REWRITE "comp_empty2") NIL))))))))) (|prefix_trans| "" (EXPAND "transitive?") (("" (SKOSIMP*) (("" (EXPAND "prefix") (("" (SKOSIMP*) (("" (INST 1 "comp(z!2,z!3)") (("" (REWRITE "comp_assoc") (("" (ASSERT) NIL))))))))))))) (|prefix_antisym| "" (LEMMA "final_bisim_finality[A]") (("" (INST -1 "LAMBDA(x,y:Seq[A]) : prefix(x,y) AND prefix(y,x)") (("" (ASSERT) (("" (PROP) (("1" (EXPAND "antisymmetric?") (("1" (PROPAX) NIL))) ("2" (HIDE 2) (("2" (EXPAND "bisimulation?") (("2" (SKOSIMP*) (("2" (EXPAND "prefix") (("2" (SKOSIMP*) (("2" (CASE "bot?(next(x1!1))") (("1" (ASSERT) (("1" (LEMMA "empty_unique[A]") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1 -2 -3) (("1" (PROP) (("1" (LEMMA "not_bot_next[A]") (("1" (INST?) (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (REPLACE -1) (("1" (REWRITE "comp_cons") (("1" (CASE "bot?(next[A](empty_seq))") (("1" (REPLACE -3 -1 RL) (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))) ("2" (REWRITE "next_empty") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (CASE "bot?(next(x2!1))") (("1" (HIDE 2) (("1" (LEMMA "empty_unique[A]") (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1 -2 -4) (("1" (LEMMA "not_bot_next[A]") (("1" (INST?) (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (REPLACE -1) (("1" (REWRITE "comp_cons") (("1" (CASE "bot?(next[A](empty_seq))") (("1" (REPLACE -3 -1 RL) (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))) ("2" (REWRITE "next_empty") (("2" (ASSERT) NIL))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (LEMMA "not_bot_next[A]") (("2" (INST-CP -1 "x2!1") (("2" (INST -1 "x1!1") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (REPLACE -2) (("2" (HIDE -1 -2) (("2" (REWRITE "next_cons") (("2" (REWRITE "next_cons") (("2" (HIDE 1 2) (("2" (REWRITE "comp_cons") (("2" (REWRITE "comp_cons") (("2" (CASE "next(cons_seq(a!1, comp(y!1, z!1))) = next(cons_seq(a!2, y!2))") (("1" (CASE "next(cons_seq(a!2, comp(y!2, z!2))) = next(cons_seq(a!1, y!1))") (("1" (REWRITE "next_cons") (("1" (REWRITE "next_cons") (("1" (REWRITE "next_cons") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (LEMMA "mono_up[[A,Seq[A]]]") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE -2) (("1" (LEMMA "mono_up[[A,Seq[A]]]") (("1" (INST?) (("1" (ASSERT) (("1" (PROP) (("1" (INST?) NIL) ("2" (INST?) NIL))))))))))))))))))))))))))) ("2" (ASSERT) NIL))) ("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|prefix_poset| "" (EXPAND "partial_order?") (("" (PROP) (("1" (EXPAND "preorder?") (("1" (PROP) (("1" (LEMMA "prefix_refl") (("1" (PROPAX) NIL))) ("2" (LEMMA "prefix_trans") (("2" (PROPAX) NIL))))))) ("2" (LEMMA "prefix_antisym") (("2" (PROPAX) NIL))))))) (|prefix_empty| "" (SKOSIMP*) (("" (EXPAND "prefix") (("" (INST 1 "x!1") (("" (REWRITE "comp_empty1") NIL))))))) (|prefix_at_up_to| "" (SKOSIMP*) (("" (EXPAND "prefix") (("" (LEMMA "comp_at_tail[A]") (("" (INST?) (("" (INST?) NIL))))))))) (|prefix_infinite| "" (SKOSIMP*) (("" (LEMMA "infinite_comp1[A]") (("" (INST?) (("" (EXPAND "prefix") (("" (SKOSIMP*) (("" (INST?) (("" (ASSERT) NIL))))))))))))) (|prefix_finite| "" (SKOSIMP*) (("" (LEMMA "fin_inf[A]") (("" (INST-CP -1 "x!1") (("" (INST -1 "y!1") (("" (EXPAND "XOR") (("" (PROP) (("" (IFF) (("" (ASSERT) (("" (LEMMA "prefix_infinite") (("" (INST?) (("" (ASSERT) NIL))))))))))))))))))))) (|prefix_tail| "" (SKOLEM!) (("" (PROP) (("" (INDUCT "n") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "prefix") (("2" (SKOSIMP*) (("2" (LEMMA "cons_at_tail[A]") (("2" (INST -1 "tail(x!1,j!1)") (("2" (REWRITE "at_tail") (("2" (CASE "bot?(at(x!1, j!1))") (("1" (ASSERT) (("1" (LEMMA "at_bot_tail[A]") (("1" (INST?) (("1" (ASSERT) (("1" (LEMMA "tail_tail[A]") (("1" (INST -1 "x!1" "j!1" "1") (("1" (REPLACE -2 -1) (("1" (REWRITE "tail_empty") (("1" (REPLACE -1 1 RL) (("1" (INST 1 "tail(y!1, 1 + j!1)") (("1" (REWRITE "comp_empty1") NIL))))))))))))))))))))) ("2" (ASSERT) (("2" (REPLACE -1 -2) (("2" (REWRITE "comp_cons") (("2" (REWRITE "tail_tail") (("2" (CASE "next(cons_seq(down(at(x!1, j!1)), comp(tail(x!1, 1 + j!1), z!1))) = next(tail(y!1, j!1))") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (LEMMA "tail_tail[A]") (("1" (INST -1 "y!1" "j!1" "1") (("1" (REPLACE -1 * RL) (("1" (EXPAND "tail" 2 2) (("1" (EXPAND "tail" 2 2) (("1" (REPLACE -2 2 RL) (("1" (ASSERT) (("1" (INST?) NIL))))))))))))))))))) ("2" (ASSERT) NIL))))))))))))))))))))))))))))))) (|prefix_simulation| "" (SKOSIMP*) (("" (PROP) (("1" (INST 1 "prefix") (("1" (PROP) (("1" (HIDE -1) (("1" (EXPAND "simulation?") (("1" (SKOSIMP*) (("1" (EXPAND "prefix") (("1" (SKOSIMP*) (("1" (LEMMA "not_bot_next[A]") (("1" (INST?) (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (REPLACE -1) (("1" (REWRITE "comp_cons") (("1" (REPLACE -2 * RL) (("1" (REWRITE "next_cons") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (INST?) NIL))))))))))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "simulation?") (("2" (EXPAND "prefix") (("2" (LEMMA "fin_inf[A]") (("2" (INST -1 "x!1") (("2" (EXPAND "XOR") (("2" (PROP) (("2" (IFF) (("2" (PROP) (("1" (EXPAND "finite?") (("1" (SKOSIMP*) (("1" (REPLACE -1 * RL) (("1" (INST 2 "tail(y!1,length(l!1))") (("1" (CASE "at_up_to(y!1,length(l!1)) = l!1") (("1" (LEMMA "comp_at_tail[A]") (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (HIDE -1 2 3) (("2" (CASE "FORALL(l:list[A],y:Seq[A]) : R!1(list_incl(l),y) IMPLIES at_up_to(y, length(l)) = l") (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (HIDE 2) (("2" (INDUCT "l") (("1" (SKOSIMP*) (("1" (EXPAND "length") (("1" (EXPAND "at_up_to") (("1" (PROPAX) NIL))))))) ("2" (SKOSIMP*) (("2" (REWRITE "list_incl_cons") (("2" (INST -3 "cons_seq(cons1_var!1, list_incl(cons2_var!1))" "y!2") (("2" (ASSERT) (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (PROP) (("2" (INST?) (("2" (ASSERT) (("2" (EXPAND "length" 1) (("2" (EXPAND "at_up_to" 1) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))) ("2" (HIDE 1) (("2" (EXPAND "infinite?") (("2" (SKOSIMP*) (("2" (REPLACE -1 * RL) (("2" (HIDE -1) (("2" (INST 1 "empty_seq") (("2" (REWRITE "comp_empty2") (("2" (LEMMA "final_bisim_finality[A]") (("2" (INST -1 "LAMBDA(x,y:Seq[A]) : R!1(x,y) AND infinite?(x)") (("2" (ASSERT) (("2" (PROP) (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "infinite?") (("1" (INST?) NIL))))))) ("2" (HIDE -2 2) (("2" (EXPAND "bisimulation?") (("2" (SKOSIMP*) (("2" (EXPAND "infinite?") (("2" (SKOSIMP*) (("2" (REPLACE -2 * RL) (("2" (INST?) (("2" (ASSERT) (("2" (HIDE -1 -2) (("2" (EXPAND "inf_incl") (("2" (REWRITE "next") (("2" (EXPAND "inf_incl_struct") (("2" (ASSERT) (("2" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (INST 1 "(LAMBDA (n: nat): f!2(1 + n))") NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|prefix_at| "" (SKOSIMP*) (("" (PROP) (("1" (LEMMA "fin_inf[A]") (("1" (INST?) (("1" (EXPAND "XOR") (("1" (FLATTEN -1) (("1" (IFF) (("1" (CASE "finite?(x!1)") (("1" (HIDE 1) (("1" (EXPAND "finite?") (("1" (SKOSIMP*) (("1" (REPLACE -1 * RL) (("1" (EXPAND "prefix") (("1" (SKOSIMP*) (("1" (REWRITE "comp_list") (("1" (REPLACE -2 * RL) (("1" (REWRITE "at_cons_list") (("1" (CASE "n!1 < length(l!1)") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (REWRITE "list_incl_list") (("2" (REWRITE "at_cons_list") (("2" (REWRITE "at_empty") (("2" (ASSERT) NIL))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (HIDE 1) (("2" (EXPAND "prefix") (("2" (SKOSIMP*) (("2" (LEMMA "infinite_comp1[A]") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))) ("2" (LEMMA "prefix_simulation") (("2" (INST?) (("2" (PROP) (("2" (HIDE 2) (("2" (INST 1 "LAMBDA(x,y:Seq[A]) : FORALL (n: nat): up?(at(x, n)) IMPLIES (up?(at(y, n)) AND down(at(x, n)) = down(at(y, n)))") (("2" (ASSERT) (("2" (PROP) (("2" (HIDE -1 2) (("2" (EXPAND "simulation?") (("2" (SKOSIMP*) (("2" (INST-CP -1 "0") (("2" (EXPAND "at" -2) (("2" (ASSERT) (("2" (FLATTEN -2) (("2" (LIFT-IF) (("2" (ASSERT) (("2" (CASE "bot?(next(y!2))") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (SKOSIMP*) (("2" (INST -1 "n!1+1") (("2" (EXPAND "at" -1) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))) (|consistent_prefix| "" (SKOSIMP*) (("" (LEMMA "fin_inf[A]") (("" (INST-CP -1 "x!1") (("" (INST -1 "y!1") (("" (EXPAND "XOR") (("" (PROP) (("" (IFF) (("" (ASSERT) (("" (CASE "infinite?(x!1)") (("1" (LEMMA "prefix_infinite") (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (CASE "infinite?(y!1)") (("1" (LEMMA "prefix_infinite") (("1" (INST -1 "y!1" "z!1") (("1" (ASSERT) NIL))))) ("2" (ASSERT) (("2" (EXPAND "finite?") (("2" (SKOSIMP*) (("2" (CASE "length(l!1) <= length(l!2)") (("1" (HIDE 1 2 4) (("1" (EXPAND "prefix") (("1" (SKOSIMP*) (("1" (LEMMA "comp_at_tail[A]") (("1" (REPLACE -3 * RL) (("1" (REPLACE -4 * RL) (("1" (HIDE -3 -4) (("1" (INST -1 "list_incl(l!2)" "length(l!1)") (("1" (REPLACE -1 -3 RL) (("1" (LEMMA "comp_assoc[A]") (("1" (INST?) (("1" (REPLACE -1 -4 RL) (("1" (HIDE -1) (("1" (REWRITE "comp_list") (("1" (REWRITE "comp_list") (("1" (REWRITE "comp_list") (("1" (REPLACE -3 -4 RL) (("1" (HIDE -3) (("1" (LEMMA "cons_list_mono[A]") (("1" (INST?) (("1" (CASE "length(at_up_to(list_incl(l!2), length(l!1))) = length(l!1)") (("1" (ASSERT) (("1" (REPLACE -2 -3 RL) (("1" (REVEAL 3) (("1" (HIDE 2) (("1" (EXPAND "prefix") (("1" (REVEAL -6 -7) (("1" (REPLACE -1 * RL) (("1" (REPLACE -2 * RL) (("1" (HIDE -1 -2) (("1" (INST 1 "tail(list_incl(l!2), length(l!1))") (("1" (REWRITE "comp_list") NIL))))))))))))))))))))) ("2" (HIDE -1 2) (("2" (LEMMA "length_at_up_to[A]") (("2" (INST?) (("2" (ASSERT) (("2" (PROP) (("2" (LEMMA "at_list_incl_up[A]") (("2" (INST -1 "l!2" "length(l!1) - 1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (REPLACE -1 * RL) (("2" (REPLACE -2 * RL) (("2" (HIDE -1 -2 2 3 5) (("2" (EXPAND "prefix") (("2" (SKOSIMP*) (("2" (LEMMA "comp_at_tail[A]") (("2" (INST -1 "list_incl(l!1)" "length(l!2)") (("2" (REPLACE -1 -3 RL) (("2" (HIDE -1) (("2" (LEMMA "comp_assoc[A]") (("2" (INST?) (("2" (REPLACE -1 -3 RL) (("2" (HIDE -1) (("2" (REWRITE "comp_list") (("2" (REWRITE "comp_list") (("2" (REPLACE -1 -2 RL) (("2" (HIDE -1) (("2" (LEMMA "cons_list_mono[A]") (("2" (INST?) (("2" (ASSERT) (("2" (CASE "length(at_up_to(list_incl(l!1), length(l!2))) = length(l!2)") (("1" (ASSERT) (("1" (REVEAL -5) (("1" (REPLACE -3 -1) (("1" (INST?) NIL))))))) ("2" (HIDE -1 3) (("2" (LEMMA "length_at_up_to[A]") (("2" (INST?) (("2" (PROP) (("2" (LEMMA "at_list_incl_up[A]") (("2" (INST -1 "l!1" "length(l!2) -1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))(|Ascending_chains| (|achains_asc| "" (CASE "FORALL (f: (AChains?), n, m: nat) : f(n) <= f(n+m)") (("1" (SKOSIMP*) (("1" (INST -1 "f!1" "n!1" "m!1-n!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))) ("2" (HIDE 2) (("2" (INDUCT "m") (("1" (SKOSIMP*) (("1" (ASSERT) (("1" (LEMMA "poset") (("1" (EXPAND "partial_order?") (("1" (EXPAND "preorder?") (("1" (PROP) (("1" (EXPAND "reflexive?") (("1" (INST?) NIL))))))))))))))) ("2" (SKOSIMP*) (("2" (INST?) (("2" (TYPEPRED "f!1") (("2" (EXPAND "AChains?") (("2" (INST -1 "n!1 + j!1") (("2" (LEMMA "poset") (("2" (EXPAND "partial_order?") (("2" (EXPAND "preorder?") (("2" (EXPAND "transitive?") (("2" (PROP) (("2" (INST -2 "f!1(n!1)" "f!1(n!1 + j!1)" "f!1(n!1 + (j!1 + 1))") (("2" (ASSERT) NIL))))))))))))))))))))))))))))) (|least_upperbound_unique| "" (SKOSIMP*) (("" (EXPAND "least_upperbound?") (("" (PROP) (("" (INST -2 "y!1") (("" (INST -4 "x!1") (("" (ASSERT) (("" (LEMMA "poset") (("" (EXPAND "partial_order?") (("" (PROP) (("" (EXPAND "antisymmetric?") (("" (INST?) (("" (ASSERT) NIL))))))))))))))))))))))))(|Seq_alg_cpo| (|achain_tail_TCC1| "" (SKOSIMP*) (("" (LEMMA "prefix_poset[A]") (("" (PROPAX) NIL))))) (|achain_tail| "" (SKOSIMP*) (("" (EXPAND "AChains?") (("" (SKOSIMP*) (("" (TYPEPRED "f!1") (("" (EXPAND "AChains?") (("" (INST?) (("" (LEMMA "prefix_tail[A]") (("" (INST?) (("" (ASSERT) (("" (INST?) NIL))))))))))))))))))) (|seq_achains_asc_TCC1| "" (SUBTYPE-TCC) NIL) (|seq_achains_asc| "" (SKOSIMP*) (("" (LEMMA "achains_asc[Seq[A],prefix[A]]") (("" (INST?) (("" (INST -1 "m!1") (("" (ASSERT) (("" (LEMMA "prefix_at[A]") (("" (INST?) (("" (ASSERT) (("" (INST -1 "k!1") (("" (ASSERT) NIL))))))))))))))))))) (|lub_struct_TCC1| "" (SUBTYPE-TCC) NIL) (|lub_struct_TCC2| "" (SUBTYPE-TCC) NIL) (|lub_struct_TCC3| "" (SKOSIMP*) (("" (LEMMA "achain_tail") (("" (INST?) NIL))))) (|tail_cont_TCC1| "" (SKOSIMP*) (("" (LEMMA "achain_tail") (("" (INST?) NIL))))) (|tail_cont| "" (INDUCT "m") (("1" (EXPAND "tail") (("1" (SKOSIMP*) (("1" (ASSERT) (("1" (CASE "f!1 = LAMBDA (n: nat): f!1(n)") (("1" (REPLACE -1 1 RL) (("1" (PROPAX) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))) ("2" (SKOSIMP*) (("2" (CASE "next(tail(lub(f!1), j!1)) = next(lub(LAMBDA (n: nat): tail(f!1(n), j!1)))") (("1" (EXPAND "lub" -1 2) (("1" (LEMMA "next[A,(AChains?[Seq[A],prefix[A]])]") (("1" (INST -1 "lub_struct" "LAMBDA (n: nat): tail(f!1(n), j!1)") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (CASE "bot?(lub_struct(LAMBDA (n: nat): tail(f!1(n), j!1)))") (("1" (ASSERT) (("1" (EXPAND "lub_struct") (("1" (CASE "FORALL (n: nat): bot?(next(tail(f!1(n), j!1)))") (("1" (LIFT-IF -2) (("1" (PROP) (("1" (HIDE -1) (("1" (HIDE -1) (("1" (LEMMA "tail_tail[A]") (("1" (LEMMA "empty_unique[A]") (("1" (INST?) (("1" (ASSERT) (("1" (INST -2 "lub(f!1)" "j!1" "1") (("1" (REPLACE -1) (("1" (REWRITE "tail_empty") (("1" (REPLACE -2 1 RL) (("1" (CASE "bot?(next(lub(LAMBDA (n: nat): tail(f!1(n), 1 + j!1))))") (("1" (LEMMA "empty_unique[A]") (("1" (INST -1 "lub(LAMBDA (n: nat): tail(f!1(n), 1 + j!1))") (("1" (ASSERT) NIL) ("2" (LEMMA "achain_tail") (("2" (INST?) NIL))))))) ("2" (HIDE 2) (("2" (EXPAND "lub" 1) (("2" (LEMMA "next[A,(AChains?[Seq[A],prefix[A]])]") (("2" (INST -1 "lub_struct" "LAMBDA (n: nat): tail(f!1(n), 1+j!1)") (("1" (CASE "bot?(lub_struct(LAMBDA (n: nat): tail(f!1(n), 1 + j!1)))") (("1" (ASSERT) NIL) ("2" (HIDE -1 2) (("2" (EXPAND "lub_struct") (("2" (CASE "FORALL (n: nat): bot?(next(tail(f!1(n), 1 + j!1)))") (("1" (ASSERT) (("1" (LIFT-IF 1) (("1" (PROP) (("1" (ASSERT) NIL))))))) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (INST -3 "n!1") (("2" (LEMMA "empty_unique[A]") (("2" (INST -1 "tail(f!1(n!1), j!1)") (("2" (ASSERT) (("2" (LEMMA "tail_tail[A]") (("2" (INST -1 "f!1(n!1)" "j!1" "1") (("2" (REPLACE -2) (("2" (REWRITE "tail_empty") (("2" (REPLACE -1 * RL) (("2" (PROPAX) NIL))))))))))))))))))))))))))))))) ("2" (LEMMA "achain_tail") (("2" (INST?) NIL))))))))))) ("3" (LEMMA "achain_tail") (("3" (INST?) NIL))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (LIFT-IF -1) (("2" (PROP) (("2" (ASSERT) NIL))))))))))))) ("2" (ASSERT) (("2" (LEMMA "tail_tail[A]") (("2" (INST -1 "lub(f!1)" "j!1" "1") (("2" (EXPAND "tail" -1 1) (("2" (EXPAND "tail" -1 1) (("2" (REPLACE -2) (("2" (ASSERT) (("2" (HIDE -2) (("2" (EXPAND "lub_struct" -1 2) (("2" (CASE "FORALL (n: nat): bot?(next(tail(f!1(n), j!1)))") (("1" (HIDE -2) (("1" (EXPAND "lub_struct") (("1" (ASSERT) (("1" (LIFT-IF 1) (("1" (PROP) (("1" (ASSERT) NIL))))))))))) ("2" (ASSERT) (("2" (LIFT-IF -1) (("2" (PROP) (("2" (HIDE 1) (("2" (NAME "ape" "LAMBDA (n: nat): tail(tail(f!1(n), j!1), 1)") (("2" (REPLACE -1) (("2" (CASE "ape = LAMBDA (n: nat): tail(f!1(n), 1 + j!1)") (("1" (REPLACE -1 3 RL) (("1" (ASSERT) (("1" (EXPAND "lub") (("1" (ASSERT) NIL))))))) ("2" (HIDE -2 -3 2 3 4) (("2" (REPLACE -1 1 RL) (("2" (HIDE -1) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (LEMMA "tail_tail[A]") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (LEMMA "achain_tail") (("2" (INST?) NIL))))))))) ("2" (ASSERT) (("2" (INST -1 "f!1") (("2" (ASSERT) NIL))))) ("3" (LEMMA "achain_tail") (("3" (INST?) NIL))))))) ("3" (SKOSIMP*) (("3" (LEMMA "achain_tail") (("3" (INST?) NIL))))))) (|seq_lub| "" (SKOSIMP*) (("" (EXPAND "least_upperbound?") (("" (PROP) (("1" (EXPAND "upperbound?") (("1" (SKOSIMP*) (("1" (LEMMA "prefix_simulation[A]") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE 2) (("1" (INST 1 "LAMBDA(x,y:Seq[A]) : EXISTS(m:nat) : x = tail(f!1(n!1),m) AND y = tail(lub(f!1),m)") (("1" (ASSERT) (("1" (PROP) (("1" (EXPAND "simulation?") (("1" (SKOSIMP*) (("1" (REPLACE -1) (("1" (REPLACE -2) (("1" (HIDE -1 -2) (("1" (LEMMA "tail_cont") (("1" (INST?) (("1" (REPLACE -1) (("1" (NAME "ape" "next(lub(LAMBDA (n: nat): tail(f!1(n), m!1)))") (("1" (REPLACE -1) (("1" (EXPAND "lub" -1) (("1" (LEMMA "next[A,(AChains?[Seq[A],prefix[A]])]") (("1" (INST -1 "lub_struct" "LAMBDA (n: nat): tail(f!1(n), m!1)") (("1" (CASE "bot?(lub_struct(LAMBDA (n: nat): tail(f!1(n), m!1)))") (("1" (HIDE -2) (("1" (HIDE -2) (("1" (EXPAND "lub_struct") (("1" (CASE "FORALL (n: nat): bot?(next(tail(f!1(n), m!1)))") (("1" (HIDE -2) (("1" (INST -1 "n!1") (("1" (ASSERT) NIL))))) ("2" (LIFT-IF -1) (("2" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL))))))))))))) ("2" (ASSERT) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (EXPAND "lub_struct" -1 1) (("2" (EXPAND "lub_struct" -1 2) (("2" (CASE "FORALL (n: nat): bot?(next(tail(f!1(n), m!1)))") (("1" (HIDE -2) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (ASSERT) (("2" (NAME "l" "least({n: nat | NOT bot? (next(tail(f!1(n), m!1)))})") (("1" (REPLACE -1) (("1" (TYPEPRED "l") (("1" (INST -1 "n!1") (("1" (ASSERT) (("1" (LEMMA "achains_asc[Seq[A],prefix[A]]") (("1" (INST?) (("1" (INST -1 "n!1") (("1" (ASSERT) (("1" (LEMMA "prefix_tail[A]") (("1" (INST?) (("1" (ASSERT) (("1" (INST -1 "m!1") (("1" (LIFT-IF -5) (("1" (PROP) (("1" (HIDE 2) (("1" (REPLACE -1 * RL) (("1" (ASSERT) (("1" (HIDE -1) (("1" (LEMMA "prefix_at[A]") (("1" (INST?) (("1" (ASSERT) (("1" (INST -1 "0") (("1" (EXPAND "at" -1) (("1" (PROPAX) NIL))))))))))))))))))) ("2" (HIDE 2) (("2" (REPLACE -1 * RL) (("2" (ASSERT) (("2" (HIDE -1) (("2" (INST 1 "m!1+1") (("2" (PROP) (("1" (LEMMA "tail_tail[A]") (("1" (INST -1 "f!1(n!1)" "m!1" "1") (("1" (REPLACE -1 1 RL) (("1" (EXPAND "tail" 1 2) (("1" (EXPAND "tail" 1 2) (("1" (PROPAX) NIL))))))))))) ("2" (NAME "dog" "LAMBDA (n: nat): tail(tail(f!1(n), m!1), 1)") (("2" (REPLACE -1) (("2" (CASE "dog = LAMBDA(n:nat) : tail(f!1(n),m!1+1)") (("1" (REPLACE -1 1) (("1" (LEMMA "tail_cont") (("1" (INST -1 "f!1" "m!1+1") (("1" (EXPAND "lub") (("1" (ASSERT) NIL))))))))) ("2" (REPLACE -1 1 RL) (("2" (HIDE -1 -2 -3 -4 -5 -6 -7 2 3 4 5) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (LEMMA "tail_tail[A]") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (HIDE -1) (("2" (EXPAND "nonempty?") (("2" (EXPAND "empty?") (("2" (EXPAND "member") (("2" (PROPAX) NIL))))))))))))))))))))))))))) ("2" (LEMMA "achain_tail") (("2" (INST?) NIL))))))))))) ("2" (LEMMA "achain_tail") (("2" (INST?) NIL))))))))))))))))))))) ("2" (INST 1 "0") (("2" (EXPAND "tail") (("2" (PROPAX) NIL))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "upperbound?") (("2" (LEMMA "prefix_simulation[A]") (("2" (INST?) (("2" (PROP) (("2" (INST 1 " LAMBDA(x,y:Seq[A]) : EXISTS(m:nat) : x = lub(LAMBDA(n:nat) : tail(f!1(n),m)) AND y = tail(y!1,m)") (("1" (ASSERT) (("1" (PROP) (("1" (HIDE 2 3) (("1" (EXPAND "simulation?") (("1" (SKOSIMP*) (("1" (REPLACE -1) (("1" (REPLACE -2) (("1" (HIDE -1 -2) (("1" (NAME "cow" "next(lub(LAMBDA (n: nat): tail(f!1(n), m!1)))") (("1" (REPLACE -1) (("1" (EXPAND "lub" -1) (("1" (LEMMA "next[A,(AChains?[Seq[A],prefix[A]])]") (("1" (INST?) (("1" (REPLACE -1 -2) (("1" (HIDE -1) (("1" (CASE "bot?(lub_struct(LAMBDA (n: nat): tail(f!1(n), m!1)))") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (EXPAND "lub_struct" -1 1) (("2" (EXPAND "lub_struct" -1 2) (("2" (NAME "le" "least({n: nat | NOT bot? (next(tail(f!1(n), m!1)))})") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (TYPEPRED "le") (("1" (EXPAND "lub_struct" 2) (("1" (CASE "FORALL (n: nat): bot?(next(tail(f!1(n), m!1)))") (("1" (ASSERT) (("1" (LIFT-IF 2) (("1" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL))))))) ("2" (HIDE 3) (("2" (ASSERT) (("2" (INST -4 "le") (("2" (LEMMA "prefix_tail[A]") (("2" (INST?) (("2" (ASSERT) (("2" (INST -1 "m!1") (("2" (LEMMA "prefix_at[A]") (("2" (INST?) (("2" (ASSERT) (("2" (INST -1 "0") (("2" (EXPAND "at" -1) (("2" (ASSERT) (("2" (CASE "bot?(next(tail(y!1, m!1)))") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (LIFT-IF) (("2" (PROP) (("1" (REPLACE -1 1 RL) (("1" (ASSERT) NIL))) ("2" (INST 1 "m!1+1") (("2" (REPLACE -1 1 RL) (("2" (ASSERT) (("2" (HIDE -1) (("2" (PROP) (("1" (HIDE -1 -2 -3 -4 -5 2 3 4 5) (("1" (NAME "bird" "LAMBDA (n: nat): tail(tail(f!1(n), m!1), 1)") (("1" (REPLACE -1) (("1" (CASE "bird = LAMBDA (n: nat): tail(f!1(n), 1 + m!1)") (("1" (ASSERT) (("1" (REPLACE -1 1) (("1" (EXPAND "lub") (("1" (PROPAX) NIL))))))) ("2" (REPLACE -1 1 RL) (("2" (HIDE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (LEMMA "tail_tail[A]") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))) ("2" (LEMMA "tail_tail[A]") (("2" (INST -1 "y!1" "m!1" "1") (("2" (REPLACE -1 1 RL) (("2" (EXPAND "tail" 1 2) (("2" (EXPAND "tail" 1 2) (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (HIDE -1) (("2" (EXPAND "nonempty?") (("2" (EXPAND "empty?") (("2" (EXPAND "member") (("2" (EXPAND "lub_struct" 1) (("2" (ASSERT) (("2" (LIFT-IF 1) (("2" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL))))))))))))))))))))))))))))))) ("2" (LEMMA "achain_tail") (("2" (INST?) NIL))))))))))) ("2" (LEMMA "achain_tail") (("2" (INST?) NIL))))))))))))))))) ("2" (INST 1 "0") (("2" (EXPAND "tail") (("2" (CASE "f!1 = LAMBDA (n: nat): f!1(n)") (("1" (REPLACE -1 1 RL) (("1" (PROPAX) NIL))) ("2" (HIDE -1 2 3 4) (("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))))) ("2" (SKOSIMP*) (("2" (LEMMA "achain_tail") (("2" (INST?) NIL))))))))))))))))))))))) (|at_lub| "" (SKOSIMP*) (("" (PROP) (("1" (REPLACE -1) (("1" (SKOSIMP*) (("1" (HIDE -1) (("1" (LEMMA "seq_lub") (("1" (INST?) (("1" (EXPAND "least_upperbound?") (("1" (PROP) (("1" (CASE "FORALL(m: nat): NOT at(f!1(m), n!1) = up(a!1)") (("1" (ASSERT) (("1" (HIDE 1) (("1" (CASE "FORALL(m: nat): bot?(at(f!1(m), n!1))") (("1" (HIDE -2) (("1" (LEMMA "at_tail[A]") (("1" (INST -1 "lub(f!1)" "n!1" "0") (("1" (ASSERT) (("1" (REPLACE -1 -3 RL) (("1" (HIDE -1) (("1" (LEMMA "tail_cont") (("1" (INST?) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (EXPAND "at" -2) (("1" (NAME "ape" "next(lub(LAMBDA (n: nat): tail(f!1(n), n!1)))") (("1" (REPLACE -1) (("1" (EXPAND "lub" -1) (("1" (LEMMA "next[A,(AChains?[Seq[A],prefix[A]])]") (("1" (INST?) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (CASE "bot?(lub_struct(LAMBDA (n: nat): tail(f!1(n), n!1)))") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (EXPAND "lub_struct" 1) (("2" (CASE "FORALL (n: nat): bot?(next(tail(f!1(n), n!1)))") (("1" (ASSERT) (("1" (LIFT-IF 1) (("1" (PROP) (("1" (ASSERT) NIL))))))) ("2" (HIDE -1 2) (("2" (SKOSIMP*) (("2" (LEMMA "at_tail[A]") (("2" (INST -2 "n!2") (("2" (INST -1 "f!1(n!2)" "n!1" "0") (("2" (ASSERT) (("2" (REPLACE -1 -2 RL) (("2" (EXPAND "at" -2) (("2" (PROPAX) NIL))))))))))))))))))))))))))))) ("2" (LEMMA "achain_tail") (("2" (INST?) NIL))))))))))) ("2" (LEMMA "achain_tail") (("2" (INST?) NIL))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (INST -1 "m!1") (("2" (HIDE -3) (("2" (EXPAND "upperbound?") (("2" (INST -2 "m!1") (("2" (LEMMA "prefix_at[A]") (("2" (INST?) (("2" (ASSERT) (("2" (INST -1 "n!1") (("2" (ASSERT) (("2" (CASE "at(lub(f!1), n!1) = up(down(at(lub(f!1), n!1)))") (("1" (REPLACE -1 -3) (("1" (LEMMA "mono_up[A]") (("1" (INST -1 "down(at(lub(f!1), n!1))" "a!1") (("1" (ASSERT) (("1" (REPLACE -3 -1 RL) (("1" (REPLACE -1 2 RL) (("1" (APPLY-EXTENSIONALITY 2 :HIDE? T) NIL))))))))))))) ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (INST?) NIL))))) ("2" (SKOSIMP*) (("2" (HIDE -3) (("2" (EXPAND "upperbound?") (("2" (INST?) (("2" (LEMMA "prefix_at[A]") (("2" (INST?) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (PROP) (("2" (ASSERT) (("2" (CASE "a!1=down(at(f!1(m!1), n!1))") (("1" (REPLACE -1 -3 RL) (("1" (REPLACE -3 1) (("1" (ASSERT) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))) ("2" (ASSERT) (("2" (CASE "at(f!1(m!1), n!1) = up(down(at(f!1(m!1), n!1)))") (("1" (REPLACE -1 -4) (("1" (LEMMA "mono_up[A]") (("1" (INST?) (("1" (ASSERT) NIL))))))) ("2" (ASSERT) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))))))))))))))))))))))))))))))))))))))))))) ("2" (CASE "least_upperbound?[Seq[A],prefix[A]](f!1)(y!1)") (("1" (LEMMA "least_upperbound_unique[Seq[A],prefix[A]]") (("1" (LEMMA "seq_lub") (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (HIDE 2) (("2" (LEMMA "prefix_at[A]") (("2" (EXPAND "least_upperbound?") (("2" (PROP) (("1" (EXPAND "upperbound?") (("1" (SKOSIMP*) (("1" (INST?) (("1" (PROP) (("1" (SKOSIMP*) (("1" (HIDE 2 3) (("1" (INST -2 "down(at(f!1(n!1), n!2))" "n!2") (("1" (CASE "EXISTS (m: nat): at(f!1(m), n!2) = up(down(at(f!1(n!1), n!2)))") (("1" (ASSERT) (("1" (PROP) (("1" (ASSERT) NIL) ("2" (HIDE -2) (("2" (SKOSIMP*) (("2" (ASSERT) (("2" (CASE "m!1 <= n!1 OR n!1 <= m!1") (("1" (LEMMA "seq_achains_asc") (("1" (PROP) (("1" (INST?) (("1" (INST -2 "m!1") (("1" (ASSERT) NIL))))) ("2" (INST -2 "f!1" "n!1" "m!1" "n!2") (("2" (ASSERT) NIL))))))) ("2" (PROP) (("2" (ASSERT) NIL))))))))))))))) ("2" (HIDE -2) (("2" (INST?) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))) ("3" (PROPAX) NIL))))))))))))))))) ("2" (SKOSIMP*) (("2" (INST -2 "y!1" "y!2") (("2" (CASE "(FORALL (n: nat): up?(at(y!1, n)) IMPLIES (up?(at(y!2, n)) AND down(at(y!1, n)) = down(at(y!2, n))))") (("1" (ASSERT) NIL) ("2" (HIDE -2 2) (("2" (SKOSIMP*) (("2" (EXPAND "upperbound?") (("2" (LEMMA "up_exist[A]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (HIDE -2) (("2" (INST -3 "x!1" "n!1") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (INST -2 "m!1") (("2" (LEMMA "prefix_at[A]") (("2" (INST?) (("2" (ASSERT) (("2" (INST -1 "n!1") (("2" (ASSERT) (("2" (PROP) (("2" (CASE "at(f!1(m!1), n!1) = up(down(at(f!1(m!1), n!1)))") (("1" (REPLACE -1 -6) (("1" (LEMMA "mono_up[A]") (("1" (INST -1 "down(at(f!1(m!1), n!1))" "x!1") (("1" (ASSERT) NIL))))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|at_up_to_achain| "" (SKOSIMP*) (("" (EXPAND "AChains?") (("" (SKOSIMP*) (("" (EXPAND "prefix") (("" (LEMMA "comp_at_tail[A]") (("" (INST -1 "list_incl[A](at_up_to[A](x!1, 1 + n!1))" "n!1") (("" (INST 1 "tail(list_incl[A](at_up_to[A](x!1, 1 + n!1)), n!1)") (("" (LEMMA "at_up_to_at_up_to[A]") (("" (INST?) (("" (ASSERT) (("" (EXPAND "min") (("" (ASSERT) NIL))))))))))))))))))))))) (|lub_at_up_to_TCC1| "" (SKOSIMP*) (("" (LEMMA "at_up_to_achain") (("" (INST?) NIL))))) (|lub_at_up_to| "" (SKOSIMP*) (("" (REWRITE "at_lub") (("1" (SKOSIMP*) (("1" (PROP) (("1" (INST 1 "n!1+1") (("1" (REWRITE "at_up_to_at") NIL))) ("2" (SKOSIMP*) (("2" (REWRITE "at_up_to_at") (("2" (LIFT-IF) (("2" (PROP) (("2" (ASSERT) NIL))))))))))))) ("2" (HIDE 2) (("2" (LEMMA "at_up_to_achain") (("2" (INST?) NIL))))))))) (|at_up_to_compact_TCC1| "" (SUBTYPE-TCC) NIL) (|at_up_to_compact| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "at_up_to") (("1" (REWRITE "list_incl_null") (("1" (REWRITE "prefix_empty") (("1" (INST 1 "0") (("1" (REWRITE "prefix_empty") NIL))))))))))) ("2" (SKOSIMP*) (("2" (INST?) (("2" (INST?) (("2" (CASE "prefix(list_incl(at_up_to(x!1, j!1)), lub(f!1))") (("1" (ASSERT) (("1" (LEMMA "at_up_to_at[A]") (("1" (INST -1 "x!1" "1+j!1" "j!1") (("1" (ASSERT) (("1" (LEMMA "prefix_at[A]") (("1" (INST -1 "list_incl(at_up_to(x!1, 1 + j!1))" "lub(f!1)") (("1" (ASSERT) (("1" (INST -1 "j!1") (("1" (CASE "bot?(at(x!1,j!1))") (("1" (PROPAX) NIL) ("2" (HIDE 1) (("2" (ASSERT) (("2" (LEMMA "up_exist[A]") (("2" (INST -1 "at(x!1, j!1)") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (REPLACE -1 -4) (("2" (CASE "at(list_incl(at_up_to(x!1, 1 + j!1)), j!1) = up(down(at(list_incl(at_up_to(x!1, 1 + j!1)), j!1)))") (("1" (LEMMA "mono_up[A]") (("1" (INST -1 "down(at(list_incl(at_up_to(x!1, 1 + j!1)), j!1))" "x!2") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (LEMMA "at_lub") (("1" (INST?) (("1" (INST -1 "lub(f!1)") (("1" (ASSERT) (("1" (CASE "at(lub(f!1),j!1) = up(x!2)") (("1" (HIDE -3 -6 -7) (("1" (INST?) (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (ASSERT) (("1" (CASE "j!1=0") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (EXPAND "at_up_to" 2) (("1" (EXPAND "at" -5) (("1" (ASSERT) (("1" (CASE "bot?(next(x!1))") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (EXPAND "at_up_to" 3) (("2" (REWRITE "list_incl_cons") (("2" (REWRITE "list_incl_null") (("2" (LEMMA "mono_up[A]") (("2" (INST?) (("2" (ASSERT) (("2" (REPLACE -1) (("2" (LEMMA "comp_at_tail[A]") (("2" (INST -1 "f!1(m!1)" "1") (("2" (EXPAND "at_up_to" -1) (("2" (EXPAND "at" -5) (("2" (CASE "bot?(next(f!1(m!1)))") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (EXPAND "at_up_to" -1) (("2" (REWRITE "list_incl_cons") (("2" (REWRITE "list_incl_null") (("2" (LEMMA "mono_up[A]") (("2" (INST -1 "PROJ_1(down(next(f!1(m!1))))" "x!2") (("2" (ASSERT) (("2" (REPLACE -1) (("2" (EXPAND "prefix") (("2" (INST?) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (CASE "bot?(at(x!1, j!1 - 1))") (("1" (ASSERT) (("1" (LEMMA "at_bot_tail[A]") (("1" (INST?) (("1" (ASSERT) (("1" (LEMMA "at_tail[A]") (("1" (INST -1 "x!1" "j!1-1" "1") (("1" (REPLACE -2) (("1" (REWRITE "at_empty") (("1" (ASSERT) NIL))))))))))))))))) ("2" (ASSERT) (("2" (SKOSIMP*) (("2" (NAME "m" "max(m!1,m!2)") (("2" (CASE "m!1 <= m") (("1" (CASE "m!2 <= m") (("1" (LEMMA "seq_achains_asc") (("1" (INST-CP -1 "f!1" "m!1" "m" "j!1") (("1" (ASSERT) (("1" (CASE "at(f!1(m!1), j!1) = up(down(at(f!1(m), j!1)))") (("1" (REPLACE -8 -1) (("1" (LEMMA "mono_up[A]") (("1" (INST -1 "x!2" "down(at(f!1(m), j!1))") (("1" (ASSERT) (("1" (HIDE -2) (("1" (INST 4 "m") (("1" (LEMMA "prefix_at[A]") (("1" (INST -1 "list_incl(at_up_to(x!1, 1 + j!1))" "f!1(m)") (("1" (ASSERT) (("1" (HIDE 5) (("1" (SKOSIMP*) (("1" (REWRITE "at_up_to_at") (("1" (CASE "n!1 < 1 + j!1") (("1" (ASSERT) (("1" (CASE "n!1 = j!1") (("1" (REPLACE -1) (("1" (HIDE -1 -2) (("1" (ASSERT) NIL))))) ("2" (CASE "n!1= 0)") (("1" (INST -1 "x!1") NIL) ("2" (HIDE 2) (("2" (INDUCT "n") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (INST -3 "j!1+1") (("2" (ASSERT) NIL))))))))))))))))) ("2" (INDUCT "n") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (INST -3 "j!1+1") (("2" (ASSERT) NIL))))))) ("3" (SKOSIMP*) (("3" (INST -2 "n!1+1") (("3" (ASSERT) NIL))))))))))))) ("3" (HIDE 2) (("3" (INDUCT "n") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (INST -4 "j!1+1") (("2" (ASSERT) NIL))))))))))))) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (INST -2 "n!1+1") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (SKOSIMP*) (("2" (HIDE 2) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))) (|cum_sum_TCC1| "" (SKOLEM!) (("" (PROP) (("" (HIDE 1) (("" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "j!1+1") (("2" (ASSERT) NIL))))))))))))))))))) (|cum_sum_TCC2| "" (SUBTYPE-TCC) NIL) (|cum_sum_TCC3| "" (SUBTYPE-TCC) NIL) (|cum_sum_TCC4| "" (TERMINATION-TCC) NIL) (|cum_sum_growth| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "cum_sum") (("1" (EXPAND "cum_sum") (("1" (TYPEPRED "g!1") (("1" (EXPAND "SAChain") (("1" (PROP) (("1" (INST -2 "0") (("1" (ASSERT) NIL))))))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "cum_sum" 1) (("2" (INST -1 "LAMBDA (x: nat): g!1(1 + x) - g!1(1)") (("1" (CASE "1 <= g!1(1)") (("1" (ASSERT) NIL) ("2" (HIDE -1 2) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "0") (("2" (ASSERT) NIL))))))))))))) ("2" (HIDE 2) (("2" (EXPAND "SAChain") (("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "n!1+1") (("2" (ASSERT) NIL))))))))))))))) ("3" (HIDE 2) (("3" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "j!2+1") (("2" (ASSERT) NIL))))))))))))))))))))))) (|flatten_chop_list_TCC1| "" (GRIND) NIL) (|flatten_chop_list| "" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "cum_sum") (("1" (EXPAND "at_up_to") (("1" (EXPAND "cons_list") (("1" (TYPEPRED "g!1") (("1" (EXPAND "tail") (("1" (EXPAND "SAChain") (("1" (PROP) (("1" (REPLACE -1) (("1" (ASSERT) (("1" (CASE "g!1 = LAMBDA (x: nat): g!1(x)") (("1" (REPLACE -1 1 RL) (("1" (PROPAX) NIL))) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (LEMMA "cons_at_tail[list[A]]") (("2" (INST -1 "chop(y!1, g!1)") (("2" (REWRITE "at" -1) (("2" (REWRITE "next_chop") (("2" (BETA) (("2" (LIFT-IF -1) (("2" (PROP) (("1" (HIDE -2 1) (("1" (BETA) (("1" (PROPAX) NIL))))) ("2" (EXPAND "tail" -1) (("2" (EXPAND "tail" -1) (("2" (REWRITE "next_chop") (("2" (BETA) (("2" (LIFT-IF -1) (("2" (ASSERT) (("2" (REPLACE -1 1) (("2" (HIDE -1) (("2" (REWRITE "flatten_list") (("1" (INST?) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (REWRITE "tail_tail") (("1" (EXPAND "cum_sum" 1 3) (("1" (REWRITE "cons_list_append") (("1" (EXPAND "cum_sum" 1 4) (("1" (LEMMA "at_up_to_sublist[A]") (("1" (INST -1 "y!1" "g!1(1)" "cum_sum(LAMBDA (x: nat): g!1(1 + x) - g!1(1), j!1)") (("1" (ASSERT) (("1" (REPLACE -1 1 RL) (("1" (EXPAND "sublist") (("1" (PROPAX) NIL))))))) ("2" (HIDE 2) (("2" (REWRITE "sum_sachain") NIL))) ("3" (HIDE 2) (("3" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "j!2+1") (("2" (ASSERT) NIL))))))))))))))))))))) ("2" (HIDE 2) (("2" (REWRITE "sum_sachain") NIL))) ("3" (HIDE 2) (("3" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "1 + j!2 + j!1") (("2" (ASSERT) NIL))))))))))))))) ("4" (HIDE 2) (("4" (REWRITE "sum_sachain") NIL))) ("5" (HIDE 2) (("5" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "j!2+1") (("2" (ASSERT) NIL))))))))))))))))))) ("2" (HIDE 2) (("2" (REWRITE "sum_sachain") NIL))) ("3" (HIDE 2) (("3" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "j!2+1") (("2" (ASSERT) NIL))))))))))))))))))))))) ("2" (HIDE 2) (("2" (REWRITE "sum_sachain") NIL))) ("3" (HIDE 2) (("3" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "j!2+1") (("2" (ASSERT) NIL))))))))))))))))) ("2" (HIDE -1 2) (("2" (REWRITE "sum_sachain") NIL))) ("3" (HIDE -1 2) (("3" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (ASSERT) (("2" (INST -2 "1+j!2") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))))) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (EXPAND "SAChain") (("3" (SKOSIMP*) (("3" (TYPEPRED "g!1") (("3" (EXPAND "SAChain") (("3" (PROP) (("3" (INST -2 "n!3+n!2") (("3" (ASSERT) NIL))))))))))))))))) ("4" (HIDE 2) (("4" (INDUCT "x") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (INST -1 "g!1" "n!2+1" "empty_seq[A]") (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "n!2") (("2" (ASSERT) NIL))))))))))))))))))) (|flatten_chop| "" (SKOSIMP*) (("" (LEMMA "at_eqn[A]") (("" (INST?) (("" (PROP) (("" (HIDE 2) (("" (SKOSIMP*) (("" (LEMMA "flatten_chop_list") (("" (INST?) (("" (INST -1 "n!1+1") (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "length_at_up_to[A]") (("" (INST -1 "y!1" "cum_sum(g!1, n!1 + 1)") (("" (CASE "cum_sum(g!1, n!1 + 1) /= 0") (("1" (ASSERT) (("1" (CASE "NOT bot?(at(y!1, cum_sum(g!1, 1 + n!1) - 1))") (("1" (ASSERT) (("1" (LEMMA "at_up_to_list[A]") (("1" (INST -1 "flatten(chop(tail(y!1, cum_sum(g!1, 1 + n!1)), LAMBDA (x: nat): g!1(1 + x + n!1) - g!1(1 + n!1)))" "at_up_to(y!1, cum_sum(g!1, 1 + n!1))") (("1" (LEMMA "at_up_to_at[A]") (("1" (INST -1 "cons_list(at_up_to(y!1, cum_sum(g!1, 1 + n!1)), flatten(chop(tail(y!1, cum_sum(g!1, 1 + n!1)), LAMBDA (x: nat): g!1(1 + x + n!1) - g!1(1 + n!1))))" "cum_sum(g!1, 1 + n!1)" "n!1") (("1" (CASE "n!1 < cum_sum(g!1, 1 + n!1)") (("1" (ASSERT) (("1" (REPLACE -5) (("1" (REPLACE -3 -2) (("1" (HIDE -3) (("1" (REPLACE -2 2 RL) (("1" (HIDE -2) (("1" (REWRITE "at_up_to_at") NIL))))))))))))) ("2" (HIDE -1 -2 2 3) (("2" (LEMMA "cum_sum_growth") (("2" (INST?) (("2" (ASSERT) NIL))))))))) ("2" (REWRITE "sum_sachain") NIL) ("3" (HIDE -1 -2 -3 3 2) (("3" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (ASSERT) (("2" (INST -2 "1 + j!1 + n!1") (("2" (ASSERT) NIL))))))))))))))))))))) ("2" (REWRITE "sum_sachain") NIL) ("3" (HIDE -1 -2 2 3) (("3" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "1 + j!1 + n!1") (("2" (ASSERT) NIL))))))))))))))))))))) ("2" (LEMMA "at_bot_tail[A]") (("2" (INST -1 "y!1" "cum_sum(g!1, 1 + n!1) - 1") (("2" (ASSERT) (("2" (HIDE -4) (("2" (CASE "tail(y!1, cum_sum(g!1, 1 + n!1)) = empty_seq") (("1" (REPLACE -1) (("1" (CASE "flatten(chop(empty_seq, LAMBDA (x: nat): g!1(1 + x + n!1) - g!1(1 + n!1))) = empty_seq") (("1" (REPLACE -1) (("1" (LEMMA "list_incl_list[A]") (("1" (INST?) (("1" (REPLACE -1 1 RL) (("1" (REWRITE "at_up_to_at") (("1" (PROP) (("1" (LIFT-IF 2) (("1" (PROP) (("1" (LEMMA "cum_sum_growth") (("1" (INST?) (("1" (ASSERT) NIL))))))))))))))))))))) ("2" (HIDE 2) (("2" (CASE "bot?(next(flatten(chop(empty_seq, LAMBDA (x: nat): g!1(1 + x + n!1) - g!1(1 + n!1)))))") (("1" (LEMMA "empty_unique[A]") (("1" (INST?) (("1" (ASSERT) NIL) ("2" (REWRITE "sum_sachain") NIL) ("3" (HIDE -1 -2 -3 -4 -5 2) (("3" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "1 + j!1 + n!1") (("2" (ASSERT) NIL))))))))))))))))))) ("2" (HIDE 2) (("2" (EXPAND "flatten") (("2" (REWRITE "next") (("2" (CASE "bot?(flatten_struct(chop(empty_seq, LAMBDA (x: nat): g!1(1 + x + n!1) - g!1(1 + n!1))))") (("1" (ASSERT) NIL) ("2" (HIDE 2) (("2" (EXPAND "flatten_struct") (("2" (CASE "bot?(holds_first_at((LAMBDA (l: list[A]): NOT l = null), chop(empty_seq, LAMBDA (x: nat): g!1(1 + x + n!1) - g!1(1 + n!1))))") (("1" (ASSERT) NIL) ("2" (HIDE 2) (("2" (EXPAND "holds_first_at") (("2" (LIFT-IF 1) (("2" (PROP) (("1" (ASSERT) NIL) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (EXPAND "chop") (("2" (EXPAND "sublist") (("2" (EXPAND "tail" 1) (("2" (REWRITE "next_empty") (("2" (ASSERT) (("2" (EXPAND "at_up_to") (("2" (REWRITE "next_empty") (("2" (ASSERT) (("2" (HIDE -1) (("2" (LEMMA "at_inf_incl[list[A]]") (("2" (INST?) (("2" (BETA) (("2" (REPLACE -1) (("2" (BETA) (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("3" (HIDE -1 -2 -3 -4 2 3) (("3" (EXPAND "SAChain") (("3" (SKOSIMP*) (("3" (TYPEPRED "g!1") (("3" (EXPAND "SAChain") (("3" (PROP) (("3" (INST -2 "1+n!2+n!1") (("3" (ASSERT) NIL))))))))))))))) ("4" (HIDE -1 -2 -3 -4 2) (("4" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "1 + j!1 + n!1") (("2" (ASSERT) NIL))))))))))))))))))) ("2" (HIDE 2) (("2" (LEMMA "tail_tail[A]") (("2" (INST -1 "y!1" "cum_sum(g!1, 1 + n!1) - 1" "1") (("2" (REPLACE -2) (("2" (REWRITE "tail_empty") (("2" (ASSERT) NIL))))))))))))))))))))))))) ("2" (HIDE -1 2) (("2" (EXPAND "cum_sum") (("2" (CASE "g!1(1) > 0") (("1" (ASSERT) NIL) ("2" (HIDE 2) (("2" (TYPEPRED "g!1") (("2" (EXPAND "SAChain") (("2" (PROP) (("2" (INST -2 "0") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))(|Flatten_naturality| (|flatten_nat| "" (SKOSIMP*) (("" (LEMMA "final_bisim_finality[B]") (("" (INST -1 "LAMBDA(x,y:Seq[B]) : EXISTS(z:Seq[list[A]]) : x = seq_map(f!1)(flatten(z)) AND y = flatten(seq_map(map(f!1))(z))") (("" (ASSERT) (("" (PROP) (("1" (INST -1 "seq_map(f!1)(flatten(x!1))" "flatten(seq_map(map(f!1))(x!1))") (("1" (PROP) (("1" (ASSERT) NIL) ("2" (INST?) (("2" (ASSERT) NIL))))))) ("2" (HIDE 2) (("2" (EXPAND "bisimulation?") (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (REPLACE -2) (("2" (HIDE -1 -2) (("2" (NAME "ape" "next(seq_map(f!1)(flatten(z!1)))") (("2" (REPLACE -1) (("2" (NAME "dog" "next(flatten(seq_map(map(f!1))(z!1)))") (("2" (REPLACE -1) (("2" (EXPAND "seq_map" -2) (("2" (REWRITE "next") (("2" (NAME "cow" "seq_map_struct(f!1)(flatten(z!1))") (("2" (REPLACE -1) (("2" (EXPAND "seq_map_struct") (("2" (NAME "horse" "next(flatten(z!1))") (("2" (REPLACE -1) (("2" (EXPAND "flatten" -1) (("2" (REWRITE "next") (("2" (HIDE 1) (("2" (EXPAND "flatten" -3) (("2" (REWRITE "next") (("2" (NAME "fly" "flatten_struct(seq_map(map(f!1))(z!1))") (("2" (REPLACE -1) (("2" (CASE "bot?(holds_first_at((LAMBDA (l: list[A]): NOT l = null), z!1))") (("1" (CASE "bot?(holds_first_at((LAMBDA (l: list[B]): NOT l = null), seq_map(map(f!1))(z!1)))") (("1" (EXPAND "flatten_struct" -3) (("1" (ASSERT) (("1" (EXPAND "flatten_struct" -4) (("1" (ASSERT) (("1" (REVEAL 1) (("1" (ASSERT) NIL))))))))))) ("2" (HIDE -2 -3 -4 -5 -6) (("2" (EXPAND "holds_first_at") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (PROP) (("2" (SKOSIMP*) (("2" (LEMMA "at_seq_map[list[A],list[B]]") (("2" (INST?) (("2" (PROP) (("2" (INST?) (("2" (ASSERT) (("2" (REPLACE -4) (("2" (EXPAND "map") (("2" (PROPAX) NIL))))))))))))))))))))))))))))) ("2" (CASE "bot?(holds_first_at((LAMBDA (l: list[B]): NOT l = null), seq_map(map(f!1))(z!1)))") (("1" (HIDE -2 -3 -4 -5 -6) (("1" (EXPAND "holds_first_at") (("1" (LIFT-IF) (("1" (ASSERT) (("1" (PROP) (("1" (SKOSIMP*) (("1" (INST?) (("1" (LEMMA "at_seq_map[list[A],list[B]]") (("1" (INST?) (("1" (PROP) (("1" (REPLACE -1) (("1" (EXPAND "map") (("1" (ASSERT) NIL))))))))))))))))))))))))) ("2" (LEMMA "cover[nat]") (("2" (INST-CP -1 "holds_first_at((LAMBDA (l: list[B]): NOT l = null), seq_map(map(f!1))(z!1))") (("2" (ASSERT) (("2" (INST -1 "holds_first_at((LAMBDA (l: list[A]): NOT l = null), z!1)") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (HIDE 1 2) (("2" (CASE "x!2 = x!3") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (EXPAND "flatten_struct" -3) (("1" (REPLACE -2) (("1" (ASSERT) (("1" (EXPAND "flatten_struct" -4 4) (("1" (EXPAND "flatten_struct" -4 2) (("1" (EXPAND "flatten_struct" -4 1) (("1" (REPLACE -1) (("1" (ASSERT) (("1" (REPLACE -3 * RL) (("1" (REPLACE -4 * RL) (("1" (HIDE -3 -4) (("1" (ASSERT) (("1" (REVEAL 3) (("1" (REPLACE -3 * RL) (("1" (REPLACE -4 * RL) (("1" (REPLACE -5 * RL) (("1" (HIDE -3 -4 -5) (("1" (ASSERT) (("1" (LEMMA "at_seq_map[list[A],list[B]]") (("1" (INST?) (("1" (LEMMA "at_holds_first_at[list[B]]") (("1" (INST?) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (LEMMA "at_holds_first_at[list[A]]") (("1" (INST?) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (SPLIT 3) (("1" (BETA) (("1" (SPLIT -5) (("1" (REPLACE -1) (("1" (EXPAND "map" 1) (("1" (LIFT-IF 1) (("1" (SPLIT 1) (("1" (PROP) (("1" (HIDE -2 -4 -5 -6 -7 -8 1 2 4 5) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL))) ("2" (PROP) (("1" (ASSERT) NIL) ("2" (BETA) (("2" (PROPAX) NIL))))))))))))) ("2" (ASSERT) NIL))))) ("2" (BETA) (("2" (INST 1 "cons_seq(cdr(down(at(z!1, x!3))), tail(z!1, 1 + x!3))") (("1" (EXPAND "flatten" 1) (("1" (EXPAND "seq_map" 1 1) (("1" (EXPAND "seq_map_struct" 1 1) (("1" (LEMMA "seq_map_cons[list[A],list[B]]") (("1" (INST?) (("1" (REPLACE -1) (("1" (REWRITE "tail_seq_map") (("1" (SPLIT -6) (("1" (REPLACE -1) (("1" (EXPAND "map" 1 1) (("1" (LIFT-IF 1) (("1" (SPLIT 1) (("1" (PROP) (("1" (HIDE -2 -4 -5 -6 -7 -8 -9 1 2 4 5) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL))) ("2" (PROP) (("1" (BETA) (("1" (PROPAX) NIL))) ("2" (BETA) (("2" (PROPAX) NIL))))))))))))) ("2" (ASSERT) NIL))))))) ("2" (HIDE -1 -2 -3 -4 -5 -6 -7 2 5 6) (("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("3" (ASSERT) NIL))))))))))) ("2" (HIDE -1 -2 -3 -4 -5 -6 -7 4 5) (("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("3" (ASSERT) NIL))))))))) ("2" (PROPAX) NIL))))))))) ("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (HIDE -3 -4 -5 -6 -7) (("2" (LEMMA "at_holds_first_at[list[A]]") (("2" (INST?) (("2" (SPLIT -1) (("1" (FLATTEN) (("1" (BETA) (("1" (LEMMA "at_holds_first_at[list[B]]") (("1" (INST?) (("1" (PROP) (("1" (BETA) (("1" (INST -1 "x!2") (("1" (INST -2 "x!3") (("1" (HIDE -3 -4) (("1" (LEMMA "at_seq_map[list[A],list[B]]") (("1" (INST -1 "map(f!1)" "z!1" "x!2") (("1" (FLATTEN -1) (("1" (SPLIT -2) (("1" (SPLIT -2) (("1" (SPLIT -4) (("1" (SPLIT -4) (("1" (LEMMA "at_seq_map[list[A],list[B]]") (("1" (INST -1 "map(f!1)" "z!1" "x!3") (("1" (FLATTEN -1) (("1" (SPLIT -1) (("1" (SPLIT -2) (("1" (SPLIT -3) (("1" (CASE "down(at(z!1, x!3)) = null") (("1" (REPLACE -1) (("1" (EXPAND "map" -2 2) (("1" (PROPAX) NIL))))) ("2" (SPLIT -8) (("1" (HIDE -2 -3 -4 -5 -7 -8 1 2 3 4 5) (("1" (ASSERT) NIL))) ("2" (HIDE -2 -4 -5 -6 -7 -8 1 2 3 4 5 6) (("2" (CASE "at(z!1, x!3) = bot") (("1" (REPLACE -1) (("1" (HIDE -2) (("1" (ASSERT) NIL))))) ("2" (HIDE -2) (("2" (CASE "bot?(at(z!1, x!3))") (("1" (ASSERT) NIL) ("2" (PROPAX) NIL))))))))) ("3" (PROPAX) NIL))) ("3" (PROPAX) NIL))) ("2" (PROPAX) NIL))) ("2" (PROPAX) NIL))) ("2" (HIDE -2 -3 -4 -5 -6 -7 3 4 5 6) (("2" (SPLIT -1) (("1" (PROPAX) NIL) ("2" (ASSERT) NIL))))))))))))) ("2" (PROPAX) NIL))) ("2" (HIDE -3 -4 -5 1 2 3 4 5) (("2" (CASE "at(seq_map(map(f!1))(z!1), x!2) = bot") (("1" (REPLACE -1) (("1" (ASSERT) NIL))) ("2" (HIDE -2) (("2" (CASE "bot?(at(seq_map(map(f!1))(z!1), x!2))") (("1" (ASSERT) NIL) ("2" (PROPAX) NIL))))))))) ("3" (REPLACE -1) (("3" (HIDE -1) (("3" (SPLIT -3) (("1" (HIDE -4 1 2 5) (("1" (HIDE -2 1) (("1" (EXPAND "map") (("1" (LIFT-IF) (("1" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))) ("2" (PROPAX) NIL))))))))) ("2" (PROPAX) NIL))) ("2" (HIDE -2 -3 -4 2 3 5 6) (("2" (PROP) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))) ("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))(|Seq_strength| (|strength_struct_TCC1| "" (GRIND) NIL) (|strength_empty| "" (SKOSIMP) (("" (CASE "next(seq_strength(empty_seq[A], b!1))=next( empty_seq[[A,B]])") (("1" (LEMMA "next_iso[[A, B]]") (("1" (PROP) (("1" (INST-CP -2 "seq_strength(empty_seq, b!1)") (("1" (HIDE -1) (("1" (INST -1 "empty_seq") (("1" (ASSERT) NIL))))))))))) ("2" (HIDE 2) (("2" (EXPAND "seq_strength") (("2" (REWRITE "next") (("2" (EXPAND "strength_struct" 1 1) (("2" (REWRITE "next_empty") (("2" (ASSERT) (("2" (REWRITE "next_empty") NIL))))))))))))))))) (|strength_cons| "" (SKOSIMP) (("" (LEMMA "next_iso[[A, B]]") (("" (PROP) (("" (CASE "next(seq_strength(cons_seq(a!1, x!1), b!1))=next(cons_seq((a!1, b!1), seq_strength(x!1, b!1)))") (("1" (HIDE -2) (("1" (INST-CP -2 "seq_strength(cons_seq(a!1, x!1), b!1)") (("1" (INST -2 "cons_seq((a!1, b!1), seq_strength(x!1, b!1))") (("1" (ASSERT) NIL))))))) ("2" (HIDE -1 -2 2) (("2" (REWRITE "next_cons") (("2" (EXPAND "seq_strength" 1 1) (("2" (REWRITE "next") (("2" (REWRITE "seq_strength" :DIR RL) (("2" (EXPAND "strength_struct") (("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))))))))))))))))))))))(|Seq_strength_nat| (|seq_strength_nat| "" (SKOSIMP) (("" (LEMMA "bisim_finality[[C,D],Seq[[C,D]],Seq[[C,D]]]") (("" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("" (INST -1 "next" "next" "(seq_map((LAMBDA (x: [A, B]): (f!1(PROJ_1(x)), g!1(PROJ_2(x))))) o seq_strength[A, B])(x!1, x!2)" "(seq_strength[C, D] o (LAMBDA (x: [Seq[A], B]): (seq_map(f!1)(PROJ_1(x)), g!1(PROJ_2(x)))))(x!1, x!2)") (("" (PROP) (("1" (HIDE -1) (("1" (EXPAND "Kernel") (("1" (REWRITE "id_coreduce" :DIR RL) (("1" (REWRITE "id_coreduce" :DIR RL) NIL))))))) ("2" (HIDE 1 3) (("2" (EXPAND "bisim?") (("2" (INST 1 "{x,y:Seq[[C,D]]| exists (l: Seq[A],b: B): x= (seq_map((LAMBDA (x: [A, B]): (f!1(PROJ_1(x)), g!1(PROJ_2(x))))) o seq_strength[A, B])(l, b) AND y = (seq_strength[C, D] o (LAMBDA (x: [Seq[A], B]): (seq_map(f!1)(PROJ_1(x)), g!1(PROJ_2(x)))))(l, b)}") (("2" (PROP) (("1" (EXPAND "bisimulation?") (("1" (SKOSIMP) (("1" (SKOSIMP) (("1" (ASSERT) (("1" (PROP) (("1" (LEMMA "not_bot_next[[C,D]]") (("1" (INST -1 "x2!1") (("1" (SPLIT) (("1" (SKOSIMP*) (("1" (CASE "bot?(next(l!1))") (("1" (REWRITE "empty_unique[A]") (("1" (EXPAND "o ") (("1" (HIDE -1 -2 -3 -4) (("1" (REWRITE "seq_map_empty[A,C]") (("1" (REWRITE "strength_empty") (("1" (REPLACE -1) (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))))))))))))) ("2" (HIDE -1 -4) (("2" (LEMMA "not_bot_next[A]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (REPLACE -1 -3) (("2" (EXPAND "o ") (("2" (REWRITE "strength_cons") (("2" (REWRITE "seq_map_cons[[A,B],[C,D]]") (("2" (REPLACE -3 -2) (("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))))))))))))))))))))))))) ("2" (PROPAX) NIL))))))) ("2" (EXPAND "o ") (("2" (REPLACE -2 1) (("2" (HIDE -2) (("2" (CASE "bot?(next(l!1))") (("1" (REWRITE "empty_unique[A]") (("1" (HIDE -1) (("1" (REWRITE "seq_map_empty[A,C]") (("1" (REWRITE "strength_empty") (("1" (REWRITE "strength_empty") (("1" (REWRITE "seq_map_empty[[A,B],[C,D]]") (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))))))))))))) ("2" (HIDE 2) (("2" (LEMMA "not_bot_next[A]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (REPLACE -1 -3) (("2" (HIDE -1 1) (("2" (REWRITE "seq_map_cons[A,C] ") (("2" (REWRITE "strength_cons") (("2" (REPLACE -2 -1) (("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))) ("3" (REPLACE -1) (("3" (REPLACE -2) (("3" (HIDE -1 -2) (("3" (EXPAND "o") (("3" (REWRITE-DESTR "next" "seq_strength" 2) (("3" (EXPAND "strength_struct") (("3" (REWRITE-DESTR "next" "seq_map" 2) (("3" (LIFT-IF) (("3" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (LEMMA "not_bot_next[A]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (REPLACE -1) (("2" (HIDE -1 2) (("2" (REWRITE "seq_map_cons[A,C] ") (("2" (REWRITE "strength_cons") (("2" (REWRITE "strength_cons[C,D]") (("2" (REWRITE "seq_map_cons[[A,B],[C,D]]") (("2" (REWRITE "next_cons") (("2" (REWRITE "next_cons") (("2" (ASSERT) (("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))) ("4" (EXPAND "o ") (("4" (INST 1 "proj_2(down(next(l!1)))" "b!1") (("1" (PROP) (("1" (REPLACE -1 1) (("1" (HIDE -1 -2) (("1" (REWRITE-DESTR "next" "seq_map" 1) (("1" (REWRITE-DESTR "next" "seq_strength" 1) (("1" (EXPAND "strength_struct") (("1" (ASSERT) (("1" (LIFT-IF) (("1" (PROP) (("1" (ASSERT) (("1" (REVEAL -1) (("1" (REWRITE "empty_unique[A]") (("1" (REWRITE "strength_empty") (("1" (REWRITE "seq_map_empty[[A,B],[C,D]]") (("1" (REPLACE -1) (("1" (REWRITE "next_empty") (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))))))))))))))) ("2" (ASSERT) NIL))))))))))))))))) ("2" (REPLACE -2 1) (("2" (CASE "bot?(next(l!1))") (("1" (REWRITE "empty_unique[A]") (("1" (REWRITE "strength_empty") (("1" (REWRITE "seq_map_empty[[A,B],[C,D]]") (("1" (REPLACE -2) (("1" (REWRITE "next_empty") (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))))))))))) ("2" (LEMMA "not_bot_next[A]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (REPLACE -1) (("2" (REWRITE "seq_map_cons[A,C] ") (("2" (REWRITE "strength_cons[C,D]") (("2" (REWRITE "strength_cons") (("2" (REWRITE "next_cons") (("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (CASE "bot?(next(l!1))") (("1" (HIDE 1) (("1" (REWRITE "empty_unique[A]") (("1" (REWRITE "strength_empty") (("1" (REWRITE "seq_map_empty[[A,B],[C,D]]") (("1" (REPLACE -2) (("1" (REWRITE "next_empty" 2) (("1" (ASSERT) NIL))))))))))))) ("2" (ASSERT) NIL))))))))))))))))))) ("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))(|Seq_coherence| (|seq_strength_assoc| "" (SKOSIMP) (("" (LEMMA "bisim_finality[[A,[B,C]],Seq[[A,[B,C]]],Seq[[A,[B,C]]]]") (("" (INST -1 "next" "next" " seq_strength[A, [B, C]](l!1, (b!1, c!1))" "seq_map(LAMBDA (x: [A, B], c: C): (PROJ_1(x), (PROJ_2(x), c)))(seq_strength(seq_strength(l!1, b!1), c!1))") (("" (PROP) (("1" (EXPAND "Kernel") (("1" (REWRITE "id_coreduce" :DIR RL) (("1" (REWRITE "id_coreduce" :DIR RL) NIL))))) ("2" (HIDE 1 3) (("2" (EXPAND "bisim?") (("2" (INST 1 "{l,k:Seq[[A, [B, C]]] | exists (m:Seq[A]) : l = seq_strength[A, [B, C]](m, (b!1, c!1)) AND k = seq_map(LAMBDA (x: [A, B], c: C): (PROJ_1(x), (PROJ_2(x), c)))(seq_strength(seq_strength(m, b!1), c!1))}") (("2" (PROP) (("1" (EXPAND "bisimulation?") (("1" (SKOSIMP) (("1" (SKOSIMP) (("1" (PROP) (("1" (CASE-REPLACE "m!1=empty_seq") (("1" (REWRITE "strength_empty") (("1" (REWRITE "strength_empty") (("1" (REWRITE "strength_empty") (("1" (REWRITE "seq_map_empty[[[A,B],C],[A,[B,C]]]") (("1" (REPLACE -4 1) (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))))))))))) ("2" (LEMMA "not_bot_next[A]") (("2" (INST?) (("2" (PROP) (("1" (SKOSIMP) (("1" (REPLACE -1) (("1" (REWRITE "strength_cons") (("1" (REPLACE -3 -2) (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))))))))) ("2" (REWRITE "empty_unique") NIL))))))))) ("2" (REPLACE -2 1) (("2" (CASE "bot?(next(m!1))") (("1" (REWRITE "empty_unique") (("1" (REWRITE "strength_empty") (("1" (REWRITE "next_empty") (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))))))) ("2" (USE "not_bot_next[A]") (("2" (SPLIT) (("1" (SKOSIMP) (("1" (REPLACE -1 -4) (("1" (REWRITE "strength_cons") (("1" (REWRITE "strength_cons[[A,B],C]") (("1" (REWRITE "seq_map_cons[[[A,B],C],[A,[B,C]]]") (("1" (REPLACE -4 -2) (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))))))))))))) ("2" (PROPAX) NIL))))))))) ("3" (REPLACE -1) (("3" (REPLACE -2) (("3" (HIDE -1 -2) (("3" (REWRITE-DESTR "next" "seq_map") (("3" (REWRITE-DESTR "next" "seq_map" 2) (("3" (REWRITE-DESTR "next" "seq_strength" 2) (("3" (EXPAND "strength_struct") (("3" (LIFT-IF) (("3" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (REWRITE-DESTR "next" "seq_strength" 1) (("2" (LIFT-IF) (("2" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (EXPAND "strength_struct") (("2" (ASSERT) (("2" (LIFT-IF) (("2" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (HIDE 2) (("2" (USE "not_bot_next[A]") (("2" (HIDE 3 4) (("2" (SPLIT) (("1" (SKOSIMP) (("1" (REPLACE -1) (("1" (HIDE -1 1 2) (("1" (REWRITE "strength_cons") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (REWRITE "strength_cons") (("1" (REWRITE "strength_cons") (("1" (REWRITE "seq_map_cons[[[A,B],C],[A,[B,C]]]") (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))))))))))))))))))) ("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))))))))))) ("4" (INST 1 "proj_2(down(next(m!1)))") (("1" (ASSERT) (("1" (PROP) (("1" (REPLACE -1 1) (("1" (REWRITE-DESTR "next" "seq_strength" 1) (("1" (EXPAND "strength_struct") (("1" (LIFT-IF) (("1" (PROP) (("1" (ASSERT) (("1" (REWRITE "empty_unique") (("1" (REWRITE "strength_empty") (("1" (REPLACE -2) (("1" (REWRITE "next_empty") (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))))))))))) ("2" (ASSERT) NIL))))))))))) ("2" (REPLACE -2 1) (("2" (REWRITE-DESTR "next" "seq_map" 1 1) (("2" (LIFT-IF) (("2" (ASSERT) (("2" (PROP) (("1" (ASSERT) (("1" (REWRITE-DESTR "next" "seq_strength" -1) (("1" (EXPAND "strength_struct") (("1" (LIFT-IF) (("1" (ASSERT) (("1" (PROP) (("1" (ASSERT) (("1" (REWRITE-DESTR "next" "seq_strength" -1) (("1" (EXPAND "strength_struct") (("1" (LIFT-IF) (("1" (ASSERT) (("1" (PROP) (("1" (HIDE 1) (("1" (REWRITE "empty_unique") (("1" (REWRITE "strength_empty") (("1" (REPLACE -2) (("1" (REWRITE "next_empty") (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))))))))))))))))))))))))))))))))))) ("2" (REWRITE-DESTR "next" "seq_strength" 1) (("2" (EXPAND "strength_struct") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (PROP) (("2" (REWRITE-DESTR "next" "seq_strength" 1) (("2" (EXPAND "strength_struct") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (PROP) (("2" (USE "not_bot_next[A]") (("2" (SPLIT -1) (("1" (SKOSIMP) (("1" (REPLACE -1) (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (REWRITE "strength_cons[A,B]") (("1" (REWRITE "strength_cons[[A,B],C]") (("1" (EXPAND "seq_map_struct") (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))))))))))))))) ("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (REPLACE -1 3) (("2" (REWRITE-DESTR "next" "seq_strength" 3) (("2" (EXPAND "strength_struct") (("2" (PROPAX) NIL))))))))))))))))))) ("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))) (|seq_strength_proj| "" (SKOSIMP) (("" (LEMMA "coreduce_unique[A, Seq[A]]") (("" (INST -1 "next" "(LAMBDA (l: Seq[A]): seq_map((LAMBDA (x: [A, B]): PROJ_1(x)))(seq_strength(l, b!1)))") (("" (PROP) (("1" (CASE "(LAMBDA (l: Seq[A]): seq_map((LAMBDA (x: [A, B]): PROJ_1(x)))(seq_strength(l, b!1)))(l!1)=coreduce(next[A])(l!1)") (("1" (ASSERT) (("1" (REWRITE "id_coreduce" :DIR RL) NIL))) ("2" (REPLACE -1) (("2" (PROPAX) NIL))))) ("2" (HIDE 2) (("2" (EXPAND "struct_map?") (("2" (SKOSIMP) (("2" (PROP) (("1" (REWRITE "empty_unique") (("1" (REWRITE "strength_empty") (("1" (REWRITE "seq_map_empty[[A,B],A]") NIL))))) ("2" (REWRITE-DESTR "next" "seq_map" 1 1) (("2" (LIFT-IF) (("2" (ASSERT) (("2" (PROP) (("1" (ASSERT) (("1" (REWRITE-DESTR "next" "seq_strength" -1) (("1" (EXPAND "strength_struct") (("1" (PROPAX) NIL))))))) ("2" (ASSERT) (("2" (EXPAND "seq_map_struct") (("2" (ASSERT) (("2" (REWRITE-DESTR "next" "seq_strength" 2) (("2" (EXPAND "strength_struct") (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))(|final_obj|)(|Seq_shape| (|shape_empty| "" (EXPAND "shape") (("" (REWRITE "seq_map_empty[A,final_obj]") NIL))) (|shape_cons| "" (SKOSIMP) (("" (EXPAND "shape") (("" (REWRITE "seq_map_cons[A,final_obj]") NIL))))))(|Seq_zip| (|next_equal_bot| "" (SKOSIMP) (("" (PROP) (("1" (TYPEPRED "x!1") (("1" (EXPAND "equal_shape") (("1" (LEMMA "not_bot_next[B]") (("1" (INST?) (("1" (SPLIT) (("1" (SKOSIMP) (("1" (REPLACE -1 -2) (("1" (REWRITE "empty_unique[A]") (("1" (REWRITE "shape_empty[A]") (("1" (REWRITE "shape_cons[B]") (("1" (CASE "next(cons_seq(star, shape(y!1))) = next(empty_seq[final_obj])") (("1" (REWRITE "next_cons") (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))))) ("2" (PROPAX) NIL))))))))))) ("2" (TYPEPRED "x!1") (("2" (EXPAND "equal_shape") (("2" (REWRITE "empty_unique[B]") (("2" (REWRITE "shape_empty[B]") (("2" (LEMMA "not_bot_next[A]") (("2" (INST?) (("2" (SPLIT) (("1" (SKOSIMP) (("1" (REPLACE -1 -2) (("1" (REWRITE "shape_cons[A]") (("1" (CASE "next(cons_seq(star, shape(y!1))) = next(empty_seq[final_obj])") (("1" (REWRITE "next_cons") (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))) ("2" (PROPAX) NIL))))))))))))))))))) (|next_equal_shape_TCC1| "" (SKOSIMP) (("" (PROP) (("1" (ASSERT) NIL) ("2" (TYPEPRED "x!1") (("2" (EXPAND "equal_shape") (("2" (LEMMA "not_bot_next[B]") (("2" (INST?) (("2" (PROP) (("2" (SKOSIMP) (("2" (REPLACE -1) (("2" (REWRITE "shape_cons[B]") (("2" (CASE "next(shape(PROJ_1(x!1)))= next(cons_seq(star, shape(y!1)))") (("1" (HIDE -2 -3 1) (("1" (REWRITE "next_cons") (("1" (EXPAND "shape" -1 1) (("1" (EXPAND "seq_map") (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (REWRITE "shape" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (LIFT-IF) (("1" (PROP) (("1" (BETA) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL))))))))))))))))))))) ("2" (REPLACE -2) (("2" (PROPAX) NIL))))))))))))))))))))))))) (|next_equal_shape_TCC2| "" (SKOSIMP) (("" (PROP) (("1" (ASSERT) (("1" (TYPEPRED "x!1") (("1" (EXPAND "equal_shape") (("1" (LEMMA "not_bot_next[A]") (("1" (INST?) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (REPLACE -1) (("1" (REWRITE "shape_cons[A]") (("1" (CASE "next(shape(PROJ_2(x!1)))= next(cons_seq(star, shape(y!1)))") (("1" (HIDE -2 -3 1) (("1" (REWRITE "next_cons") (("1" (EXPAND "shape" -1 1) (("1" (EXPAND "seq_map") (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (REWRITE "shape" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (PROPAX) NIL))))))))))))))))) ("2" (REPLACE -2) (("2" (PROPAX) NIL))))))))))))))))))))))) ("2" (ASSERT) NIL))))) (|next_equal_shape| "" (SKOSIMP) (("" (PROP) (("1" (EXPAND "equal_shape") (("1" (LEMMA "not_bot_next[A]") (("1" (INST?) (("1" (SPLIT) (("1" (SKOSIMP) (("1" (TYPEPRED "x!1") (("1" (EXPAND "equal_shape") (("1" (REPLACE -2) (("1" (REWRITE "shape_cons") (("1" (CASE "next(cons_seq(star, shape(y!1))) = next(shape(PROJ_2(x!1)))") (("1" (HIDE 1) (("1" (REWRITE "next_cons") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (EXPAND "shape" -1 2) (("1" (EXPAND "seq_map") (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (ASSERT) (("1" (LIFT-IF) (("1" (ASSERT) (("1" (PROP) (("1" (REWRITE "shape" :DIR RL) (("1" (HIDE -2 -3) (("1" (LEMMA "mono_up[[final_obj,Seq[final_obj]]]") (("1" (INST -1 "(star, shape(y!1))" "(star, shape(PROJ_2(down(next(PROJ_2(x!1))))))") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))) ("2" (REPLACE -1 1) (("2" (PROPAX) NIL))))))))))))))) ("2" (PROPAX) NIL))))))))) ("2" (EXPAND "equal_shape") (("2" (TYPEPRED "x!1") (("2" (EXPAND "equal_shape") (("2" (LEMMA "not_bot_next[B]") (("2" (INST?) (("2" (SPLIT) (("1" (SKOSIMP) (("1" (CASE "next(shape(PROJ_1(x!1)))= next(shape(PROJ_2(x!1)))") (("1" (HIDE -3) (("1" (REPLACE -2) (("1" (HIDE 1) (("1" (REWRITE "shape_cons[B]") (("1" (REWRITE "next_cons") (("1" (REWRITE "next_cons[B]") (("1" (ASSERT) (("1" (EXPAND "shape" -1 1) (("1" (EXPAND "seq_map") (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (REWRITE "shape" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (LIFT-IF) (("1" (ASSERT) (("1" (PROP) (("1" (ASSERT) (("1" (CASE "PROJ_2(down(up[[final_obj,Seq[final_obj]]](star, shape(PROJ_2(down(next(PROJ_1(x!1)))))))) =PROJ_2(down(up(star, shape(y!1))))") (("1" (ASSERT) NIL) ("2" (REPLACE -1) (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))) ("2" (REPLACE -2) (("2" (PROPAX) NIL))))))) ("2" (PROPAX) NIL))))))))))))))))) (|zip_struct_TCC1| "" (SKOSIMP) (("" (LEMMA "not_bot_next[A]") (("" (INST?) (("" (ASSERT) NIL))))))) (|zip_struct_TCC2| "" (SKOSIMP) (("" (TYPEPRED "x!1") (("" (REPLACE -2) (("" (REPLACE -3) (("" (HIDE -2 -3) (("" (LEMMA "next_equal_bot") (("" (INST?) (("" (ASSERT) NIL))))))))))))))) (|zip_struct_TCC3| "" (SKOSIMP) (("" (ASSERT) (("" (TYPEPRED "x!1") (("" (LEMMA "next_equal_shape") (("" (INST?) (("" (ASSERT) NIL))))))))))) (|zip_empty_left| "" (SKOSIMP) (("" (LEMMA "next_equal_bot") (("" (INST?) (("" (ASSERT) (("" (EXPAND "zip") (("" (REWRITE "next") (("" (REWRITE "zip" :DIR RL) (("" (EXPAND "zip_struct") (("" (PROPAX) NIL))))))))))))))))) (|zip_empty_right| "" (SKOSIMP) (("" (LEMMA "next_equal_bot") (("" (INST?) (("" (ASSERT) (("" (EXPAND "zip") (("" (REWRITE "next") (("" (REWRITE "zip" :DIR RL) (("" (EXPAND "zip_struct") (("" (PROPAX) NIL))))))))))))))))) (|zip_cons_left_TCC1| "" (GRIND) NIL) (|zip_cons_left_TCC2| "" (LEMMA "next_equal_bot") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL))))))) (|zip_cons_left_TCC3| "" (SKOSIMP) (("" (LEMMA "next_equal_bot") (("" (LEMMA "next_equal_shape") (("" (INST?) (("" (INST?) (("" (ASSERT) NIL))))))))))) (|zip_cons_left| "" (SKOSIMP) (("" (LEMMA "next_equal_bot") (("" (INST?) (("" (ASSERT) (("" (CASE "next(zip(x!1)) = next(cons_seq((PROJ_1(down(next(PROJ_1(x!1)))), PROJ_1(down(next(PROJ_2(x!1))))), zip(PROJ_2(down(next(PROJ_1(x!1)))), PROJ_2(down(next(PROJ_2(x!1)))))))") (("1" (LEMMA "next_iso[[A,B]]") (("1" (PROP) (("1" (INST-CP -2 "zip(x!1)") (("1" (INST -2 "cons_seq((PROJ_1(down(next(PROJ_1(x!1)))), PROJ_1(down(next(PROJ_2(x!1))))), zip(PROJ_2(down(next(PROJ_1(x!1)))), PROJ_2(down(next(PROJ_2(x!1))))))") (("1" (ASSERT) NIL))))))))) ("2" (HIDE 4) (("2" (REWRITE "next_cons") (("2" (EXPAND "zip") (("2" (REWRITE "next") (("2" (REWRITE "zip" :DIR RL) (("2" (LIFT-IF) (("2" (PROP) (("1" (EXPAND "zip_struct") (("1" (PROPAX) NIL))) ("2" (ASSERT) (("2" (EXPAND "zip_struct") (("2" (PROPAX) NIL))))))))))))))))))))))))))))) (|zip_cons_right_TCC1| "" (SKOSIMP) (("" (LEMMA "next_equal_bot") (("" (INST?) (("" (ASSERT) NIL))))))) (|zip_cons_right_TCC2| "" (GRIND) NIL) (|zip_cons_right_TCC3| "" (SKOSIMP) (("" (LEMMA "next_equal_bot") (("" (LEMMA "next_equal_shape") (("" (INST?) (("" (INST?) (("" (ASSERT) NIL))))))))))) (|zip_cons_right| "" (SKOSIMP) (("" (USE "next_equal_bot") (("" (PROP) (("" (CASE "next(zip(x!1)) = next(cons_seq((PROJ_1(down(next(PROJ_1(x!1)))), PROJ_1(down(next(PROJ_2(x!1))))), zip(PROJ_2(down(next(PROJ_1(x!1)))), PROJ_2(down(next(PROJ_2(x!1)))))))") (("1" (USE "next_iso[[A,B]]") (("1" (PROP) (("1" (INST-CP -2 "zip(x!1)") (("1" (INST -2 "cons_seq((PROJ_1(down(next(PROJ_1(x!1)))), PROJ_1(down(next(PROJ_2(x!1))))), zip(PROJ_2(down(next(PROJ_1(x!1)))), PROJ_2(down(next(PROJ_2(x!1))))))") (("1" (ASSERT) NIL) ("2" (USE "next_equal_shape") (("2" (ASSERT) NIL))) ("3" (ASSERT) NIL))))))))) ("2" (HIDE 5) (("2" (REWRITE "next_cons") (("2" (REWRITE-DESTR "next" "zip" 1 1) (("2" (EXPAND "zip_struct") (("2" (PROPAX) NIL))))))))) ("3" (USE "next_equal_shape") (("3" (ASSERT) NIL))) ("4" (ASSERT) NIL))))))))) (|zip_cons_TCC1| "" (SKOSIMP) (("" (EXPAND "equal_shape") (("" (REWRITE "shape_cons[B]") (("" (REWRITE "shape_cons") (("" (ASSERT) NIL))))))))) (|zip_cons| "" (SKOSIMP) (("" (CASE "equal_shape(cons_seq(a!1, l!1), cons_seq(b!1, k!1))") (("1" (CASE "not(bot?(next(cons_seq(a!1, l!1))))") (("1" (REWRITE "zip_cons_left") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))))))) ("2" (REWRITE "next_cons") (("2" (ASSERT) NIL))))) ("2" (HIDE 2) (("2" (EXPAND "equal_shape" 1) (("2" (REWRITE "shape_cons") (("2" (REWRITE "shape_cons[B]") (("2" (EXPAND "equal_shape") (("2" (ASSERT) NIL))))))))))))))) (|zip_inv_TCC1| "" (SKOSIMP) (("" (EXPAND "equal_shape") (("" (LEMMA "bisim_finality[final_obj,Seq[final_obj],Seq[final_obj]]") (("" (INST -1 "next" "next" "shape(seq_map[[A, B], A]((LAMBDA (x: [A, B]): PROJ_1(x)))(l!1))" "shape(seq_map[[A, B], B]((LAMBDA (x: [A, B]): PROJ_2(x)))(l!1))") (("" (PROP) (("1" (EXPAND "Kernel") (("1" (REWRITE "id_coreduce" :DIR RL) (("1" (REWRITE "id_coreduce" :DIR RL) NIL))))) ("2" (HIDE 1 3) (("2" (EXPAND "bisim?") (("2" (INST 1 "{l,k:Seq[final_obj] | EXISTS (l1: Seq[[A,B]]) : l = shape(seq_map[[A, B], A]((LAMBDA (x: [A, B]): PROJ_1(x)))(l1)) AND k = shape(seq_map[[A, B], B]((LAMBDA (x: [A, B]): PROJ_2(x)))(l1))}") (("2" (PROP) (("1" (EXPAND "bisimulation?") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (SKOSIMP) (("1" (PROP) (("1" (REPLACE -2 -1) (("1" (REPLACE -3 1) (("1" (HIDE -2 -3) (("1" (EXPAND "shape" -1) (("1" (EXPAND "seq_map" -1 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (EXPAND "shape" 1) (("1" (EXPAND "seq_map" 1 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (LIFT-IF) (("1" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (ASSERT) (("3" (EXPAND "seq_map" 1 1) (("3" (REWRITE "next") (("3" (REWRITE "seq_map" :DIR RL) (("3" (EXPAND "seq_map_struct") (("3" (EXPAND "seq_map" -1 1) (("3" (REWRITE "next") (("3" (REWRITE "seq_map" :DIR RL) (("3" (EXPAND "seq_map_struct") (("3" (ASSERT) (("3" (LIFT-IF) (("3" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))))))) ("4" (ASSERT) NIL))))))))))))))))))))))))))))))) ("2" (LEMMA "not_bot_next[final_obj]") (("2" (INST -1 "x1!1") (("2" (ASSERT) (("2" (SKOSIMP) (("2" (CASE "bot?(next(l1!1))") (("1" (REWRITE "empty_unique[[A,B]]") (("1" (HIDE -5 -3) (("1" (REWRITE "seq_map_empty[[A,B],A]") (("1" (REWRITE "shape_empty") (("1" (HIDE -1 1) (("1" (REPLACE -1) (("1" (CASE "next(cons_seq(a!1, y!1)) = next(empty_seq[final_obj])") (("1" (REWRITE "next_cons") (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))) ("2" (REPLACE -2 1) (("2" (PROPAX) NIL))))))))))))))))) ("2" (LEMMA "not_bot_next[[A,B]]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (REPLACE -1 -5) (("2" (REWRITE "seq_map_cons[[A,B],B]") (("2" (REWRITE "shape_cons") (("2" (CASE "next(x2!1) = next(cons_seq(star, shape(seq_map((LAMBDA (x: [A, B]): PROJ_2(x)))(y!2))))") (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))) ("2" (REPLACE -5) (("2" (PROPAX) NIL))))))))))))))))))))))))))))) ("3" (REPLACE -1 1) (("3" (REPLACE -2 1) (("3" (CASE "star = PROJ_1(down(next(shape(seq_map[[A, B], B]((LAMBDA (x: [A, B]): PROJ_2(x)))(l1!1)))))") (("1" (REPLACE -1 1 RL) (("1" (CASE "star = PROJ_1(down(next(shape(seq_map[[A, B], A]((LAMBDA (x: [A, B]): PROJ_1(x)))(l1!1)))))") (("1" (REPLACE -1 1 RL) (("1" (PROPAX) NIL))) ("2" (HIDE 2 3) (("2" (ASSERT) NIL))) ("3" (ASSERT) NIL))))) ("2" (ASSERT) NIL) ("3" (ASSERT) (("3" (ASSERT) NIL))))))))) ("4" (INST 1 "proj_2(down(next(l1!1)))") (("1" (ASSERT) (("1" (PROP) (("1" (REPLACE -1 1) (("1" (EXPAND "shape" 1 1) (("1" (EXPAND "seq_map" 1 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (EXPAND "seq_map" 1 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (CASE "not(bot?(next(l1!1)))") (("1" (ASSERT) (("1" (EXPAND "seq_map" 2 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (REWRITE "shape" :DIR RL) (("1" (EXPAND "seq_map" 2 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (PROPAX) NIL))))))))))))))))))))) ("2" (HIDE 1) (("2" (LEMMA "not_bot_next[final_obj]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (HIDE -3 1 2) (("2" (REPLACE -1) (("2" (CASE "next(cons_seq(a!1, y!1)) = next(shape(seq_map[[A, B], B]((LAMBDA (x: [A, B]): PROJ_2(x)))(l1!1)))") (("1" (REWRITE "next_cons") (("1" (HIDE -4) (("1" (EXPAND "shape") (("1" (EXPAND "seq_map" -1 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (EXPAND "seq_map" -1 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (PROPAX) NIL))))))))))))))))))))))) ("2" (REPLACE -3 1) (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))))) ("2" (REPLACE -2 1) (("2" (CASE "not(bot?(next(l1!1)))") (("1" (LEMMA "not_bot_next[[A,B]]") (("1" (INST?) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (REPLACE -1) (("1" (REWRITE "seq_map_cons[[A,B],B]") (("1" (REWRITE "shape_cons") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))))))))))))))))))) ("2" (LEMMA "not_bot_next[final_obj]") (("2" (INST?) (("2" (ASSERT) (("2" (HIDE 1 2 3 -3) (("2" (SKOSIMP) (("2" (REPLACE -1) (("2" (CASE "next(cons_seq(a!1, y!1)) = next(shape(seq_map[[A, B], B]((LAMBDA (x: [A, B]): PROJ_2(x)))(l1!1)))") (("1" (HIDE -4) (("1" (REWRITE "next_cons") (("1" (EXPAND "shape") (("1" (EXPAND "seq_map" -1 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (EXPAND "seq_map" -1 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (PROPAX) NIL))))))))))))))))))))))) ("2" (REPLACE -3) (("2" (PROPAX) NIL))))))))))))))))))))))))) ("2" (LEMMA "not_bot_next[final_obj]") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (HIDE -2 2 3) (("2" (REPLACE -1) (("2" (CASE "next(cons_seq(a!1, y!1)) = next(shape(seq_map[[A, B], B]((LAMBDA (x: [A, B]): PROJ_2(x)))(l1!1)))") (("1" (HIDE -3) (("1" (REWRITE "next_cons") (("1" (EXPAND "shape") (("1" (EXPAND "seq_map" -1 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (EXPAND "seq_map" -1 1) (("1" (REWRITE "next") (("1" (REWRITE "seq_map" :DIR RL) (("1" (EXPAND "seq_map_struct") (("1" (PROPAX) NIL))))))))))))))))))))))) ("2" (REPLACE -2) (("2" (PROPAX) NIL))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))) (|zip_inv_cons| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (EXPAND "zip_inv") (("1" (REWRITE "seq_map_cons[[A,B],A]") NIL))) ("2" (EXPAND "zip_inv") (("2" (REWRITE "seq_map_cons[[A,B],B]") NIL))))))) (|zip_iso_left| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (LEMMA "bisim_finality[A,Seq[A],Seq[A]]") (("1" (INST -1 "next" "next" "PROJ_1(zip_inv(zip(x!1)))" "PROJ_1(x!1)") (("1" (PROP) (("1" (EXPAND "Kernel") (("1" (REWRITE "id_coreduce" :DIR RL) (("1" (REWRITE "id_coreduce" :DIR RL) NIL))))) ("2" (HIDE 1 3) (("2" (EXPAND "bisim?") (("2" (INST 1 "{l,k: Seq[A] | EXISTS (x: (equal_shape)): PROJ_1(zip_inv(zip(x)))=l AND PROJ_1(x)=k}") (("2" (EXPAND "bisimulation?") (("2" (PROP) (("1" (SKOSIMP) (("1" (SKOSIMP) (("1" (ASSERT) (("1" (PROP) (("1" (EXPAND "zip_inv") (("1" (USE "zip_cons_left") (("1" (ASSERT) (("1" (REPLACE -1 -3) (("1" (REWRITE "seq_map_cons[[A,B],A]") (("1" (CASE "next(cons_seq(PROJ_1(down(next(PROJ_1(x!2)))), seq_map((LAMBDA (x: [A, B]): PROJ_1(x))) (zip(PROJ_2(down(next(PROJ_1(x!2)))), PROJ_2(down(next(PROJ_2(x!2))))))))=next(x1!1)") (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL) ("3" (USE "next_equal_bot") (("3" (ASSERT) NIL))))) ("2" (USE "next_equal_shape") (("2" (ASSERT) NIL))) ("3" (USE "next_equal_bot") (("3" (ASSERT) NIL))))))))))))) ("2" (EXPAND "zip_inv") (("2" (USE "zip_empty_right") (("2" (ASSERT) (("2" (USE "next_equal_bot") (("2" (ASSERT) (("2" (REWRITE "empty_unique[[A,B]]") (("2" (REWRITE "seq_map_empty[[A,B],A]") (("2" (ASSERT) (("2" (REPLACE -4 1 RL) (("2" (REWRITE "next_empty") (("2" (REWRITE "next_empty[A]") (("2" (ASSERT) NIL))))))))))))))))))))))) ("3" (REPLACE -1 + RL) (("3" (REPLACE -2 + RL) (("3" (EXPAND "zip_inv") (("3" (REWRITE-DESTR "next" "seq_map" 1) (("3" (REWRITE-DESTR "next" "zip" 1) NIL))))))))) ("4" (INST 1 "(proj_2(down(next(proj_1(x!2)))),proj_2(down(next(proj_2(x!2)))))") (("1" (EXPAND "zip_inv") (("1" (REPLACE -1 + RL) (("1" (REPLACE -2 + RL) (("1" (HIDE -1 -2) (("1" (REWRITE-DESTR "next" "seq_map" 3) (("1" (LIFT-IF) (("1" (ASSERT) (("1" (PROP) (("1" (REWRITE-DESTR "next" "seq_map" 2) (("1" (EXPAND "zip") (("1" (REWRITE "next") (("1" (REWRITE "zip" :DIR RL) (("1" (EXPAND "zip_struct") (("1" (PROPAX) NIL))))))))))))))))))))))))))) ("2" (USE "next_equal_shape") (("2" (ASSERT) NIL))) ("3" (ASSERT) (("3" (REPLACE -2 + RL) (("3" (USE "next_equal_bot") (("3" (ASSERT) NIL))))))) ("4" (ASSERT) NIL))))))))))) ("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))) ("2" (LEMMA "bisim_finality[B,Seq[B],Seq[B]]") (("2" (INST -1 "next" "next" "PROJ_2(zip_inv(zip(x!1)))" "PROJ_2(x!1)") (("2" (PROP) (("1" (EXPAND "Kernel") (("1" (REWRITE "id_coreduce" :DIR RL) (("1" (REWRITE "id_coreduce" :DIR RL) NIL))))) ("2" (HIDE 1 3) (("2" (EXPAND "bisim?") (("2" (INST 1 "{l,k: Seq[B] | EXISTS (x: (equal_shape)): PROJ_2(zip_inv(zip(x)))=l AND PROJ_2(x)=k}") (("2" (PROP) (("1" (EXPAND "bisimulation?") (("1" (SKOSIMP) (("1" (SKOSIMP) (("1" (ASSERT) (("1" (EXPAND "zip_inv") (("1" (PROP) (("1" (USE "zip_cons_right") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (REWRITE "seq_map_cons[[A,B],B]") (("1" (CASE "next(cons_seq(PROJ_1(down(next(PROJ_2(x!2)))), seq_map((LAMBDA (x: [A, B]): PROJ_2(x))) (zip(PROJ_2(down(next(PROJ_1(x!2)))), PROJ_2(down(next(PROJ_2(x!2))))))))= next(x1!1)") (("1" (HIDE -4) (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL) ("3" (USE "next_equal_bot") (("3" (ASSERT) NIL))))) ("2" (USE "next_equal_shape") (("2" (ASSERT) NIL))) ("3" (USE "next_equal_bot") (("3" (ASSERT) NIL))))))))))) ("2" (ASSERT) (("2" (REPLACE -2 1 RL) (("2" (REWRITE-DESTR "next" "seq_map" 1) (("2" (LIFT-IF) (("2" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (REWRITE-DESTR "next" "zip" 1) (("2" (REPLACE -3 1) (("2" (LEMMA "next_equal_bot") (("2" (INST -1 "x!2") (("2" (ASSERT) NIL))))))))))))))))))))) ("3" (REPLACE -1 + RL) (("3" (REPLACE -2 + RL) (("3" (REWRITE-DESTR "next" "seq_map" 3) (("3" (LIFT-IF) (("3" (PROP) (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (HIDE 2) (("2" (REWRITE-DESTR "next" "seq_map" 2) (("2" (REWRITE-DESTR "next" "zip" 2) (("2" (LEMMA "next_equal_bot") (("2" (INST -1 "x!2") (("2" (ASSERT) NIL))))))))))))))))))))))) ("4" (INST 1 "(proj_2(down(next(proj_1(x!2)))),proj_2(down(next(proj_2(x!2)))))") (("1" (ASSERT) (("1" (LEMMA "next_equal_bot") (("1" (INST -1 "x!2") (("1" (ASSERT) (("1" (REPLACE -2 + RL) (("1" (REPLACE -1 2 RL) (("1" (REWRITE-DESTR "next[B,Seq[[A,B]]]" "seq_map" 2) (("1" (REWRITE-DESTR "next" "zip" 2) (("1" (REWRITE-DESTR "next[[A,B],(equal_shape)]" "zip" 2) NIL))))))))))))))))) ("2" (USE "next_equal_shape") (("2" (ASSERT) NIL))) ("3" (USE "next_equal_bot") (("3" (ASSERT) NIL))) ("4" (USE "next_equal_bot") (("4" (ASSERT) NIL))))))))))))))))) ("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))) (|zip_iso_right| "" (SKOSIMP) (("" (LEMMA "bisim_finality[[A,B],Seq[[A,B]],Seq[[A,B]]]") (("" (INST -1 "next" "next" "zip(zip_inv(l!1))" "l!1") (("" (PROP) (("1" (EXPAND "Kernel") (("1" (REWRITE "id_coreduce" :DIR RL) (("1" (REWRITE "id_coreduce" :DIR RL) NIL))))) ("2" (HIDE 1 3) (("2" (EXPAND "bisim?") (("2" (INST 1 "{l,k:Seq[[A, B]] | zip(zip_inv(k)) = l}") (("2" (PROP) (("1" (EXPAND "bisimulation?") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (PROP) (("1" (LEMMA "not_bot_next[[A,B]]") (("1" (INST -1 "x2!1") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (REPLACE -1 -3) (("1" (REWRITE "zip_inv_cons") (("1" (REWRITE "zip_cons") (("1" (CASE "next(cons_seq((PROJ_1(a!1), PROJ_2(a!1)), zip(PROJ_1(zip_inv(y!1)), PROJ_2(zip_inv(y!1))))) = next(x1!1)") (("1" (REWRITE "next_cons") (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL))) ("2" (CASE "(PROJ_1(zip_inv(y!1)), PROJ_2(zip_inv(y!1))) = zip_inv(y!1)") (("1" (REPLACE -1 1) (("1" (TYPEPRED "zip_inv(y!1)") (("1" (PROPAX) NIL))))) ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))))))))))))))) ("2" (REWRITE "empty_unique") (("2" (EXPAND "zip_inv") (("2" (REWRITE "seq_map_empty[[A,B],A]") (("2" (REWRITE "seq_map_empty[[A,B],B]") (("2" (USE "zip_empty_left") (("1" (ASSERT) (("1" (REWRITE "next_empty") (("1" (ASSERT) NIL))))) ("2" (EXPAND "equal_shape") (("2" (REWRITE "shape_empty") (("2" (REWRITE "shape_empty") NIL))))))))))))))) ("3" (REPLACE -1 1 RL) (("3" (HIDE -1) (("3" (LEMMA "not_bot_next[[A,B]]") (("3" (INST -1 "x2!1") (("3" (ASSERT) (("3" (SKOSIMP) (("3" (REPLACE -1 1) (("3" (REWRITE "next_cons") (("3" (ASSERT) (("3" (REWRITE "zip_inv_cons") (("3" (REWRITE "zip_cons") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))) ("2" (CASE "(PROJ_1(zip_inv(y!1)), PROJ_2(zip_inv(y!1))) = zip_inv(y!1)") (("1" (REPLACE -1) (("1" (TYPEPRED "zip_inv(y!1)") (("1" (PROPAX) NIL))))) ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))) ("2" (CASE "(PROJ_1(zip_inv(y!1)), PROJ_2(zip_inv(y!1))) = zip_inv(y!1)") (("1" (REPLACE -1) (("1" (TYPEPRED "zip_inv(y!1)") (("1" (PROPAX) NIL))))) ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))))))))))))))))))))))) ("4" (LEMMA "not_bot_next[[A,B]]") (("4" (INST-CP -1 "x1!1") (("4" (ASSERT) (("4" (SKOSIMP) (("4" (INST -1 "x2!1") (("4" (ASSERT) (("4" (SKOSIMP) (("4" (HIDE 2 3) (("4" (REPLACE -1) (("4" (REPLACE -2) (("4" (HIDE -1 -2) (("4" (REWRITE "next_cons") (("4" (REWRITE "next_cons") (("4" (ASSERT) (("4" (REWRITE "zip_inv_cons") (("4" (REWRITE "zip_cons") (("1" (CASE "next(cons_seq((PROJ_1(a!2), PROJ_2(a!2)), zip(PROJ_1(zip_inv(y!2)), PROJ_2(zip_inv(y!2)))))= next(cons_seq(a!1, y!1))") (("1" (REWRITE "next_cons") (("1" (REWRITE "next_cons") (("1" (ASSERT) (("1" (HIDE -2) (("1" (LEMMA "mono_up[[[A,B],Seq[[A,B]]]]") (("1" (INST -1 "((PROJ_1(a!2), PROJ_2(a!2)), zip(PROJ_1(zip_inv(y!2)), PROJ_2(zip_inv(y!2))))" "(a!1, y!1)") (("1" (ASSERT) (("1" (PROP) (("1" (REPLACE -2 1 RL) (("1" (CASE "(PROJ_1(zip_inv(y!2)), PROJ_2(zip_inv(y!2)))=zip_inv(y!2)") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (PROPAX) NIL))))) ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))))))))))))))))))) ("2" (CASE "(PROJ_1(zip_inv(y!2)), PROJ_2(zip_inv(y!2)))=zip_inv(y!2)") (("1" (TYPEPRED "zip_inv(y!2)") (("1" (ASSERT) NIL))) ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))) ("2" (CASE "(PROJ_1(zip_inv(y!2)), PROJ_2(zip_inv(y!2)))=zip_inv(y!2)") (("1" (REPLACE -1) (("1" (TYPEPRED "zip_inv(y!2)") (("1" (PROPAX) NIL))))) ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL))))))))))))))))))))))))))))))))))))))))))) ("2" (ASSERT) NIL))))))))))))))))) (|zip_mono| "" (SKOSIMP) (("" (CASE "zip_inv(zip(x!1))=zip_inv(zip(y!1))") (("1" (REWRITE "zip_iso_left") (("1" (REWRITE "zip_iso_left") NIL))) ("2" (ASSERT) NIL))))))