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
80
81
82
|
Minlog loaded successfully
> > loading nat.scm ...
> > > ; ok, variable f: nat=>nat added
; ok, variable g: nat=>nat added
> ; ?_1: all f,g,n(
; all n(n<f 0 -> bot) ->
; all n n<f(g n) -> excl m((n<f m -> bot) ! n<f(m+1)))
> ; ok, we now have the new goal
; ?_2: bot from
; f g n 1:all n(n<f 0 -> bot)
; 2:all n n<f(g n)
; 3:all m((n<f m -> bot) -> n<f(m+1) -> bot)
> ; ok, ?_2 can be obtained from
; ?_4: all m(n<f m -> bot) from
; f g n 1:all n(n<f 0 -> bot)
; 2:all n n<f(g n)
; 3:all m((n<f m -> bot) -> n<f(m+1) -> bot)
; ?_3: excl m n<f m from
; f g n 1:all n(n<f 0 -> bot)
; 2:all n n<f(g n)
; 3:all m((n<f m -> bot) -> n<f(m+1) -> bot)
> ; ok, ?_3 is proved by minimal quantifier logic. The active goal now is
; ?_4: all m(n<f m -> bot) from
; f g n 1:all n(n<f 0 -> bot)
; 2:all n n<f(g n)
; 3:all m((n<f m -> bot) -> n<f(m+1) -> bot)
> ; ok, ?_4 can be obtained from
; ?_6: all n561((n<f n561 -> bot) -> n<f(Succ n561) -> bot) from
; f g n 1:all n(n<f 0 -> bot)
; 2:all n n<f(g n)
; 3:all m((n<f m -> bot) -> n<f(m+1) -> bot)
; m559
; ?_5: n<f 0 -> bot from
; f g n 1:all n(n<f 0 -> bot)
; 2:all n n<f(g n)
; 3:all m((n<f m -> bot) -> n<f(m+1) -> bot)
; m559
> ; ok, ?_5 is proved by minimal quantifier logic. The active goal now is
; ?_6: all n561((n<f n561 -> bot) -> n<f(Succ n561) -> bot) from
; f g n 1:all n(n<f 0 -> bot)
; 2:all n n<f(g n)
; 3:all m((n<f m -> bot) -> n<f(m+1) -> bot)
; m559
> ; ok, ?_6 is proved by minimal quantifier logic. Proof finished.
> ; ok, IntSqRt has been added as a new theorem.
; ok, program constant cIntSqRt: (nat=>nat)=>(nat=>nat)=>nat=>(nat=>alpha3)=>(nat=>alpha3=>alpha3)=>alpha3
; of t-degree 1 and arity 0 added
> (lambda (f)
(lambda (g)
(lambda (n)
(lambda (u480)
(lambda (u481)
(lambda (u482)
((lambda (u485) ((u485 (g n)) (u481 n)))
(lambda (m559)
(((((|Ind| n) f) m559) (lambda (u488) ((u480 n) u488)))
(lambda (n561)
(lambda (u489)
(lambda (u490)
(((u482 n561) (lambda (u491) (u489 u491)))
u490)))))))))))))
> (lambda (f)
(lambda (g)
(lambda (n)
(lambda (u492)
(lambda (u493)
(lambda (u494)
((((((|Ind| n) f) (g n)) (u492 n)) u494) (u493 n))))))))
> > > > [f0,f1,n2](Rec nat=>nat)(f1 n2)0([n3,n4][if (n2<f0 n3) n4 n3])
> > 1
> 2
> 2
> 3
> 3
> 4
> ; ok, Lemma1 has been added as a new global assumption.
> ; ok, Lemma2 has been added as a new global assumption.
>
|
