script.kps 1.1 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
script split_from_quicksort_nice() {
  autopilot_prep;
  foreach{
    tryclose;
  }
  foreach{
    simp_upd;
    seqPermFromSwap;
    andRight;
  }


  cases{
    case match `==> seqDef(_,_,_) = seqDef(_, _, _)`:
        auto;
    case match `==> \exists ...`: //hier sollten bessere branchnamen hin
        instantiate  var=`iv` with=`i_0`;
        instantiate  var=`jv` with=`j_0`;
        auto;
  }
}




script split_from_quicksort() {
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
autopilot_prep;
foreach{
	tryclose;
}

cases{
	default:
		simp_upd;  //only 2nd open goal needs this
		seqPermFromSwap;
		andRight;
}


cases{
	case match '#0.*':
		auto;
	case match '#1.*':
				instantiate  var=`iv` with=`i_0`;
				instantiate  var=`jv` with=`j_0`;
				auto;
}
}



52
script split_from_quicksort_rev() {
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
  autopilot_prep;
  foreach{
    tryclose;
  }
  foreach{
    simp_upd;
    seqPermFromSwap;
    andRight;
  }


  cases{
    case match '#0.*': //hier sollten bessere branchnamen hin
        auto;
    case match '#1.*': //hier sollten bessere branchnamen hin
        instantiate  var=`iv` with=`i_0`;
        instantiate  var=`jv` with=`j_0`;
        auto;
  }
}