%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                         %
%      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