define type nat; define variable k,m,n of type nat; define atom predicate P of type nat, nat; define atom predicate Q of type nat, nat; define predicate \varphi_{cutf} by all m (ex n ( (not P(m,n)) or Q(m,n))); define proof p proves all m (all n (P(m,n) impl Q(m,n))) :- ex m ( ex n ( ( not Q( m, n ) ) impl ( not P( m, n ) ) ) ); with cut \varphi_{cutf} left by proof \varphi_1 right by proof \varphi_2; ; define proof \varphi_1 proves all m (all n (P(m,n) impl Q(m,n))) :- \varphi_{cutf}; with undef \varphi_{cutf} :- all m (ex n ( (not P(m,n)) or Q(m,n))); with all right :- ex n ( (not P(k,n)) or Q(k,n)); with ex right :- (not P(k,n)) or Q(k,n); with all left all n (P(k,n) impl Q(k,n)) :- ; with all left P(k,n) impl Q(k,n) :- ; with or right :- not P(k,n), Q(k,n); with impl left left by proof \varphi_{1-1} right by proof \varphi_{1-2}; ; define proof \varphi_{1-1} proves :- not P(k,n), P(k,n) ; with not right P(k,n) :- ; ; define proof \varphi_{1-2} proves Q(k,n) :- Q(k,n); ; define proof \varphi_2 proves \varphi_{cutf} :- ex m ( ex n ( ( not Q( m, n ) ) impl ( not P( m, n ) ) ) ); with undef \varphi_{cutf} all m (ex n ( (not P(m,n)) or Q(m,n))) :- ; with all left ex n ( (not P(m,n)) or Q(m,n)) :- ; with ex left (not P(m,k)) or Q(m,k) :- ; with ex right :- ex n ( ( not Q( m, n ) ) impl ( not P( m, n ) ) ); with ex right :- ( not Q( m, k ) ) impl ( not P( m, k ) ); with impl right not Q( m, k ) :- not P( m, k ); with or left left by proof \varphi_{2-1} right by proof \varphi_{2-2}; ; define proof \varphi_{2-1} proves not P(m,k) :- not P( m, k ); with not left :- P(m,k); with not right P(m,k) :- ; ; define proof \varphi_{2-2} proves Q(m,k), not Q( m, k ) :- ; with not left :- Q(m,k); ;