# Module is html

ws2s;

guide a->(dummy,b), b->(b,b), dummy->(dummy,dummy);	
universe UNI_H:1, u_dummy:0;

# Skeleton

var2 [UNI_H] $ where all1 p: (p in $) => (p^ in $);
defaultwhere1(p) = p in $;


# Type environment

var2 T0,T1;
var2 G0,G1,G2;

# Type predicates

macro NULL(var1 p) = 
   (p notin T0) & (p notin T1) &
   (p notin G0) & (p notin G1) & (p notin G2);

macro TYPE_Bool(var1 p) =
   (p notin T0) & (p notin T1);

macro TYPE0_Bool(var0 t0,t1) =
   ~t0 & ~t1;

macro TYPE_HTML(var1 p) =
   (p in T0) & (p notin T1);

macro TYPE0_HTML(var0 t0,t1) =
   t0 & ~t1;

macro TYPE_LIST(var1 p) =
   (p notin T0) & (p in T1);

macro TYPE0_LIST(var0 t0,t1) =
   ~t0 & t1;

macro TYPE_URL(var1 p) =
   (p in T0) & (p in T1);

macro TYPE0_URL(var0 t0,t1) =
   t0 & t1;

macro GROUP_HTML_word(var1 p,var2 G0,G1,G2) =
   (p notin G0) & (p notin G1) & (p notin G2);

macro GROUP0_HTML_word(var0 g0,g1,g2) =
   ~g0 & ~g1 & ~g2;

macro GROUP_HTML_anchor(var1 p,var2 G0,G1,G2) =
   (p in G0) & (p notin G1) & (p notin G2);

macro GROUP0_HTML_anchor(var0 g0,g1,g2) =
   g0 & ~g1 & ~g2;

macro GROUP_HTML_bold(var1 p,var2 G0,G1,G2) =
   (p notin G0) & (p in G1) & (p notin G2);

macro GROUP0_HTML_bold(var0 g0,g1,g2) =
   ~g0 & g1 & ~g2;

macro GROUP_HTML_italic(var1 p,var2 G0,G1,G2) =
   (p in G0) & (p in G1) & (p notin G2);

macro GROUP0_HTML_italic(var0 g0,g1,g2) =
   g0 & g1 & ~g2;

macro GROUP_HTML_paragraph(var1 p,var2 G0,G1,G2) =
   (p notin G0) & (p notin G1) & (p in G2);

macro GROUP0_HTML_paragraph(var0 g0,g1,g2) =
   ~g0 & ~g1 & g2;

macro GROUP_HTML_rule(var1 p,var2 G0,G1,G2) =
   (p in G0) & (p notin G1) & (p in G2);

macro GROUP0_HTML_rule(var0 g0,g1,g2) =
   g0 & ~g1 & g2;

macro GROUP_HTML_list(var1 p,var2 G0,G1,G2) =
   (p notin G0) & (p in G1) & (p in G2);

macro GROUP0_HTML_list(var0 g0,g1,g2) =
   ~g0 & g1 & g2;

macro GROUP_HTML(var1 p,var2 G0,G1,G2) =
   GROUP_HTML_word(p,G0,G1,G2) | GROUP_HTML_anchor(p,G0,G1,G2) | GROUP_HTML_bold(p,G0,G1,G2) | GROUP_HTML_italic(p,G0,G1,G2) | GROUP_HTML_paragraph(p,G0,G1,G2) | GROUP_HTML_rule(p,G0,G1,G2) | GROUP_HTML_list(p,G0,G1,G2);

macro GROUP0_HTML(var0 g0,g1,g2) =
   GROUP0_HTML_word(g0,g1,g2) | GROUP0_HTML_anchor(g0,g1,g2) | GROUP0_HTML_bold(g0,g1,g2) | GROUP0_HTML_italic(g0,g1,g2) | GROUP0_HTML_paragraph(g0,g1,g2) | GROUP0_HTML_rule(g0,g1,g2) | GROUP0_HTML_list(g0,g1,g2);

macro GROUP_LIST_empty(var1 p,var2 G0) =
   (p notin G0);

macro GROUP0_LIST_empty(var0 g0) =
   ~g0;

macro GROUP_LIST_entity(var1 p,var2 G0) =
   (p in G0);

macro GROUP0_LIST_entity(var0 g0) =
   g0;

macro GROUP_LIST(var1 p,var2 G0) =
   GROUP_LIST_empty(p,G0) | GROUP_LIST_entity(p,G0);

macro GROUP0_LIST(var0 g0) =
   GROUP0_LIST_empty(g0) | GROUP0_LIST_entity(g0);

macro SCALAR_Bool_false_true(var1 p, var2 S0) =
   true;

macro SCALAR0_Bool_false_true(var0 s0) =
   true;

macro SCALAR_Bool(var1 p, var2 S0) =
   SCALAR_Bool_false_true(p,S0);

macro SCALAR0_Bool(var0 s0) =
   SCALAR0_Bool_false_true(s0);

macro SUCC_HTML_word(var1 p) =
   (p.0 notin $) & (p.1 notin $);

macro SUCC_HTML_anchor(var1 p) =
   (p.11 notin $) &   
   (p.1 in $) & NULL(p.1) & (p.0 in $) & TYPE_URL(p.0) & (p.10 in $) & TYPE_HTML(p.10);

macro SUCC_HTML_bold(var1 p) =
   (p.1 notin $) &   (p.0 in $) & TYPE_HTML(p.0);

macro SUCC_HTML_italic(var1 p) =
   (p.1 notin $) &   (p.0 in $) & TYPE_HTML(p.0);

macro SUCC_HTML_paragraph(var1 p) =
   (p.0 notin $) & (p.1 notin $);

macro SUCC_HTML_rule(var1 p) =
   (p.0 notin $) & (p.1 notin $);

macro SUCC_HTML_list(var1 p) =
   (p.1 notin $) &   (p.0 in $) & TYPE_LIST(p.0);

macro SUCC_LIST_empty(var1 p) =
   (p.0 notin $) & (p.1 notin $);

macro SUCC_LIST_entity(var1 p) =
   (p.11 notin $) &   
   (p.1 in $) & NULL(p.1) & (p.0 in $) & TYPE_HTML(p.0) & (p.10 in $) & TYPE_LIST(p.10);

macro SUCC_URL_url(var1 p) =
   (p.0 notin $) & (p.1 notin $);

macro EQ0_HTML(var0 g0_l,g1_l,g2_l,g0_r,g1_r,g2_r) = (
   (g0_l <=> g0_r) & (g1_l <=> g1_r) & (g2_l <=> g2_r)
);

macro WF_HTML(var1 p,var2 G0,G1,G2) = TYPE_HTML(p) & (
   (GROUP_HTML_word(p,G0,G1,G2) & SUCC_HTML_word(p))
  |
   (GROUP_HTML_anchor(p,G0,G1,G2) & SUCC_HTML_anchor(p))
  |
   (GROUP_HTML_bold(p,G0,G1,G2) & SUCC_HTML_bold(p))
  |
   (GROUP_HTML_italic(p,G0,G1,G2) & SUCC_HTML_italic(p))
  |
   (GROUP_HTML_paragraph(p,G0,G1,G2) & SUCC_HTML_paragraph(p))
  |
   (GROUP_HTML_rule(p,G0,G1,G2) & SUCC_HTML_rule(p))
  |
   (GROUP_HTML_list(p,G0,G1,G2) & SUCC_HTML_list(p))
);

macro WF0_HTML(var0 t0,t1,g0,g1,g2) =
   TYPE0_HTML(t0,t1) & (
   (GROUP0_HTML_word(g0,g1,g2))
  |
   (GROUP0_HTML_anchor(g0,g1,g2))
  |
   (GROUP0_HTML_bold(g0,g1,g2))
  |
   (GROUP0_HTML_italic(g0,g1,g2))
  |
   (GROUP0_HTML_paragraph(g0,g1,g2))
  |
   (GROUP0_HTML_rule(g0,g1,g2))
  |
   (GROUP0_HTML_list(g0,g1,g2))
);

macro EQ0_LIST(var0 g0_l,g0_r) = (
   (g0_l <=> g0_r)
);

macro WF_LIST(var1 p,var2 G0) = TYPE_LIST(p) & (
   (GROUP_LIST_empty(p,G0) & SUCC_LIST_empty(p))
  |
   (GROUP_LIST_entity(p,G0) & SUCC_LIST_entity(p))
);

macro WF0_LIST(var0 t0,t1,g0) =
   TYPE0_LIST(t0,t1) & (
   (GROUP0_LIST_empty(g0))
  |
   (GROUP0_LIST_entity(g0))
);

macro WF_URL(var1 p) = TYPE_URL(p) & (
   (SUCC_URL_url(p))
);

macro WF0_URL(var0 t0,t1) =
   TYPE0_URL(t0,t1);

macro TREE_HTML(var1 p,var2 G0,G1,G2) =
   TYPE_HTML(p) & (all1 [p] q: (p<=q) => (NULL(q) | WF_HTML(q,G0,G1,G2) | WF_LIST(q,G0) | WF_URL(q)));

macro SKEL_HTML(var1 p,var2 G0_f,G1_f,G2_f) =
   all1 [p] q: (p<=q) => (
   (TYPE_HTML(q) => (
      (GROUP_HTML_word(q,G0,G1,G2) <=> GROUP_HTML_word(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_anchor(q,G0,G1,G2) <=> GROUP_HTML_anchor(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_bold(q,G0,G1,G2) <=> GROUP_HTML_bold(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_italic(q,G0,G1,G2) <=> GROUP_HTML_italic(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_paragraph(q,G0,G1,G2) <=> GROUP_HTML_paragraph(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_rule(q,G0,G1,G2) <=> GROUP_HTML_rule(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_list(q,G0,G1,G2) <=> GROUP_HTML_list(q,G0_f,G1_f,G2_f))
   )) &
   (TYPE_LIST(q) => (
      (GROUP_LIST_empty(q,G0) <=> GROUP_LIST_empty(q,G0_f)) &
      (GROUP_LIST_entity(q,G0) <=> GROUP_LIST_entity(q,G0_f))
   )) &
   (TYPE_URL(q) => (
      true
   ))
);

macro TREE_LIST(var1 p,var2 G0,G1,G2) =
   TYPE_LIST(p) & (all1 [p] q: (p<=q) => (NULL(q) | WF_LIST(q,G0) | WF_HTML(q,G0,G1,G2) | WF_URL(q)));

macro SKEL_LIST(var1 p,var2 G0_f,G1_f,G2_f) =
   all1 [p] q: (p<=q) => (
   (TYPE_LIST(q) => (
      (GROUP_LIST_empty(q,G0) <=> GROUP_LIST_empty(q,G0_f)) &
      (GROUP_LIST_entity(q,G0) <=> GROUP_LIST_entity(q,G0_f))
   )) &
   (TYPE_HTML(q) => (
      (GROUP_HTML_word(q,G0,G1,G2) <=> GROUP_HTML_word(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_anchor(q,G0,G1,G2) <=> GROUP_HTML_anchor(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_bold(q,G0,G1,G2) <=> GROUP_HTML_bold(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_italic(q,G0,G1,G2) <=> GROUP_HTML_italic(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_paragraph(q,G0,G1,G2) <=> GROUP_HTML_paragraph(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_rule(q,G0,G1,G2) <=> GROUP_HTML_rule(q,G0_f,G1_f,G2_f)) &
      (GROUP_HTML_list(q,G0,G1,G2) <=> GROUP_HTML_list(q,G0_f,G1_f,G2_f))
   )) &
   (TYPE_URL(q) => (
      true
   ))
);

macro TREE_URL(var1 p) =
   TYPE_URL(p) & (all1 [p] q: (p<=q) => (NULL(q) | WF_URL(q)));

macro SKEL_URL(var1 p) =
   all1 [p] q: (p<=q) => (
   (TYPE_URL(q) => (
      true
   ))
);

macro DOT_u(var1 p,var1 q) =
   (TYPE_HTML(p) & GROUP_HTML_word(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_anchor(p,G0,G1,G2) & (q=p.0))
 | (TYPE_HTML(p) & GROUP_HTML_bold(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_italic(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_paragraph(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_rule(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_list(p,G0,G1,G2) & (q=p));

macro DOT_a(var1 p,var1 q) =
   (TYPE_HTML(p) & GROUP_HTML_word(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_anchor(p,G0,G1,G2) & (q=p.10))
 | (TYPE_HTML(p) & GROUP_HTML_bold(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_italic(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_paragraph(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_rule(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_list(p,G0,G1,G2) & (q=p));

macro DOT_b(var1 p,var1 q) =
   (TYPE_HTML(p) & GROUP_HTML_word(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_anchor(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_bold(p,G0,G1,G2) & (q=p.0))
 | (TYPE_HTML(p) & GROUP_HTML_italic(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_paragraph(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_rule(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_list(p,G0,G1,G2) & (q=p));

macro DOT_i(var1 p,var1 q) =
   (TYPE_HTML(p) & GROUP_HTML_word(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_anchor(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_bold(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_italic(p,G0,G1,G2) & (q=p.0))
 | (TYPE_HTML(p) & GROUP_HTML_paragraph(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_rule(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_list(p,G0,G1,G2) & (q=p));

macro DOT_l(var1 p,var1 q) =
   (TYPE_HTML(p) & GROUP_HTML_word(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_anchor(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_bold(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_italic(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_paragraph(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_rule(p,G0,G1,G2) & (q=p))
 | (TYPE_HTML(p) & GROUP_HTML_list(p,G0,G1,G2) & (q=p.0));

macro DOT_h(var1 p,var1 q) =
   (TYPE_LIST(p) & GROUP_LIST_empty(p,G0) & (q=p))
 | (TYPE_LIST(p) & GROUP_LIST_entity(p,G0) & (q=p.0));

macro DOT_next(var1 p,var1 q) =
   (TYPE_LIST(p) & GROUP_LIST_empty(p,G0) & (q=p))
 | (TYPE_LIST(p) & GROUP_LIST_entity(p,G0) & (q=p.10));

macro DOT(var1 p,var1 q) =
   DOT_u(p,q) | DOT_a(p,q) | DOT_b(p,q) | DOT_i(p,q) | DOT_l(p,q) | DOT_h(p,q) | DOT_next(p,q);

macro UP(var1 p,var1 q) =
   (root(p,[p]) & p=q) | DOT(q,p);

# Free variables

assert ex1 [UNI_H] p: root(p,[p]) & TREE_HTML(p,G0,G1,G2);

# Functions

pred FUNC_NoNestedAnchors(universe UNI_h,var2 G0_h,G1_h,G2_h) =
(all1 [UNI_h] POS_p: (TYPE_HTML(POS_p)) => ((ex0 t0_1,t1_1,g0_1,g1_1,g2_1: ex0 t0_4,t1_4,g0_4,g1_4,g2_4: 
(ex1  [UNI_h] POS3: (POS3=POS_p) & (t1_1<=>(POS3 in T1)) & (t0_1<=>(POS3 in T0)) & 
(g2_1<=>(POS3 in G2)) & (g1_1<=>(POS3 in G1)) & (g0_1<=>(POS3 in G0))) & ((TYPE0_HTML(t0_4,t1_4) 
& g0_4 & ~g1_4 & ~g2_4)) & EQ0_HTML(g0_1,g1_1,g2_1,g0_4,g1_4,g2_4)) => (~(ex1 [UNI_h] 
POS_q: (TYPE_HTML(POS_q)) & ((ex1 [UNI_h] POS6: ex1 [UNI_h] POS8: (POS6=POS_p) & 
(POS8=POS_q) & (POS6 < POS8)) & (ex0 t0_9,t1_9,g0_9,g1_9,g2_9: ex0 t0_12,t1_12,g0_12,g1_12,g2_12: 
(ex1 [UNI_h] POS11: (POS11=POS_q) & (t1_9<=>(POS11 in T1)) & (t0_9<=>(POS11 in T0)) 
& (g2_9<=>(POS11 in G2)) & (g1_9<=>(POS11 in G1)) & (g0_9<=>(POS11 in G0))) & ((TYPE0_HTML(t0_12,t1_12) 
& g0_12 & ~g1_12 & ~g2_12)) & EQ0_HTML(g0_9,g1_9,g2_9,g0_12,g1_12,g2_12)))))));

# Main formula

export("html.gta",(ex2 G0_13,G1_13,G2_13: ((G0_13=G0) & (G1_13=G1) & (G2_13=G2)) & FUNC_NoNestedAnchors(UNI_H,G0_13,G1_13,G2_13)));