mod Ex09 logic: 'cl'

rem 
  \para \bf  9. CVIČENIE Z PREDMETU LOGIKA PRE INFORMATIKOV 2  \end 
  \para* http://ii.fmph.uniba.sk/cl/courses/lpi2/ex/ex09.cl 

rem 
  \para* \it  Dátum:  \end štvrtok 2. 12. 2004 
  \para* \it  Odporúčaná verzia CL:  \end 5.81.16 
  \para* \it  WWW stránka predmetu:  \end 
  http://ii.fmph.uniba.sk/cl/courses/lpi2?lang=sk 
  \para* \it  Kontakt na cvičiaceho:  \end mailto:kluka@fmph.uniba.sk 

rem 
  \para Preskočte nasledujúce komponenty až po nadpis "Cvičenia". 

appldisp/1 Dlp_d
  Subsup(Num('2',0),75,None,Fenced(Op(Ent('mid'),0),Arg(0),Op(Ent('mid'),0)))

appldisp/2 Dconc_d
  Infix(Arg(0),34,1,Op(Ent('star'),0),Arg(1))

appldisp/3 Split_d
  Infix(Arg(0),25,1,Op(Ent('doteq'),0),
        Fenced(Op('[',0),Frac(Arg(1),0,Arg(2)),Op(']',0)))

appldisp/2 Conc_d
  Infix(Arg(0),35,1,Op(Ent('boxplus'),0),Arg(1))

appldisp/2 Cons_d
  Infix(Arg(0),30,2,Op(';',0),Arg(1))

appldisp/2 Tail_d
  Infix(Arg(0),25,1,Op(Ent('sqsube'),0),Arg(1))

appldisp/2 Inlist_d
  Infix(Arg(0),25,0,Op(Ent('isin'),0),Arg(1))

appldisp/4 Lb_d
  Infix(Prefix(90,2,Subsup(Id(2,'g',0),75,None,Op(Ent('lowast'),0)),
               Fenced(Op('(',0),
                      Infix(Arg(0),30,2,Op(',',0),
                            Infix(Arg(1),30,2,Op(',',0),Arg(2))),Op(')',0))),25,0,
        Subsup(Op('=',0),75,None,Op(Ent('bull'),0)),Arg(3))

appldisp/1 Ms_d
  Prefix(90,2,Id(0,Ent('mu'),0),Arg(0))

appldisp/3 G_d
  Std('g',0)

appldisp/4 G_gnit_d
  Infix(Prefix(90,2,Subsup(Id(2,'g',0),75,None,Op(Ent('lowast'),0)),
               Fenced(Op('(',0),
                      Infix(Arg(0),30,2,Op(',',0),
                            Infix(Arg(1),30,2,Op(',',0),Arg(2))),Op(')',0))),25,0,
        Op(Ent('doteq'),0),Arg(3))

appldisp/3 Gnit_d
  Prefix(90,2,Subsup(Id(1,'g',0),75,None,Op(Ent('lowast'),0)),
         Fenced(Op('(',0),
                Infix(Arg(0),30,2,Op(',',0),Infix(Arg(1),30,2,Op(',',0),Arg(2))),
                Op(')',0)))

theory Dconcat

rem 
  \para Nasledujúce tvrdenia ste dokázali v minulom cvičení. 

fun Dlp 'Dlp_d'
  Dlp(0) = 1
  Dlp S1(x) = 2*Dlp(x)
  Dlp S2(x) = 2*Dlp(x)

fun/2 Dconc 'Dconc_d'
  Dconc(x,0) = x
  Dconc(x,S1(y)) = S1 Dconc(x,y)
  Dconc(x,S2(y)) = S2 Dconc(x,y)

pred/3 Split 'Split_d'
  Split(t,v,m) <-> 
    t = Dconc(v,m) & \e w\e i(v = Dconc(w,i) & Dlp(i) <= 2 & Dlp(w) = Dlp(m))

rem 
  \para \bf  Dyadic Pairing and List Concatenation Functions in PA  \end 

rem 
  \para \it  Adjustment of atoms  \end 

fun Adj 
  Adj(t) = \m s 
    [ \e v1\e v2\e m\e y(Split(t,Dconc(v1,v2),Dconc(S0(m),Dlp(y)-1)) & 
                         Dlp(v1) = Dlp S0(m) & Split(s,v1,S0(m))) ]

axiom Adj0
  Adj(0) = 0

rem 
  \para \it  Introduction of a dyadic list concatenation function into PA  \end 

fun/2 Conc 'Conc_d'
  Conc(s,t) = \m u 
    [ \a v1\a v2\a m1\a m2(Split(Adj(s),v1,m1) & Split(t,v2,m2) -> 
                           Split(u,Dconc(v1,v2),Dconc(m1,m2))) ]

axiom Conc_assoc
  Conc(s,Conc(t,u)) = Conc(Conc(s,t),u)

rem 
  \para \it  Introduction of a dyadic pairing function into PA  \end 

fun/2 Cons 'Cons_d'
  Cons(x,t) = \m s [ s = Conc(Dconc(x+1,Dlp(x+1)),t) ]

axiom Cons_unique
  Cons(x1,t1) = Cons(x2,t2) -> x1 = x2 & t1 = t2

axiom Dlist_case
  Adj(t) = 0 \/ \e x\e s t = Cons(x,s)

axiom Adj_cons_pos
  Adj Cons(x,t) > 0

rem 
  \para \it  Towards admissibility of pair induction  \end 

axiom Cons_less
  x < Cons(x,t) & t < Cons(x,t)

rem 
  \para \it  Recurrences for dyadic list concatenation  \end 

axiom Conc_atom
  Adj(s) = 0 -> Conc(s,t) = t

axiom Conc_cons
  Conc(Cons(x,s),t) = Cons(x,Conc(s,t))

rem 
  \para \it  Tails of dyadic lists  \end 

pred/2 Tail 'Tail_d'
  Tail(s,t) <-> \e u Conc(u,s) = t

axiom Tail_refl
  Tail(s,s)

axiom Tail_trans
  Tail(t,s) & Tail(s,r) -> Tail(t,r)

axiom Tail_b
  Adj(s) = 0 -> Tail(t,s) <-> t = s

axiom Tail_i
  Tail(t,Cons(x,s)) <-> t = Cons(x,s) \/ Tail(t,s)

rem 
  \para \it  Membership in dyadic lists  \end 

pred/2 Inlist 'Inlist_d'
  Inlist(x,t) <-> \e sTail(Cons(x,s),t)

axiom Inlist_cons
  Inlist(x,Cons(x,s))

axiom Inlist_conc
  Inlist(x,s) -> Inlist(x,Conc(s,t)) & Inlist(x,Conc(t,s))

lemma Nb_case
  \e y x = S0(y) \/ \e y x = S1(y)
proof 
 ind N; x @ 0; x
  inst* \e y y = 0; 0 proved.
  split \e y x = S0(y) \/ \e y x = S1(y).4,0,0,0
   proved
   eigen \e y x = S1(y); y
    inst* \e y1 y+1 = y1; y+1 proved.....

rem 
  \para \bf  C V I Č E N I A  \end 

rem 
  \para \bf  Closure of PA under a Schema of Nested Iteration  \end 
  \para* http://ii.fmph.uniba.sk/cl/courses/lpi2/lect/pa.pdf#section.1.6 

theory Nested_iteration

rem 
  \para \it  Schema of nested iteration  \end 

fun/0 C 

fun/3 G 'G_d'

fun Ms 'Ms_d'

axiom Measure_major
  G(x,n,a) = S1(y) -> Ms(y) < Ms(x)

axiom Count
  \e y G(x,0,a) = S0(y)

rem 
  \para \it  Arithmetization of computation trees  \end 

fun/4 Lb 'Lb_d'
  Lb(n,x,a,y) = Cons(n,Cons(x,Cons(a,y)))

pred/5 Lcond 
  Lcond(x,n,a,y,t) <-> 
    \e v(G(x,n,a) = S0(v) & y = v \/ 
         \e m\e w(G(x,n,a) = S1(v) & n = m+1 & Inlist(Lb(v,C,0,w),t) & 
                  Inlist(Lb(x,m,Conc(a,Cons(w,0)),y),t)))

pred Ct 
  Ct(s) <-> 
    \a x\a n\a a\a y\a t(Tail(Cons(Lb(x,n,a,y),t),s) -> Lcond(x,n,a,y,t))

lemma Lcond_conc
  Lcond(x,n,a,y,s) -> Lcond(x,n,a,y,Conc(s,t))
proof 
 use Lcond.2,0,0; x; n; a; y; s
  split \e v(G(x,n,a) = S0(v) & y = v) \/ 
        \e v(\e m(\e w(Inlist(Cons(v,Cons(C,Cons(0,w))),s) & 
                       Inlist(Cons(x,Cons(m,Cons(Conc(a,Cons(w,0)),y))),s)) & 
                  n = m+1) & G(x,n,a) = S1(v)).4,0,0,0
   eigen \e v(G(x,n,a) = S0(v) & y = v).0; v
    use Lcond.2,1,0:0; x; n; a; v; Conc(s,t)
     split \e v1 v = v1 -> Lcond(x,n,a,v,Conc(s,t)).2,1,0
      inst* \e v1 v = v1; y proved.
      proved...
   eigen \e v(\e m(\e w(Inlist(Cons(v,Cons(C,Cons(0,w))),s) & 
                        Inlist(Cons(x,Cons(m,Cons(Conc(a,Cons(w,0)),y))),s)) & 
                   n = m+1) & G(x,n,a) = S1(v)).0:0,3,(0,3,0,1,0),1,0; v,m,w
    use Inlist_conc.0; Lb(v,C,0,w); s; t
     use Inlist_conc.0; Lb(x,m,Conc(a,Cons(w,0)),y); s; t
      use Lcond.2,1,0:0; x; n; a; y; Conc(s,t)
       split \e v1(\e m1(\e w(Inlist(Cons(v1,Cons(C,Cons(0,w))),Conc(s,t)) & 
                              Inlist(Cons(x,Cons(m1,Cons(Conc(a,Cons(w,0)),y))),
                                     Conc(s,t))) & m = m1) & v = v1) -> 
             Lcond(x,m+1,a,y,Conc(s,t)).2,1,0
        inst* \e v1(\e m1(\e w(Inlist(Cons(v1,Cons(C,Cons(0,w))),Conc(s,t)) & 
                               Inlist(Cons(x,Cons(m1,Cons(Conc(a,Cons(w,0)),y))),
                                      Conc(s,t))) & m = m1) & v = v1):0,3,
                                                                      (0,3,0,1,0),
                                                                      1,0; v; m; w proved.
        proved........

thm Ct_tail
  Ct(s) & Tail(t,s) -> Ct(t)
proof 
 use Ct.2,1,0; t
  split \a x\a n\a a\a y\a t1(Tail(Cons(Cons(x,Cons(n,Cons(a,y))),t1),t) -> 
                              Lcond(x,n,a,y,t1)) -> Ct(t).2,1,0
   eigen* \a x\a n\a a\a y\a t1(Tail(Cons(Cons(x,Cons(n,Cons(a,y))),t1),t) -> 
                                Lcond(x,n,a,y,t1)).0; x,n,a,y,u
    use Tail_trans; Cons(Lb(x,n,a,y),u); t; s
     use Ct.2,0,0:0,2,1,0; s; x; n; a; y; u proved...
   proved...

thm Ct_atom
  Adj(s) = 0 -> Ct(s)
proof 
 use Ct.2,1,0; s
  split \a x\a n\a a\a y\a t(Tail(Cons(Cons(x,Cons(n,Cons(a,y))),t),s) -> 
                             Lcond(x,n,a,y,t)) -> Ct(s).2,1,0
   eigen* \a x\a n\a a\a y\a t(Tail(Cons(Cons(x,Cons(n,Cons(a,y))),t),s) -> 
                               Lcond(x,n,a,y,t)).0; x,n,a,y,t
    use Tail_b.1,0,2,0,0; s; Cons(Lb(x,n,a,y),t)
     use Adj_cons_pos; Lb(x,n,a,y); t proved...
   proved...

thm Ct_bad
  \a x\a n\a a\a y b != Lb(x,n,a,y) -> Ct Cons(b,s) <-> Ct(s)
proof 
 split* Ct Cons(b,s) <-> Ct(s).2,0,0
  use Tail_refl; s
   use Tail_i.2,1,0; s; b; s
    use Ct_tail; Cons(b,s); s proved...
  use Ct.2,1,0; Cons(b,s)
   split \a x\a n\a a\a y\a t(Tail(Cons(Cons(x,Cons(n,Cons(a,y))),t),Cons(b,s)) -> 
                              Lcond(x,n,a,y,t)) -> Ct Cons(b,s).2,1,0
    eigen* \a x\a n\a a\a y\a t(Tail(Cons(Cons(x,Cons(n,Cons(a,y))),t),Cons(b,s)) -> 
                                Lcond(x,n,a,y,t)).0; x,n,a,y,t
     use Tail_i.2,0,0; Cons(Lb(x,n,a,y),t); b; s
      split Cons(Cons(x,Cons(n,Cons(a,y))),t) = Cons(b,s) \/ 
            Tail(Cons(Cons(x,Cons(n,Cons(a,y))),t),s).4,0,0,0
       use Cons_unique.0; Lb(x,n,a,y); t; b; s
        inst \a x1\a n1\a a1\a y1 b != Cons(x1,Cons(n1,Cons(a1,y1))); x; n; a; y proved..
       exp Ct; s
        inst \a x1\a n1\a a1\a y1\a t1(Tail(Cons(Cons(x1,Cons(n1,Cons(a1,y1))),
                                                 t1),s) -> Lcond(x1,n1,a1,y1,t1)); x; n; a; y; t proved.....
    proved....

thm Ct_cons
  Ct Cons(Lb(x,n,a,y),s) <-> Lcond(x,n,a,y,s) & Ct(s)
proof 
 split* Ct Cons(Cons(x,Cons(n,Cons(a,y))),s) <-> Lcond(x,n,a,y,s) & Ct(s).2,0,0
  use Tail_refl; Cons(Lb(x,n,a,y),s)
   use Ct.2,0,0:0,2,1,0; Cons(Lb(x,n,a,y),s); x; n; a; y; s
    use Tail_refl; s
     use Tail_i.2,1,0; s; Lb(x,n,a,y); s
      use Ct_tail; Cons(Lb(x,n,a,y),s); s proved.....
  use Ct.2,1,0; Cons(Lb(x,n,a,y),s)
   split \a x1\a n1\a a1\a y1\a t(Tail(Cons(Cons(x1,Cons(n1,Cons(a1,y1))),t),
                                       Cons(Cons(x,Cons(n,Cons(a,y))),s)) -> 
                                  Lcond(x1,n1,a1,y1,t)) -> 
         Ct Cons(Cons(x,Cons(n,Cons(a,y))),s).2,1,0
    eigen* \a x1\a n1\a a1\a y1\a t(Tail(Cons(Cons(x1,Cons(n1,Cons(a1,y1))),t),
                                         Cons(Cons(x,Cons(n,Cons(a,y))),s)) -> 
                                    Lcond(x1,n1,a1,y1,t)).0; x1,n1,a1,y1,t
     use Tail_i.2,0,0; Cons(Lb(x1,n1,a1,y1),t); Lb(x,n,a,y); s
      split Cons(Cons(x1,Cons(n1,Cons(a1,y1))),t) = 
            Cons(Cons(x,Cons(n,Cons(a,y))),s) \/ 
            Tail(Cons(Cons(x1,Cons(n1,Cons(a1,y1))),t),s).4,0,0,0
       use Cons_unique.0; Lb(x1,n1,a1,y1); t; Lb(x,n,a,y); s
        use Cons_unique.0; x1; Cons(n1,Cons(a1,y1)); x; Cons(n,Cons(a,y))
         use Cons_unique.0; n1; Cons(a1,y1); n; Cons(a,y)
          use Cons_unique.0; a1; y1; a; y proved....
       use Ct.2,0,0:0,2,1,0; s; x1; n1; a1; y1; t proved....
    proved....

thm Ct_conc
  Ct(s) & Ct(t) -> Ct Conc(s,t)
proof 
 indm s @ s1
  use Dlist_case; s
   split Adj(s) = 0 \/ \e x\e s1 s = Cons(x,s1).4,0,0,0
    use Conc_atom; s; t proved.
    eigen \e x\e s1 s = Cons(x,s1); b,u
     use Cons_less.0; b; u
      inst \a s1(s1 < Cons(b,u) -> Ct(s1) -> Ct Conc(s1,t)); u
       use Conc_cons; b; u; t
        cut \a x\a n\a a\a y b != Lb(x,n,a,y)
         use Ct_bad.1,0,2,1,0; b; Conc(u,t)
          use Ct_bad.1,0,2,0,0; b; u proved..
         inv ~\a x\a n\a a\a y b != Cons(x,Cons(n,Cons(a,y)))
          eigen* \a x\a n\a a\a y b != Cons(x,Cons(n,Cons(a,y))); x,n,a,y
           inv* b != Cons(x,Cons(n,Cons(a,y)))
            use Tail_refl; s
             use Ct.2,0,0:0,2,1,0; s; x; n; a; y; u
              use Lcond_conc; x; n; a; y; u; t
               use Ct_cons.2,1,0; x; n; a; y; Conc(u,t)
                use Ct_cons.2,0,1,0,4,1,0; x; n; a; y; u proved.................

rem 
  \para \it  Introduction of graph of the nested iteration function into PA 
   \end 

pred/4 G_gnit 'G_gnit_d'
  G_gnit(x,n,a,y) <-> \e tCt Cons(Lb(x,n,a,y),t)

lemma Ct_inlist
  Ct(s) & Inlist(Lb(x,n,a,y),s) -> G_gnit(x,n,a,y)
proof 
 exp Inlist; Cons(x,Cons(n,Cons(a,y))),s
  eigen \e s1Tail(Cons(Cons(x,Cons(n,Cons(a,y))),s1),s); u
   use Ct_tail; s; Cons(Lb(x,n,a,y),u)
    use G_gnit.0; x; n; a; y
     inst* \e tCt Cons(Cons(x,Cons(n,Cons(a,y))),t); u proved......

thm G_gnit1
  G(x,n,a) = S0(v) -> G_gnit(x,n,a,y) <-> y = v
proof 
 split* G_gnit(x,n,a,y) <-> y = v.2,0,0
  use G_gnit.2,0,0; x; n; a; y
   eigen \e tCt Cons(Cons(x,Cons(n,Cons(a,y))),t); t
    use Ct_cons.2,0,0; x; n; a; y; t
     use Lcond.2,0,0; x; n; a; y; t
      eigen \e v1(v = v1 & y = v1).0; v1 proved.....
  use Lcond.2,1,1,(4,0,0),0:0,2,0,1; x; n; a; v; 0
   split \e v1 v = v1 -> Lcond(x,n,a,v,0).2,1,0
    inst* \e v1 v = v1; v proved.
    use Adj0
     use Ct_atom; 0
      use Ct_cons.2,1,0; x; n; a; v; 0
       use G_gnit.2,1,0:0,2,0,1; x; n; a; v; 0 proved........

thm G_gnit2
  G(x,n+1,a) = S1(v) -> G_gnit(x,n+1,a,y) <-> 
  \e w(G_gnit(v,C,0,w) & G_gnit(x,n,Conc(a,Cons(w,0)),y))
proof 
 split* G_gnit(x,n+1,a,y) <-> 
        \e w(G_gnit(v,C,0,w) & G_gnit(x,n,Conc(a,Cons(w,0)),y)).2,0,0
  use G_gnit.2,0,0; x; n+1; a; y
   eigen \e tCt Cons(Cons(x,Cons(n+1,Cons(a,y))),t); s
    use Ct_cons.2,0,0; x; n+1; a; y; s
     use Lcond.2,0,0; x; n+1; a; y; s
      eigen \e v1(\e m(\e w(Inlist(Cons(v1,Cons(C,Cons(0,w))),s) & 
                            Inlist(Cons(x,Cons(m,Cons(Conc(a,Cons(w,0)),y))),s)) & 
                       n = m) & v = v1).0:0,3,(0,3,0,1,0),1,0; v1,m,w
       use Ct_inlist; s; v1; C; 0; w
        use Ct_inlist; s; x; m; Conc(a,Cons(w,0)); y
         inst* \e w(G_gnit(v1,C,0,w) & G_gnit(x,m,Conc(a,Cons(w,0)),y)); w proved........
  eigen \e w(G_gnit(v,C,0,w) & G_gnit(x,n,Conc(a,Cons(w,0)),y)).0; w
   use G_gnit.2,0,0; v; C; 0; w
    use G_gnit.2,0,0; x; n; Conc(a,Cons(w,0)); y
     eigen \e tCt Cons(Cons(v,Cons(C,Cons(0,w))),t); s
      eigen \e tCt Cons(Cons(x,Cons(n,Cons(Conc(a,Cons(w,0)),y))),t); t
       use Ct_conc; Cons(Lb(v,C,0,w),s); Cons(Lb(x,n,Conc(a,Cons(w,0)),y),t)
        let Conc(Cons(Lb(v,C,0,w),s),Cons(Lb(x,n,Conc(a,Cons(w,0)),y),t)); u
         use Inlist_cons; Lb(v,C,0,w); s
          use Inlist_conc.1,0,4,0,0; Lb(v,C,0,w); Cons(Lb(v,C,0,w),s); Cons(Lb(x,n,Conc(a,Cons(w,0)),y),t)
           use Inlist_cons; Lb(x,n,Conc(a,Cons(w,0)),y); t
            use Inlist_conc.1,0,4,1,0; Lb(x,n,Conc(a,Cons(w,0)),y); Cons(Lb(x,n,Conc(a,Cons(w,0)),y),t); Cons(Lb(v,C,0,w),s)
             use Lcond.2,1,1,(4,1,0),0:0,2,0,1; x; n+1; a; y; u; v; n; w
              use Ct_cons.2,1,0; x; n+1; a; y; u
               use G_gnit.2,1,0:0; x; n+1; a; y
                split \e tCt Cons(Cons(x,Cons(n+1,Cons(a,y))),t) -> 
                      G_gnit(x,n+1,a,y).2,1,0
                 inst* \e tCt Cons(Cons(x,Cons(n+1,Cons(a,y))),t); u proved.
                 proved.................

rem 
  \para \it  Introduction of the nested iteration function into PA  \end 

thm Gnit_exists
  \e yG_gnit(x,n,a,y)
proof 
 indm Ms(x)*C+n; a @ x1,n1
  use Nb_case; G(x,n,a)
   split \e y G(x,n,a) = S0(y) \/ \e y G(x,n,a) = S1(y).4,0,0,0
    eigen \e y G(x,n,a) = S0(y); v
     use G_gnit1.1,0,2,1,0; x; n; a; v; v
      inst* \e yG_gnit(x,n,a,y); v proved...
    eigen \e y G(x,n,a) = S1(y); v
     use Measure_major; x; n; a; v
      use Count; x; a
       cut n = 0
        proved
        let n-1; m
         let Ms(x)-Ms(v)-1; d
          weak \e y G(x,0,a) = S0(y)
           inst \a x1\a n1(n1+C*Ms(x1) <= d*C+m+C+C*Ms(v) -> 
                           \a a\e yG_gnit(x1,n1,a,y)):0,2,1,0; v; C; 0
            eigen \e yG_gnit(v,C,0,y); w
             inst \a x1\a n1(n1+C*Ms(x1) <= d*C+m+C+C*Ms(v) -> 
                             \a a\e yG_gnit(x1,n1,a,y)):0,2,1,0; x; m; Conc(a,Cons(w,0))
              eigen \e yG_gnit(x,m,Conc(a,Cons(w,0)),y); y
               use G_gnit2.1,0,2,1,0:0,2,1,2,0,1; x; m; a; v; y; w
                inst* \e yG_gnit(x,m+1,a,y); y proved.................

thm Gnit_unique
  G_gnit(x,n,a,y1) & G_gnit(x,n,a,y2) -> y1 = y2
proof 
 indm Ms(x)*C+n; a,y1,y2 @ x1,n1
  use Nb_case; G(x,n,a)
   split \e y G(x,n,a) = S0(y) \/ \e y G(x,n,a) = S1(y).4,0,0,0
    eigen \e y G(x,n,a) = S0(y); v
     use G_gnit1.1,0,2,0,0; x; n; a; v; y1
      use G_gnit1.1,0,2,0,0; x; n; a; v; y2 proved...
    eigen \e y G(x,n,a) = S1(y); v
     use Measure_major; x; n; a; v
      use Count; x; a
       eigen \e y G(x,0,a) = S0(y); y
        cut n = 0
         proved
         let n-1; m
          let Ms(x)-Ms(v)-1; d
           weak G(x,0,a) = S0(y)
            use G_gnit2.1,0,2,0,0; x; m; a; v; y1
             use G_gnit2.1,0,2,0,0; x; m; a; v; y2
              eigen \e w(G_gnit(v,C,0,w) & G_gnit(x,m,Conc(a,Cons(w,0)),y1)).0; w1
               eigen \e w(G_gnit(v,C,0,w) & G_gnit(x,m,Conc(a,Cons(w,0)),y2)).0; w2
                inst \a x1\a n1(n1+C*Ms(x1) <= d*C+m+C+C*Ms(v) -> 
                                \a a\a y1(G_gnit(x1,n1,a,y1) -> 
                                          \a y2(G_gnit(x1,n1,a,y2) -> y1 = y2))):0,
                                                                                 2,
                                                                                 1,
                                                                                 0,
                                                                                 2,
                                                                                 1,
                                                                                 0; v; C; 0; w1; w2
                 inst \a x1\a n1(n1+C*Ms(x1) <= d*C+m+C+C*Ms(v) -> 
                                 \a a\a y1(G_gnit(x1,n1,a,y1) -> 
                                           \a y2(G_gnit(x1,n1,a,y2) -> y1 = y2))):0,
                                                                                  2,
                                                                                  1,
                                                                                  0,
                                                                                  2,
                                                                                  1,
                                                                                  0; x; m; Conc(a,Cons(w2,0)); y1; y2 proved..................

fun/3 Gnit 'Gnit_d'
  Gnit(x,n,a) = \m y [ G_gnit(x,n,a,y) ]

thm Gnit1
  G(x,n,a) = S0(v) -> Gnit(x,n,a) = v
proof 
 use Gnit.4,0,0; x; n; a
  use G_gnit1.1,0,2,0,0; x; n; a; v; Gnit(x,n,a) proved...

thm Gnit2
  G(x,n,a) = S1(v) & n = m+1 & Gnit(v,C,0) = w & Gnit(x,m,Conc(a,Cons(w,0))) = y -> 
  Gnit(x,n,a) = y
proof 
 use Gnit.4,0,0; v; C; 0
  use Gnit.4,0,0; x; m; Conc(a,Cons(w,0))
   use G_gnit2.1,0,2,1,0:0,2,1,2,0,1; x; m; a; v; y; w
    use Gnit.4,0,0; x; n; a
     use Gnit_unique; x; n; a; Gnit(x,n,a); y proved......

end theory Nested_iteration

end theory Dconcat