equal
deleted
inserted
replaced
855 Goal |
855 Goal |
856 " ! n. ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \ |
856 " ! n. ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \ |
857 \ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2)))"; |
857 \ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2)))"; |
858 by (Seq_induct_tac "x" [] 1); |
858 by (Seq_induct_tac "x" [] 1); |
859 by (strip_tac 1); |
859 by (strip_tac 1); |
860 by (exhaust_tac "n" 1); |
860 by (cases_tac "n" 1); |
861 by Auto_tac; |
861 by Auto_tac; |
862 by (exhaust_tac "n" 1); |
862 by (cases_tac "n" 1); |
863 by Auto_tac; |
863 by Auto_tac; |
864 qed"take_reduction1"; |
864 qed"take_reduction1"; |
865 |
865 |
866 |
866 |
867 Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \ |
867 Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \ |
877 Goal |
877 Goal |
878 " ! n. ((! k. k < n --> seq_take k`y1 << seq_take k`y2) \ |
878 " ! n. ((! k. k < n --> seq_take k`y1 << seq_take k`y2) \ |
879 \ --> seq_take n`(x @@ (t>>y1)) << seq_take n`(x @@ (t>>y2)))"; |
879 \ --> seq_take n`(x @@ (t>>y1)) << seq_take n`(x @@ (t>>y2)))"; |
880 by (Seq_induct_tac "x" [] 1); |
880 by (Seq_induct_tac "x" [] 1); |
881 by (strip_tac 1); |
881 by (strip_tac 1); |
882 by (exhaust_tac "n" 1); |
882 by (cases_tac "n" 1); |
883 by Auto_tac; |
883 by Auto_tac; |
884 by (exhaust_tac "n" 1); |
884 by (cases_tac "n" 1); |
885 by Auto_tac; |
885 by Auto_tac; |
886 qed"take_reduction_less1"; |
886 qed"take_reduction_less1"; |
887 |
887 |
888 |
888 |
889 Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \ |
889 Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \ |