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
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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
Minlog loaded successfully
> > loading nat.scm ...
> > > ; ok, variable f: nat=>nat added
> ; ?_1: all f(all m(m<0 -> bot) -> excl k(f(k+1)<f k -> bot))
> ; ok, we now have the new goal
; ?_2: excl k(f(k+1)<f k -> bot) from
; f 1:all m(m<0 -> bot)
> ; ok, ?_2 can be obtained from
; ?_6: excl k(f(k+1)<f k -> bot) from
; f 1:all m(m<0 -> bot)
; k k-Min:all n1283(f n1283<f k -> T -> bot)
; k-Hyp:T
; ?_5: excl k T from
; f 1:all m(m<0 -> bot)
> ; ok, ?_5 can be obtained from
; ?_7: T from
; f 1:all m(m<0 -> bot)
> ; ok, ?_7 is proved. The active goal now is
; ?_6: excl k(f(k+1)<f k -> bot) from
; f 1:all m(m<0 -> bot)
; k k-Min:all n1283(f n1283<f k -> T -> bot)
; k-Hyp:T
> ; ok, we now have the new goal
; ?_8: bot from
; f 1:all m(m<0 -> bot)
; k k-Min:all n1283(f n1283<f k -> T -> bot)
; k-Hyp:T
; H1:all k((f(k+1)<f k -> bot) -> bot)
> ; ok, ?_8 can be obtained from
; ?_9: f(k+1)<f k -> bot from
; f 1:all m(m<0 -> bot)
; k k-Min:all n1283(f n1283<f k -> T -> bot)
; k-Hyp:T
; H1:all k((f(k+1)<f k -> bot) -> bot)
> ; ok, we now have the new goal
; ?_10: bot from
; f 1:all m(m<0 -> bot)
; k k-Min:all n1283(f n1283<f k -> T -> bot)
; k-Hyp:T
; H1:all k((f(k+1)<f k -> bot) -> bot)
; H2:f(k+1)<f k
> ; ok, ?_10 can be obtained from
; ?_12: T from
; f 1:all m(m<0 -> bot)
; k k-Min:all n1283(f n1283<f k -> T -> bot)
; k-Hyp:T
; H1:all k((f(k+1)<f k -> bot) -> bot)
; H2:f(k+1)<f k
; ?_11: f(k+1)<f k from
; f 1:all m(m<0 -> bot)
; k k-Min:all n1283(f n1283<f k -> T -> bot)
; k-Hyp:T
; H1:all k((f(k+1)<f k -> bot) -> bot)
; H2:f(k+1)<f k
> ; ok, ?_11 is proved. The active goal now is
; ?_12: T from
; f 1:all m(m<0 -> bot)
; k k-Min:all n1283(f n1283<f k -> T -> bot)
; k-Hyp:T
; H1:all k((f(k+1)<f k -> bot) -> bot)
; H2:f(k+1)<f k
> ; ok, ?_12 is proved. Proof finished.
> ; ok, WfTest has been added as a new theorem.
; ok, program constant cWfTest: (nat=>nat)=>(nat=>alpha3)=>(nat=>alpha3=>alpha3)=>alpha3
; of t-degree 0 and arity 0 added
> > > > > [f0]
[if (f0 1<f0 0)
[if (f0 2<f0 1)
((GRecGuard nat nat)f0 2([n1,f2][if (f0(Succ n1)<f0 n1) (f2(Succ n1)) n1])
(f0 2<f0 1))
1]
0]
> > 1
> > 2
>
|
