value "Dang (fst r1)"

"⌈indeg ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 1 ⌈∧⌉ ⌈outdeg ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 0 ⌈∧⌉ form.T"
  :: "form"

lemma "(Dang (fst r1)) = (⌈indeg  ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 1 ⌈∧⌉ ⌈outdeg  ↝⇩V 3⌉ ⌈=⌉ ▹⇩I 0 ⌈∧⌉ form.T)"
  apply (simp  add: r1_def)

goal (1 subgoal):
 1. (eval g undefined
      (foldr
        (λk a. ⌈indeg ↝⇩V k⌉ ⌈=⌉
                ▹⇩I foldr
                     (λka b.
                         if edge_trg
                             (the (if ka = Suc 0 then Some ⦇edge_src = Suc 0, edge_trg = 2, edge_mark = RuleMarkEdge_None, edge_label = [Var 3]⦈
                                   else [2 ↦ ⦇edge_src = Suc 0, edge_trg = 3, edge_mark = RuleMarkEdge_None, edge_label = [Var 4]⦈] ka)) =
                            k
                         then Suc b else b)
                     (Mapping.ordered_keys
                       (AList_Mapping.Mapping
                         [(Suc 0, ⦇edge_src = Suc 0, edge_trg = 2, edge_mark = RuleMarkEdge_None, edge_label = [Var 3]⦈),
                          (2, ⦇edge_src = Suc 0, edge_trg = 3, edge_mark = RuleMarkEdge_None, edge_label = [Var 4]⦈)]))
                     0 ⌈∧⌉
                ⌈outdeg ↝⇩V k⌉ ⌈=⌉
....