("digraphs" |digraphs| |singleton_digraph_TCC2| "" (SKOSIMP*) (("" (EXPAND "emptyset") (("" (PROPAX) NIL)))))("digraph_ops" |digraph_ops| |num_edges_TCC1| "" (SUBTYPE-TCC))("digraph_ops" |digraph_ops| |del_edge_TCC2| "" (SUBTYPE-TCC) NIL)("digraph_ops" |digraph_ops| |union_TCC2| "" (SUBTYPE-TCC) NIL)("walks" |walks| |walk?_caret_TCC2| "" (SUBTYPE-TCC) NIL)("walks" |walks| |prewalk_across_TCC7| "" (SUBTYPE-TCC) NIL)("walks" |walks| |edges_of_TCC4| "" (SUBTYPE-TCC))("paths" |paths| |path?_gen_seq2_TCC2| "" (SUBTYPE-TCC) NIL)("paths" |paths| |path?_gen_seq2_TCC1| "" (SUBTYPE-TCC) NIL)("paths" |paths| |path_from?_caret_TCC3| "" (SUBTYPE-TCC) NIL)("paths" |paths| |path?_caret_TCC2| "" (SUBTYPE-TCC) NIL)("walk_inductions" |walk_inductions| |walk_to_path| "" (SKOLEM!) (("" (CASE "FORALL (w: prewalk): NOT walk_from?(G!1, w, s!1, t!1) OR (EXISTS (p: prewalk): path?(G!1, p) AND walk_from?(G!1, p, s!1, t!1))") (("1" (FLATTEN) (("1" (SKOSIMP*) (("1" (INST -1 "w!1") (("1" (ASSERT) NIL))))))) ("2" (HIDE 2) (("2" (INDUCT "w" 1 "digraph_induction_walk") (("2" (SKOSIMP*) (("2" (CASE "(EXISTS (i,j: below(l(w!1))): i /= j AND seq(w!1)(i) = seq(w!1)(j))") (("1" (SKOSIMP*) (("1" (CASE "i!1 < j!1") (("1" (INST -3 "w!1^(0,i!1) o w!1^(j!1-1,l(w!1)-1)") (("1" (SPLIT -3) (("1" (POSTPONE) NIL) ("2" (PROPAX) NIL) ("3" (EXPAND "^") (("3" (EXPAND "o ") (("3" (ASSERT) (("3" (TYPEPRED "j!1") (("3" (TYPEPRED "i!1") (("3" (POSTPONE) NIL))))))))))))) ("2" (POSTPONE) NIL) ("3" (ASSERT) NIL))) ("2" (POSTPONE) NIL))))) ("2" (INST 2 "w!1") (("2" (ASSERT) (("2" (EXPAND "path?") (("2" (EXPAND "walk_from?") (("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (INST 1 "i!1" "j!1") (("2" (ASSERT) (("2" (EXPAND "fseq") (("2" (PROPAX) NIL)))))))))))))))))))))))))))))))))))("seq_pidgeon" |seq_pidgeon| |seq_pigeon_hole2| "" (SKOSIMP*) (("" (LEMMA "seq_pigeon_lem") (("" (INST?) (("" (ASSERT) (("" (SKOSIMP*) (("" (INST?) (("" (ASSERT) NIL)))))))))))))("seq_pidgeon" |seq_pidgeon| |CY_lem| "" (SKOSIMP*) (("" (LEMMA "card_empty?[below(l(w!1))]") (("" (INST?) (("" (ASSERT) (("" (EXPAND "empty?") (("" (SKOSIMP*) (("" (EXPAND "member") (("" (HIDE -2) (("" (EXPAND "Y") (("" (CASE-REPLACE "card(T(w!1, x!1)) > 1") (("1" (HIDE -2) (("1" (INST 1 "choose(T(w!1,x!1))" "choose(remove(choose(T(w!1,x!1)), T(w!1,x!1)))") (("1" (POSTPONE) NIL) ("2" (POSTPONE) NIL) ("3" (POSTPONE) NIL))))) ("2" (HIDE 2) (("2" (LEMMA "T_1") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))))))))("seq_pidgeon" |seq_pidgeon| |Y_lem| "" (SKOSIMP*) (("" (LEMMA "X_lem") (("" (INST?) (("" (LEMMA "XY_lem") (("" (INST?) (("" (ASSERT) NIL)))))))))))("seq_pidgeon" |seq_pidgeon| |XY_lem| "" (SKOSIMP*) (("" (CASE "fullset[below(l(w!1))] = union(X(w!1),Y(w!1))") (("1" (CASE-REPLACE "card(fullset[below(l(w!1))]) = card(union(X(w!1), Y(w!1)))") (("1" (HIDE -2) (("1" (REWRITE "card_union[below(l(w!1))]") (("1" (CASE-REPLACE "card(intersection(X(w!1), Y(w!1))) = 0") (("1" (HIDE -1) (("1" (REWRITE "card_below_fullset") (("1" (ASSERT) NIL))))) ("2" (HIDE -1 2) (("2" (CASE-REPLACE "intersection(X(w!1), Y(w!1)) = emptyset[below(l(w!1))]") (("1" (HIDE -1) (("1" (REWRITE "card_emptyset[below(l(w!1))]") NIL))) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL))))))))) ("3" (REWRITE "finite_below") NIL))))))) ("2" (ASSERT) NIL) ("3" (REWRITE "finite_below") NIL) ("4" (REWRITE "finite_below") NIL))) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL)))))))))("seq_pidgeon" |seq_pidgeon| |X_lem| "" (SKOSIMP*) (("" (POSTPONE) NIL)))("seq_pidgeon" |seq_pidgeon| W_TCC1 "" (SUBTYPE-TCC))("seq_pidgeon" |seq_pidgeon| Y_TCC1 "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL)))("seq_pidgeon" |seq_pidgeon| X_TCC1 "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL)))("seq_pidgeon" |seq_pidgeon| T_1 "" (SKOSIMP*) (("" (EXPAND "T") (("" (EXPAND "fseq") (("" (CASE "{j: below(l(w!1)) | (seq(w!1)(j) = seq(w!1)(i!1))}(i!1)") (("1" (LEMMA "card_empty?[below(l(w!1))]") (("1" (INST -1 "{j: below(l(w!1)) | (seq(w!1)(j) = seq(w!1)(i!1))}") (("1" (CASE "card({j: below(l(w!1)) | (seq(w!1)(j) = seq(w!1)(i!1))}) = 0") (("1" (ASSERT) (("1" (HIDE -1 1) (("1" (EXPAND "empty?") (("1" (INST?) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))))))) ("2" (HIDE -1 -2) (("2" (ASSERT) NIL))) ("3" (HIDE -1 -2 2) (("3" (REWRITE "finite_below") NIL))))) ("2" (REWRITE "finite_below") NIL))))) ("2" (HIDE 2) (("2" (GRIND) NIL)))))))))))("seq_pidgeon" |seq_pidgeon| T_TCC1 "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL)))("di_subgraphs_from_walk" |di_subgraphs_from_walk| |edge?_G_from_TCC3| "" (SKOSIMP*) (("" (TYPEPRED "i!1") (("" (ASSERT) NIL)))))("reduce_walks" |reduce_walks| |reduce_lem_TCC4| "" (SUBTYPE-TCC) NIL)("reduce_walks" |reduce_walks| |reduce_TCC7| "" (SUBTYPE-TCC))("digraph_inductions" |digraph_inductions| |digraph_induction_both| "" (SKOSIMP*) (("" (INST?) (("" (PROP) (("1" (LEMMA "digraph_induction_edge") (("1" (INST -1 "P!1") (("1" (SPLIT -1) (("1" (INST?) NIL) ("2" (SKOSIMP*) (("2" (POSTPONE) NIL))))))))) ("2" (POSTPONE) NIL)))))))