diff --git a/src/pnf_sugared.rs b/src/pnf_sugared.rs
index f5a72d7..17828c1 100644
--- a/src/pnf_sugared.rs
+++ b/src/pnf_sugared.rs
@@ -3,6 +3,7 @@ use crate::{sugar::SugaredTypeTerm, SugaredEnumVariant, SugaredStructMember};
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
 pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< SugaredTypeTerm >  ) -> Vec< SugaredTypeTerm > {
+    // check for overlap
     for i in 0 .. upper.len() {
         if upper[i] == lower[0] {
             let mut result_ladder = Vec::<SugaredTypeTerm>::new();
@@ -12,6 +13,7 @@ pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< Sugare
         }
     }
 
+    // no overlap found, just concatenate ladders
     upper.append(&mut lower);
     upper
 }
@@ -24,132 +26,210 @@ impl SugaredTypeTerm {
     /// <Seq <Digit 10>>~<Seq Char>
     /// ⇒ <Seq <Digit 10>~Char>
     /// ```
-    pub fn param_normalize(mut self) -> Self {
-
+    pub fn normalize(mut self) -> Self {
+        eprintln!("normalize {:?}", self);
         match self {
             SugaredTypeTerm::Ladder(mut rungs) => {
-                if rungs.len() > 0 {
-                    let mut new_rungs = Vec::new();
-                    while let Some(bottom) = rungs.pop() {
-                        if let Some(last_but) = rungs.last_mut() {
-                            match (bottom, last_but) {
-                                (SugaredTypeTerm::Spec(bot_args), SugaredTypeTerm::Spec(last_args)) => {
-                                    if bot_args.len() == last_args.len() {
-                                        let mut new_rung_params = Vec::new();
-                                        let mut require_break = false;
+                if rungs.len() == 0 {
+                    return SugaredTypeTerm::unit();
+                } else if rungs.len() == 1 {
+                    return rungs.pop().unwrap().normalize();
+                }
 
-                                        if bot_args.len() > 0 {
-                                            todo!();
-                                            /*
-                                            if let Ok(_idx) =  last_args[0].is_syntactic_subtype_of(&bot_args[0]) {
-                                                for i in 0 .. bot_args.len() {
+                let mut new_rungs = Vec::new();
+                let mut r2 = rungs.pop().unwrap().strip();
+                while let Some(r1) = rungs.pop() {
+                    let r1 = r1.strip();
+                    match (r1.clone(), r2.clone()) {
+                        (SugaredTypeTerm::Seq { seq_repr: seq_repr1, items: items1 },
+                         SugaredTypeTerm::Seq { seq_repr: seq_repr2, items: items2 })
+                        => {
+                            eprintln!("popped two seq {:?} , {:?}", items1, items2);
+                            r2 = SugaredTypeTerm::Seq {
+                                    seq_repr:
+                                        if seq_repr1.is_some() || seq_repr2.is_some() {
+                                            let sr1 = if let Some(seq_repr1) = seq_repr1 { *seq_repr1.clone() }
+                                                        else { SugaredTypeTerm::unit() };
+                                            let sr2 = if let Some(seq_repr2) = seq_repr2 { *seq_repr2 }
+                                                        else { SugaredTypeTerm::unit() };
 
-                                                    let spliced_type_ladder = splice_ladders(
-                                                        last_args[i].clone().get_lnf_vec(),
-                                                        bot_args[i].clone().get_lnf_vec()
-                                                    );
-                                                    let spliced_type =
-                                                        if spliced_type_ladder.len() == 1 {
-                                                            spliced_type_ladder[0].clone()
-                                                        } else if spliced_type_ladder.len() > 1 {
-                                                            SugaredTypeTerm::Ladder(spliced_type_ladder)
-                                                        } else {
-                                                            SugaredTypeTerm::unit()
-                                                        };
-
-                                                    new_rung_params.push( spliced_type.param_normalize() );
-                                                }
-
-                                            } else {
-                                                new_rung_params.push(
-                                                    SugaredTypeTerm::Ladder(vec![
-                                                        last_args[0].clone(),
-                                                        bot_args[0].clone()
-                                                    ])//.normalize()
-                                                );
-
-                                                for i in 1 .. bot_args.len() {
-                                                    if let Ok(_idx) = last_args[i].is_syntactic_subtype_of(&bot_args[i]) {
-                                                        let spliced_type_ladder = splice_ladders(
-                                                            last_args[i].clone().get_lnf_vec(),
-                                                            bot_args[i].clone().get_lnf_vec()
-                                                        );
-                                                        let spliced_type =
-                                                            if spliced_type_ladder.len() == 1 {
-                                                                spliced_type_ladder[0].clone()
-                                                            } else if spliced_type_ladder.len() > 1 {
-                                                                SugaredTypeTerm::Ladder(spliced_type_ladder)
-                                                            } else {
-                                                                SugaredTypeTerm::unit()
-                                                            };
-
-                                                        new_rung_params.push( spliced_type.param_normalize() );
-                                                    } else {
-                                                        new_rung_params.push( bot_args[i].clone() );
-                                                        require_break = true;
-                                                    }
-                                                }
-                                            }
-                                            */
-                                        }
-
-                                        if require_break {
-                                            new_rungs.push( SugaredTypeTerm::Spec(new_rung_params) );
+                                            Some(Box::new(
+                                                if sr1 == sr2 {
+                                                    sr1
+                                                } else if sr1 == SugaredTypeTerm::unit() {
+                                                    sr2
+                                                } else {
+                                                    SugaredTypeTerm::Ladder(vec![ sr1, sr2 ]).normalize()
+                                                }))
                                         } else {
-                                            rungs.pop();
-                                            rungs.push(SugaredTypeTerm::Spec(new_rung_params));
-                                        }
+                                            None
+                                        },
+                                    items:
+                                        items1.into_iter()
+                                            .zip(items2.into_iter())
+                                            .map(|(item1, item2)| {
+                                                if item1 == item2 {
+                                                    item1
+                                                } else {
+                                                    SugaredTypeTerm::Ladder(vec![ item1.clone(), item2 ])
+                                                }
+                                            })
+                                            .collect()
+                                };
+                        }
 
-                                    } else {
-                                        new_rungs.push( SugaredTypeTerm::Spec(bot_args) );
-                                    }
-                                }
-                                (bottom, last_buf) => {
-                                    new_rungs.push( bottom );
-                                }
+                        (SugaredTypeTerm::Seq { seq_repr, items },
+                            SugaredTypeTerm::Spec( mut args )
+                        ) => {
+                            if args.len() == items.len()+1 {
+                                r2 = SugaredTypeTerm::Seq {
+                                    seq_repr: Some(Box::new(SugaredTypeTerm::Ladder(vec![
+                                        if let Some(seq_repr) = seq_repr {
+                                            *seq_repr.clone()
+                                        } else {
+                                            SugaredTypeTerm::unit()
+                                        },
+                                        args.remove(0)
+                                    ]).normalize())),
+
+                                    items: items.into_iter()
+                                        .zip(args.into_iter())
+                                        .map(|(i1, i2)| {
+                                            if i1 == i2 {
+                                                i1
+                                            } else {
+                                                SugaredTypeTerm::Ladder(vec![ i1, i2 ]).normalize()
+                                            }
+                                        })
+                                        .collect()
+                                };
+                            } else {
+                                new_rungs.push(r2);
+                                r2 = r1;
+                            }
+                        }
+
+                        (SugaredTypeTerm::Struct { struct_repr: struct_repr1, members: members1 },
+                         SugaredTypeTerm::Struct { struct_repr: struct_repr2, members: members2 }) => {
+                            todo!();
+                        }
+
+                        (SugaredTypeTerm::Enum { enum_repr: enum_repr1, variants: variants1 },
+                         SugaredTypeTerm::Enum { enum_repr: enum_repr2, variants: variants2 }) => {
+                            todo!();
+                        }
+
+                        (SugaredTypeTerm::Spec(args1), SugaredTypeTerm::Spec(args2)) => {
+                            eprintln!("popped two spec {:?} , {:?}", args1, args2);
+                            if args1.len() == args2.len() {
+                                r2 = SugaredTypeTerm::Spec(
+                                    args1.into_iter().zip(args2.into_iter())
+                                    .map(|(a1,a2)|
+                                        if a1 == SugaredTypeTerm::unit() {
+                                            a2
+                                        } else if a1 == a2 {
+                                            a2
+                                        } else if a2 == SugaredTypeTerm::unit() {
+                                            a1
+                                        } else {
+                                            SugaredTypeTerm::Ladder(vec![ a1, a2 ]).normalize()
+                                        })
+                                    .collect()
+                                );
+                            } else {
+                                new_rungs.push(r2);
+                                r2 = r1;
+                            }
+                        }
+                        (SugaredTypeTerm::Univ(args1), SugaredTypeTerm::Univ(args2)) => {
+                            todo!();
+                        }
+
+                        (SugaredTypeTerm::Func(args1), SugaredTypeTerm::Func(args2)) => {
+                            todo!();
+                        }
+                        (SugaredTypeTerm::Morph(args1), SugaredTypeTerm::Morph(args2)) => {
+                            todo!();
+                        }
+
+                        (SugaredTypeTerm::Ladder(rr1), SugaredTypeTerm::Ladder(rr2)) => {
+                            eprintln!("popped two ladders {:?} , {:?}", rr1, rr2);
+
+                            if rr1.len() > 0 {
+                                let l = splice_ladders(rr1, rr2);
+                                eprintln!("splice ladders .. = {:?}",l);
+                                r2 = SugaredTypeTerm::Ladder(l).normalize();
+                            }
+                        }
+
+                        (atomic1, SugaredTypeTerm::Ladder(mut rr2)) => {
+                            if !atomic1.is_empty() {
+                                eprintln!("add head of ladder");
+                                if rr2.first() != Some(&atomic1) {
+                                    rr2.insert(0, atomic1);
+                                } else {
+                                    eprintln!("skip equal head at ladder");
+                                }
+                            } else {
+                                eprintln!("skip empty atomic at head of ladder");
+                            }
+                            r2 = SugaredTypeTerm::Ladder(rr2).normalize();
+                        }
+
+                        (atomic1, atomic2) => {
+                            eprintln!("popped two atomics {:?} , {:?}", atomic1, atomic2);
+                            if atomic1.is_empty() {
+                                eprintln!("skip atomic1 (empty)");
+                            } else if atomic1 == atomic2 {
+                                eprintln!("atomic are equal");
+                                if !atomic2.is_empty() {
+                                    new_rungs.push(atomic2);
+                                }
+                                r2 = atomic1;
+                            } else if atomic2.is_empty() {
+                                eprintln!("lol");
+                                r2 = atomic1;
+                            } else {
+                                eprintln!("differnt, take atomic2");
+                                new_rungs.push(atomic2);
+                                r2 = atomic1;
                             }
-                        } else {
-                            new_rungs.push( bottom );
                         }
                     }
+                }
 
+                if new_rungs.len() > 0 {
+                    new_rungs.push(r2);
                     new_rungs.reverse();
-
-                    if new_rungs.len() > 1 {
-                        SugaredTypeTerm::Ladder(new_rungs)
-                    } else if new_rungs.len() == 1 {
-                        new_rungs[0].clone()
-                    } else {
-                        SugaredTypeTerm::unit()
-                    }
+                    return SugaredTypeTerm::Ladder(new_rungs);
                 } else {
-                    SugaredTypeTerm::unit()
+                    return r2;
                 }
             }
 
             SugaredTypeTerm::Spec(params) => {
                 SugaredTypeTerm::Spec(
                     params.into_iter()
-                        .map(|p| p.param_normalize())
+                        .map(|p| p.normalize())
                         .collect())
             }
 
             SugaredTypeTerm::Seq { seq_repr, items } => SugaredTypeTerm::Seq {
-                seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.param_normalize())) } else { None },
-                items: items.into_iter().map(|p| p.param_normalize()).collect()
+                seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.normalize())) } else { None },
+                items: items.into_iter().map(|p| p.normalize()).collect()
             },
-            SugaredTypeTerm::Struct { struct_repr, members } =>SugaredTypeTerm::Struct {
-                struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.param_normalize())) } else { None },
+            SugaredTypeTerm::Struct { struct_repr, members } => SugaredTypeTerm::Struct {
+                struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.normalize())) } else { None },
                 members: members.into_iter()
                     .map(|SugaredStructMember{symbol, ty}|
-                        SugaredStructMember{ symbol, ty: ty.param_normalize() })
+                        SugaredStructMember{ symbol, ty: ty.normalize() })
                     .collect()
             },
-            SugaredTypeTerm::Enum{ enum_repr, variants } => SugaredTypeTerm::Enum{
-                enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.param_normalize())) } else { None },
+            SugaredTypeTerm::Enum { enum_repr, variants } => SugaredTypeTerm::Enum{
+                enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.normalize())) } else { None },
                 variants: variants.into_iter()
                     .map(|SugaredEnumVariant{symbol, ty}|
-                        SugaredEnumVariant{ symbol, ty: ty.param_normalize() })
+                        SugaredEnumVariant{ symbol, ty: ty.normalize() })
                     .collect()
             },