File: test.save

package info (click to toggle)
minlog 4.0.99.20100221-6
links: PTS
area: main
in suites: buster, stretch
size: 7,060 kB
ctags: 4,293
sloc: lisp: 112,614; makefile: 257; sh: 11
file content (4545 lines) | stat: -rw-r--r-- 178,809 bytes
parent folder | download | duplicates (4)


Minlog loaded successfully
> > ; ok, algebra nat added
> ; ok, algebra ordl added
> ; ok, algebra list added
> ; ok, algebra ytensor added
> ; ok, algebra yplus added
> ; ok, algebra tree added
; ok, algebra tlist added
> ; ok, algebra labtree added
; ok, algebra labtlist added
> ; ok, algebra hterm added
; ok, algebra htermlist added
; ok, algebra term added
> ; ok, algebra inftree added
; ok, algebra inftlist added
> #t
> #f
> #t
> #f
> #t
> #f
> #t
> #f
> #t
> #t
> #t
> #t
> #f
> #f
> #t
> #f
> #t
> #f
> #t
> #t
> #t
> #t
> #f
> ; ok, algebra nat removed
; ok, constructor Lim removed
; ok, constructor Infbranch removed
; ok, constructor Newleaf removed
; ok, constructor Dn removed
; ok, constructor OrdSup removed
; ok, constructor Succ removed
; ok, constructor Zero removed
; ok, algebra ordl removed
; ok, constructor OrdZero removed
; ok, algebra list removed
; ok, constructor Cons removed
; ok, constructor Nil removed
; ok, algebra ytensor removed
; ok, constructor TensorPair removed
; ok, algebra yplus removed
; ok, constructor Inright removed
; ok, constructor Inleft removed
; ok, algebra tree removed
; ok, algebra tlist removed
; ok, constructor Tcons removed
; ok, constructor Empty removed
; ok, constructor Branch removed
; ok, constructor Leaf removed
; ok, algebra labtree removed
; ok, algebra labtlist removed
; ok, constructor LabTcons removed
; ok, constructor LabEmpty removed
; ok, constructor LabBranch removed
; ok, constructor LabLeaf removed
; ok, algebra hterm removed
; ok, algebra htermlist removed
; ok, algebra term removed
; ok, constructor Seq removed
; ok, constructor Hcons removed
; ok, constructor Hempty removed
; ok, constructor One removed
; ok, algebra inftree removed
; ok, algebra inftlist removed
; ok, constructor Inftcons removed
; ok, constructor Emptyinftlist removed
> ; ok, algebra tree added
; ok, algebra tlist added
> ; ok, algebra nat added
> alpha1=>boole
tlist alpha1=>nat=>boole
nat
tree alpha1=>tlist alpha1=>boole=>nat=>nat
> nat
tlist alpha1=>nat=>nat
> alpha1=>boole
boole
> tree alpha1=>
(alpha1=>alpha6)=>
(tlist alpha1=>alpha5=>alpha6)=>
alpha5=>(tree alpha1=>tlist alpha1=>alpha6=>alpha5=>alpha5)=>alpha6
tlist alpha1=>
(alpha1=>alpha6)=>
(tlist alpha1=>alpha5=>alpha6)=>
alpha5=>(tree alpha1=>tlist alpha1=>alpha6=>alpha5=>alpha5)=>alpha5
; Type substitution:
; alpha1	->	unit
; alpha6	->	boole
; alpha5	->	nat
> tlist alpha1=>alpha7=>(tlist alpha1=>alpha7=>alpha7)=>alpha7
; Type substitution:
; alpha1	->	unit
; alpha7	->	nat
> tree alpha1=>(alpha1=>alpha8)=>alpha8=>alpha8
; Type substitution:
; alpha1	->	unit
; alpha8	->	boole
> ; ok, algebra tree removed
; ok, algebra tlist removed
; ok, constructor Tcons removed
; ok, constructor Empty removed
; ok, constructor Branch removed
; ok, constructor Leaf removed
> ; ok, algebra nat removed
; ok, constructor Succ removed
; ok, constructor Zero removed
> > loading nat.scm ...
> > ; ok, inductively defined predicate constant Even added
> ("cInitEven" "cGenEven")
> ; ok, inductively defined predicate constant Ev added
; ok, inductively defined predicate constant Od added
> ("cInitEv" "cGenEv")
> ("cGenOd")
> ; ok, variable x: alpha added
; ok, variable y: alpha added
; ok, variable z: alpha added
> ; ok, predicate variable P: (arity) added
> ; ok, predicate variable Q: (arity alpha) added
> ; ok, predicate variable R: (arity alpha alpha) added
> ; ok, inductively defined predicate constant EqD added
> > x^1 eqd x^2
> > n1 eqd n2
> ; ok, inductively defined predicate constant OrD added
> ("cInlOrD" "cInrOrD")
> > P1 ord P2
> > T ord F
> ; ok, inductively defined predicate constant ExD added
> > "exd n n=m"
> ; ok, inductively defined predicate constant PiOne added
> ; ok, inductively defined predicate constant TrCl added
> ; ok, inductively defined predicate constant Acc added
> ("cEfqAcc" "cGenAccSup")
> > (Acc (cterm (x^1,x^2) R x^1 x^2))x^3
> > (Acc (cterm (n1,n2) n1<n2))n3
> ; ok, inductively defined predicate constant ExDT added
> ; ok, inductively defined predicate constant Cup added
> ; ok, inductively defined predicate constant Cap added
> ; ok, variable x is removed
; warning: x was default variable of type alpha
; ok, variable y is removed
; ok, variable z is removed
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity)
; ok, predicate variable Q is removed
; warning: Q was default pvariable of arity (arity alpha)
; ok, predicate variable R is removed
; warning: R was default pvariable of arity (arity alpha alpha)
> ; ok, inductively defined predicate constant Even removed
; ok, inductively defined predicate constant Ev removed
; ok, inductively defined predicate constant Od removed
; ok, inductively defined predicate constant EqD removed
; ok, inductively defined predicate constant OrD removed
; ok, inductively defined predicate constant ExD removed
; ok, inductively defined predicate constant PiOne removed
; ok, inductively defined predicate constant TrCl removed
; ok, inductively defined predicate constant Acc removed
; ok, inductively defined predicate constant ExDT removed
; ok, inductively defined predicate constant Cup removed
; ok, inductively defined predicate constant Cap removed
> ; ok, variable x: alpha added
> ; ok, predicate variable Q: (arity alpha) added
> ; Predicate substitution:
; Q	->	(cterm (x^) Total x^)
> ; Predicate substitution:
; (Pvar unit)	->	(cterm (unit^1384) Total x^)
> ; Type substitution:
; alpha	->	unit
; Substitution:
; x^	->	unit^
> ; ok, variable x is removed
; warning: x was default variable of type alpha
> ; ok, predicate variable Q is removed
; warning: Q was default pvariable of arity (arity alpha)
> ; Predicate substitution:
; (Pvar boole)	->	(cterm (boole12) boole12=boole12)
> ; Predicate substitution:
; (Pvar boole)	->	(cterm (boole^12) Equal boole^12 boole^12)
> ; ok, algebra tree added
; ok, algebra tlist added
> ; ok, variable u: tree alpha1 added
; ok, variable v: tree alpha1 added
> ; ok, variable us: tlist alpha1 added
; ok, variable vs: tlist alpha1 added
> ; ok, variable a: tree unit added
; ok, variable b: tree unit added
> ; ok, variable as: tlist unit added
; ok, variable bs: tlist unit added
> (Rec tlist unit=>nat tree unit=>tree unit)as([unit1393](Leaf unit)unit1393)
([as1391,n1392](Branch unit)as1391)
0
([a1389,bs,a1390,n]Succ n)
> (Rec tlist unit=>nat)as 0([as1]Succ)
> (Rec tlist unit=>nat)as 0([as1,n]Succ n)
> ; ok, variable u is removed
; warning: u was default variable of type tree alpha1
; ok, variable v is removed
> ; ok, variable us is removed
; warning: us was default variable of type tlist alpha1
; ok, variable vs is removed
> ; ok, variable a is removed
; warning: a was default variable of type tree unit
; ok, variable b is removed
> ; ok, variable as is removed
; warning: as was default variable of type tlist unit
; ok, variable bs is removed
> ; ok, algebra tree removed
; ok, algebra tlist removed
; ok, constructor Tcons removed
; ok, constructor Empty removed
; ok, constructor Branch removed
; ok, constructor Leaf removed
> ; ok, variable x: alpha added
; ok, variable y: alpha added
> ; ok, predicate variable Q: (arity alpha) added
> ; ok, inductively defined predicate constant ExD added
> > > ("x2" "x3")
> ("alpha")
> ("Q")
> ; warning: x already is a variable of type alpha
; warning: y already is a variable of type alpha
> ; warning: Q already is a predicate variable of arity (arity alpha)
> exd unit1401(Equal unit1401 unit1403 -> (Pvar unit)_316 unit1402)
> Total boole^1404
> Q y
> Total x
> Equal x^ x^
> Equal x^ x^
> exd boole^1405 Equal boole^1405 boole^1405
> exd x^ Equal x^ x^
> exd x^ Equal x^ x^
> ; ok, inductively defined predicate constant ExDT added
> exdt x Equal x x
> ; ok, variable x is removed
; warning: x was default variable of type alpha
; ok, variable y is removed
> ; ok, predicate variable Q is removed
; warning: Q was default pvariable of arity (arity alpha)
> ; ok, inductively defined predicate constant ExD removed
; ok, inductively defined predicate constant ExDT removed
> > ()
> #t
> nat=>
nat=>((nat=>atomic=>atomic)=>atomic)=>(nat=>nat=>atomic=>alpha3)=>alpha3
> 2
> (((var (alg "unit") 2 1 "") (var (alg "unit") 3 1 "")))
> "n0"
> all n1408(
 0=0 -> all n1409(n1409=n1409 -> Succ n1409=Succ n1409) -> n1408=n1408)
> all n(0=0 -> all n0(n0=n0 -> Succ n0=Succ n0) -> n=n)
> all (nat=>nat)_1412,n1413(
 all n1413(
  all n1414((nat=>nat)_1412 n1414<(nat=>nat)_1412 n1413 -> n1414=n1414) -> 
  n1413=n1413) -> 
 allnc boole(boole -> n1413=n1413))
> all (nat=>nat),n(
 all n0(all n0((nat=>nat)n0<(nat=>nat)n0 -> n0=n0) -> n0=n0) -> 
 allnc boole0(boole0 -> n=n))
> ; ok, algebra list added
> ; ok, predicate variable P: (arity nat) added
> all n^1418(
 E n^1418 -> 
 P322 0 -> all n1419(P322 n1419 -> P322(Succ n1419)) -> P322 n^1418)
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity nat)
> ; ok, predicate variable P: (arity list nat) added
> ; ok, variable ns: list nat added
> all (list alpha39)^1420(
 SE(list alpha39)^1420 -> 
 (Pvar list alpha39)_323(Nil alpha39) -> 
 all alpha39^1422,(list alpha39)^1421(
  SE(list alpha39)^1421 -> 
  (Pvar list alpha39)_323(list alpha39)^1421 -> 
  (Pvar list alpha39)_323((Cons alpha39)alpha39^1422(list alpha39)^1421)) -> 
 (Pvar list alpha39)_323(list alpha39)^1420)
> ; Type substitution:
; alpha40	->	nat
; Predicate substitution:
; (Pvar list alpha40)_324	->	(cterm (ns^) P ns^)
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity list nat)
> ; ok, variable ns is removed
; warning: ns was default variable of type list nat
> ; ok, algebra list removed
; ok, constructor Cons removed
; ok, constructor Nil removed
> ; ok, predicate variable P: (arity nat) added
> all n1426(P 0 -> all n1427(P n1427 -> P(Succ n1427)) -> P n1426)
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity nat)
> ; ok, algebra tree added
; ok, algebra tlist added
> ; ok, predicate variable P: (arity tree) added
> ; ok, predicate variable Q: (arity tlist) added
> all tree1429(
 P Leaf -> 
 all tlist1432(Q tlist1432 -> P(Branch tlist1432)) -> 
 Q Empty -> 
 all tree1431,tlist1430(
  P tree1431 -> Q tlist1430 -> Q(Tcons tree1431 tlist1430)) -> 
 P tree1429)
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity tree)
; ok, predicate variable Q is removed
; warning: Q was default pvariable of arity (arity tlist)
> ; ok, algebra tree removed
; ok, algebra tlist removed
; ok, constructor Tcons removed
; ok, constructor Empty removed
; ok, constructor Branch removed
; ok, constructor Leaf removed
> ; ok, predicate variable P: (arity nat) added
> all n1433(P 0 -> all n1434 P(Succ n1434) -> P n1433)
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity nat)
> ; ok, variable h: alpha=>alpha=>nat added
> ; ok, variable x: alpha added
> ; ok, predicate variable R: (arity alpha alpha) added
> all h1435,x1436,x1437(
 all x1436,x1437(
  all x1438,x1439(h1435 x1438 x1439<h1435 x1436 x1437 -> R x1438 x1439) -> 
  R x1436 x1437) -> 
 allnc boole(boole -> R x1436 x1437))
> ; ok, inductively defined predicate constant Even added
> > > Even 0
> > allnc n^(Even n^ -> Even(n^ +2))
> > algEven=>algEven
> ; ok, predicate variable Q: (arity nat) added
> > allnc n^1448(
 Even n^1448 -> Q 0 -> allnc n^(Even n^ -> Q n^ -> Q(n^ +2)) -> Q n^1448)
> > algEven=>alpha42=>(algEven=>alpha42=>alpha42)=>alpha42
> ; ok, predicate variable Q is removed
; warning: Q was default pvariable of arity (arity nat)
> ; ok, inductively defined predicate constant Even removed
> ; ok, inductively defined predicate constant Ev added
; ok, inductively defined predicate constant Od added
> > > > Ev 0
> > allnc n^(Od n^ -> Ev(n^ +1))
> > allnc n^(Ev n^ -> Od(n^ +1))
> > algEv=>algOd
> ; ok, predicate variable Q: (arity nat) added
> > allnc n^1471(
 Ev n^1471 -> 
 Q1 0 -> 
 allnc n^(Od n^ -> Q2 n^ -> Q1(n^ +1)) -> 
 allnc n^(Ev n^ -> Q1 n^ -> Q2(n^ +1)) -> Q1 n^1471)
> > algEv=>
alpha45=>(algOd=>alpha46=>alpha45)=>(algEv=>alpha45=>alpha46)=>alpha45
> ; ok, predicate variable Q is removed
; warning: Q was default pvariable of arity (arity nat)
> ; ok, inductively defined predicate constant Ev removed
; ok, inductively defined predicate constant Od removed
> ; warning: x already is a variable of type alpha
; ok, variable y: alpha added
; ok, variable z: alpha added
> ; ok, predicate variable P: (arity) added
> ; ok, predicate variable Q: (arity alpha) added
> ; warning: R already is a predicate variable of arity (arity alpha alpha)
> ; ok, inductively defined predicate constant EqD added
> > > allnc x^ x^ eqd x^
> > algEqD
> > allnc x^1487,x^1486(
 x^1487 eqd x^1486 -> allnc x^ R x^ x^ -> R x^1487 x^1486)
> > algEqD=>alpha18=>alpha18
> ; ok, inductively defined predicate constant OrD added
> > > P1 -> P1 ord P2
> > P2 -> P1 ord P2
> > alpha15=>algOrD alpha15 alpha13
> > P1 ord P2 -> (P1 -> P) -> (P2 -> P) -> P
> > algOrD alpha15 alpha13=>(alpha15=>alpha49)=>(alpha13=>alpha49)=>alpha49
> ; ok, inductively defined predicate constant ExD added
> > "exd n n=m"
> > allnc m all n^1496(n^1496=m -> exd n^1497 n^1497=m)
> > nat=>algExD nat unit
> > allnc m,k(exd n^1505 n^1505=m -> all n^1506(n^1506=m -> k=0) -> k=0)
> > "exd n^ n^ =m"
> > allnc m all n^1508(n^1508=m -> exd n^1509 n^1509=m)
> > allnc m,k(exd n^1511 n^1511=m -> all n^1512(n^1512=m -> k=0) -> k=0)
> ; ok, inductively defined predicate constant PiOne added
> > "(PiOne (cterm (x^1535,x^1534) R x^1535 x^1534))"
> > all x^,y^(R x^ y^ -> (PiOne (cterm (x^1537,x^1536) R x^1537 x^1536))x^)
> > alpha=>alpha=>alpha18=>algPiOne alpha alpha18
> > allnc x^1548,k(
 (PiOne (cterm (x^1546,x^1545) R x^1546 x^1545))x^1548 -> 
 all x^,y^(R x^ y^ -> k=0) -> k=0)
> ; ok, inductively defined predicate constant TrCl added
> > "(TrCl (cterm (x^1535,x^1534) R x^1535 x^1534))"
> > allnc x^,y^(R x^ y^ -> (TrCl (cterm (x^1564,x^1563) R x^1564 x^1563))x^ y^)
> > alpha18=>algTrCl alpha18
> > allnc x^1577,x^1576,k(
 (TrCl (cterm (x^1573,x^1572) R x^1573 x^1572))x^1577 x^1576 -> 
 allnc x^,y^(R x^ y^ -> k=0) -> 
 allnc x^,y^,z^(
  R x^ y^ -> 
  (TrCl (cterm (x^1573,x^1572) R x^1573 x^1572))y^ z^ -> k=0 -> k=0) -> 
 k=0)
> ; ok, inductively defined predicate constant Acc added
> > > allnc x^(F -> (Acc (cterm (x^1590,x^1589) R x^1590 x^1589))x^)
> > algAcc alpha alpha18
> > allnc x^(
 all y^(R y^ x^ -> (Acc (cterm (x^1597,x^1596) R x^1597 x^1596))y^) -> 
 (Acc (cterm (x^1597,x^1596) R x^1597 x^1596))x^)
> > (alpha=>alpha18=>algAcc alpha alpha18)=>algAcc alpha alpha18
> > allnc x^1606,k(
 (Acc (cterm (x^1604,x^1603) R x^1604 x^1603))x^1606 -> 
 allnc x^(F -> k=0) -> 
 allnc x^(
  all y^(R y^ x^ -> (Acc (cterm (x^1604,x^1603) R x^1604 x^1603))y^) -> 
  all y^(R y^ x^ -> k=0) -> k=0) -> 
 k=0)
> ; ok, inductively defined predicate constant ExDT added
> > "exdt n n=m"
> > allnc m all n1610(n1610=m -> exdt n1611 n1611=m)
> > nat=>algExDT nat unit
> > allnc m,k(exdt n1619 n1619=m -> all n1620(n1620=m -> k=0) -> k=0)
> ; ok, inductively defined predicate constant Cup added
> > > all x^(
 Q1 x^ -> (Cup (cterm (x^1633) Q1 x^1633) (cterm (x^1632) Q2 x^1632))x^)
> > all x^(
 Q2 x^ -> (Cup (cterm (x^1636) Q1 x^1636) (cterm (x^1635) Q2 x^1635))x^)
> > alpha=>alpha25=>algCup alpha alpha25 alpha23
> > allnc x^1646(
 (Cup (cterm (x^1644) Q1 x^1644) (cterm (x^1643) Q2 x^1643))x^1646 -> 
 all x^(Q1 x^ -> P) -> all x^(Q2 x^ -> P) -> P)
> > algCup alpha alpha25 alpha23=>
(alpha=>alpha25=>alpha49)=>(alpha=>alpha23=>alpha49)=>alpha49
> ; ok, inductively defined predicate constant Cap added
> > > all x^(
 Q1 x^ -> 
 Q2 x^ -> (Cap (cterm (x^1658) Q1 x^1658) (cterm (x^1657) Q2 x^1657))x^)
> > alpha=>alpha25=>alpha23=>algCap alpha alpha25 alpha23
> > allnc x^1669(
 (Cap (cterm (x^1667) Q1 x^1667) (cterm (x^1666) Q2 x^1666))x^1669 -> 
 all x^(Q1 x^ -> Q2 x^ -> P) -> P)
> > algCap alpha alpha25 alpha23=>(alpha=>alpha25=>alpha23=>alpha49)=>alpha49
> ; ok, variable x is removed
; warning: x was default variable of type alpha
; ok, variable y is removed
; ok, variable z is removed
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity)
; ok, predicate variable Q is removed
; warning: Q was default pvariable of arity (arity alpha)
; ok, predicate variable R is removed
; warning: R was default pvariable of arity (arity alpha alpha)
> ; ok, inductively defined predicate constant EqD removed
; ok, inductively defined predicate constant OrD removed
; ok, inductively defined predicate constant ExD removed
; ok, inductively defined predicate constant PiOne removed
; ok, inductively defined predicate constant TrCl removed
; ok, inductively defined predicate constant Acc removed
; ok, inductively defined predicate constant ExDT removed
; ok, inductively defined predicate constant Cup removed
; ok, inductively defined predicate constant Cap removed
> ; ok, variable x: alpha added
> allnc alpha^ Equal alpha^ alpha^
> ; ?_1: all boole Equal boole boole
> ; ok, we now have the new goal 
; ?_2: Equal boole boole from
;   boole
> ; ok, ?_2 is proved.  Proof finished.
> ; ok, predicate variable P: (arity alpha) added
> ; ok, MPUnary has been added as a new global assumption.
; ok, program constant cMPUnary: alpha=>alpha57=>(alpha57=>alpha58)=>alpha58
; of t-degree 1 and arity 0 added
; warning: theorem cMPUnaryTotal stating totality missing
> ; ?_1: all x1 P3 x1
> ; ok, we now have the new goal 
; ?_2: P3 x1 from
;   x1
> ; ok, ?_2 can be obtained from
; ?_4: Total x5 -> P3 x1 from
;   x1  x5

; ?_3: Total x5 from
;   x1  x5
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity alpha)
> allnc alpha^1,alpha^2,alpha^3(
 Equal alpha^1 alpha^2 -> Equal alpha^2 alpha^3 -> Equal alpha^1 alpha^3)
> ; ?_1: all x Equal x x
> ; ok, we now have the new goal 
; ?_2: Equal x x from
;   x
> ; ok, ?_2 can be obtained from
; ?_4: Equal x1 x from
;   x  x1

; ?_3: Equal x x1 from
;   x  x1
> ; ok, variable x is removed
; warning: x was default variable of type alpha
> ; ok, predicate variable P: (arity nat) added
> ; ?_1: all n P n
> ; ok, ?_1 can be obtained from
; ?_3: all n1707(P n1707 -> P(Succ n1707)) from
;   n1705

; ?_2: P 0 from
;   n1705
> ; ?_1: all n^(E n^ -> P n^)
> ; ok, ?_1 can be obtained from
; ?_3: all n1710(P n1710 -> P(Succ n1710)) from
;   n^1708  1:E n^1708

; ?_2: P 0 from
;   n^1708  1:E n^1708
> ; ?_1: all n^ P n^
> ; ok, we now have the new goal 
; ?_2: P n^ from
;   n^
> ; ok, ?_2 can be obtained from
; ?_5: all n1714(P n1714 -> P(Succ n1714)) from
;   n^

; ?_4: P 0 from
;   n^

; ?_3: E n^ from
;   n^
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity nat)
> ; ok, algebra ordl added
> ; ok, predicate variable P: (arity ordl) added
> ; ?_1: all ordl P ordl
> ; ok, ?_1 can be obtained from
; ?_3: all (nat=>ordl)_1717(
;       all n1718 P((nat=>ordl)_1717 n1718) -> P(OrdSup(nat=>ordl)_1717)) from
;   ordl1715

; ?_2: P OrdZero from
;   ordl1715
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity ordl)
> ; ok, algebra ordl removed
; ok, constructor OrdSup removed
; ok, constructor OrdZero removed
> ; ok, algebra list added
> ; ok, predicate variable P: (arity list nat) added
> ; ok, variable ns: list nat added
> ; ?_1: all ns P ns
> ; ok, ?_1 can be obtained from
; ?_3: all n1724,ns1725(P ns1725 -> P((Cons nat)n1724 ns1725)) from
;   ns1719

; ?_2: P(Nil nat) from
;   ns1719
> ; ?_1: all ns^(SE ns^ -> P ns^)
> ; ok, ?_1 can be obtained from
; ?_3: all n^1731,ns^1732(SE ns^1732 -> P ns^1732 -> P((Cons nat)n^1731 ns^1732)) from
;   ns^1726  1:SE ns^1726

; ?_2: P(Nil nat) from
;   ns^1726  1:SE ns^1726
> ; ?_1: all ns^(STotal ns^ -> P ns^)
> ; ok, ?_1 can be obtained from
; ?_3: all n^1738,ns^1739(SE ns^1739 -> P ns^1739 -> P((Cons nat)n^1738 ns^1739)) from
;   ns^1733  1:SE ns^1733

; ?_2: P(Nil nat) from
;   ns^1733  1:SE ns^1733
> ; ?_1: all ns^ P ns^
> ; ok, we now have the new goal 
; ?_2: P ns^ from
;   ns^
> ; ok, ?_2 can be obtained from
; ?_5: all n^1746,ns^1747(SE ns^1747 -> P ns^1747 -> P((Cons nat)n^1746 ns^1747)) from
;   ns^

; ?_4: P(Nil nat) from
;   ns^

; ?_3: SE ns^ from
;   ns^
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity list nat)
> ; ok, variable ns is removed
; warning: ns was default variable of type list nat
> ; ok, predicate variable P: (arity list alpha) added
> ; ok, variable x: alpha added
> ; ok, variable xs: list alpha added
> ; ?_1: all xs P xs
> ; ok, ?_1 can be obtained from
; ?_3: all x1753,xs1754(P xs1754 -> P((Cons alpha)x1753 xs1754)) from
;   xs1748

; ?_2: P(Nil alpha) from
;   xs1748
> ; ?_1: all xs^(SE xs^ -> P xs^)
> ; ok, ?_1 can be obtained from
; ?_3: all x^1760,xs^1761(
;       SE xs^1761 -> P xs^1761 -> P((Cons alpha)x^1760 xs^1761)) from
;   xs^1755  1:SE xs^1755

; ?_2: P(Nil alpha) from
;   xs^1755  1:SE xs^1755
> ; ?_1: all xs^(STotal xs^ -> P xs^)
> ; ok, ?_1 can be obtained from
; ?_3: all x^1767,xs^1768(
;       SE xs^1768 -> P xs^1768 -> P((Cons alpha)x^1767 xs^1768)) from
;   xs^1762  1:SE xs^1762

; ?_2: P(Nil alpha) from
;   xs^1762  1:SE xs^1762
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity list alpha)
> ; ok, variable x is removed
; warning: x was default variable of type alpha
; ok, variable xs is removed
; warning: xs was default variable of type list alpha
> ; ok, algebra list removed
; ok, constructor Cons removed
; ok, constructor Nil removed
> ; ok, algebra tree added
; ok, algebra tlist added
> ; ok, predicate variable P: (arity tree) added
> ; ok, predicate variable Q: (arity tlist) added
> ; ?_1: all tree P tree
> ; ok, ?_1 can be obtained from
; ?_5: all tree1773,tlist1772(
;       P tree1773 -> Q tlist1772 -> Q(Tcons tree1773 tlist1772)) from
;   tree1769

; ?_4: Q Empty from
;   tree1769

; ?_3: all tlist1774(Q tlist1774 -> P(Branch tlist1774)) from
;   tree1769

; ?_2: P Leaf from
;   tree1769
> ; ?_1: all tree^(STotal tree^ -> P tree^)
> ; ok, ?_1 can be obtained from
; ?_5: all tree1779,tlist1778(
;       P tree1779 -> Q tlist1778 -> Q(Tcons tree1779 tlist1778)) from
;   tree^1775  1:E tree^1775

; ?_4: Q Empty from
;   tree^1775  1:E tree^1775

; ?_3: all tlist1780(Q tlist1780 -> P(Branch tlist1780)) from
;   tree^1775  1:E tree^1775

; ?_2: P Leaf from
;   tree^1775  1:E tree^1775
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity tree)
> ; ok, predicate variable Q is removed
; warning: Q was default pvariable of arity (arity tlist)
> ; ok, algebra tree removed
; ok, algebra tlist removed
; ok, constructor Tcons removed
; ok, constructor Empty removed
; ok, constructor Branch removed
; ok, constructor Leaf removed
> ; ok, algebra inftree added
; ok, algebra inftlist added
> ; ok, predicate variable P: (arity inftree) added
> ; ok, predicate variable Q: (arity inftlist) added
> ; ?_1: all inftree P inftree
> ; ok, ?_1 can be obtained from
; ?_6: all inftree1785,inftlist1784(
;       P inftree1785 -> 
;       Q inftlist1784 -> Q(Inftcons inftree1785 inftlist1784)) from
;   inftree1781

; ?_5: Q Emptyinftlist from
;   inftree1781

; ?_4: all boole1787,(boole=>inftree)_1786(
;       all boole1788 P((boole=>inftree)_1786 boole1788) -> 
;       P(Lim boole1787(boole=>inftree)_1786)) from
;   inftree1781

; ?_3: all boole1790,inftlist1789(
;       Q inftlist1789 -> P(Infbranch boole1790 inftlist1789)) from
;   inftree1781

; ?_2: all boole1791 P(Newleaf boole1791) from
;   inftree1781
> ; ?_1: all inftree^(STotal inftree^ -> P inftree^)
> ; ok, ?_1 can be obtained from
; ?_6: all inftree^1796,inftlist^1795(
;       STotal inftree^1796 -> 
;       STotal inftlist^1795 -> 
;       P inftree^1796 -> 
;       Q inftlist^1795 -> Q(Inftcons inftree^1796 inftlist^1795)) from
;   inftree^1792  1:STotal inftree^1792

; ?_5: Q Emptyinftlist from
;   inftree^1792  1:STotal inftree^1792

; ?_4: all boole^1798,(boole=>inftree)^1797(
;       SE boole^1798 -> 
;       all boole1799 STotal((boole=>inftree)^1797 boole1799) -> 
;       all boole1800 P((boole=>inftree)^1797 boole1800) -> 
;       P(Lim boole^1798(boole=>inftree)^1797)) from
;   inftree^1792  1:STotal inftree^1792

; ?_3: all boole^1802,inftlist^1801(
;       SE boole^1802 -> 
;       STotal inftlist^1801 -> 
;       Q inftlist^1801 -> P(Infbranch boole^1802 inftlist^1801)) from
;   inftree^1792  1:STotal inftree^1792

; ?_2: all boole^1803(SE boole^1803 -> P(Newleaf boole^1803)) from
;   inftree^1792  1:STotal inftree^1792
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity inftree)
; ok, predicate variable Q is removed
; warning: Q was default pvariable of arity (arity inftlist)
> ; ok, algebra inftree removed
; ok, algebra inftlist removed
; ok, constructor Inftcons removed
; ok, constructor Emptyinftlist removed
; ok, constructor Lim removed
; ok, constructor Infbranch removed
; ok, constructor Newleaf removed
> ; ok, predicate variable P: (arity nat) added
> ; ?_1: all n P n
> ; ok, ?_1 can be obtained from
; ?_3: all n1806 P(Succ n1806) from
;   n1804

; ?_2: P 0 from
;   n1804
> ; ?_1: all n^(E n^ -> P n^)
> ; ok, ?_1 can be obtained from
; ?_3: all n1809 P(Succ n1809) from
;   n^1807  1:E n^1807

; ?_2: P 0 from
;   n^1807  1:E n^1807
> ; ?_1: all n^ P n^
> ; ok, we now have the new goal 
; ?_2: P n^ from
;   n^
> ; ok, ?_2 can be obtained from
; ?_5: all n1815(Equal n^(Succ n1815) -> P(Succ n1815)) from
;   n^

; ?_4: Equal n^ 0 -> P 0 from
;   n^

; ?_3: E n^ from
;   n^
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity nat)
> ; ok, algebra ordl added
> ; ok, predicate variable P: (arity ordl) added
> ; ?_1: all ordl P ordl
> ; ok, ?_1 can be obtained from
; ?_3: all (nat=>ordl)_1818 P(OrdSup(nat=>ordl)_1818) from
;   ordl1816

; ?_2: P OrdZero from
;   ordl1816
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity ordl)
> ; ok, algebra ordl removed
; ok, constructor OrdSup removed
; ok, constructor OrdZero removed
> ; ok, algebra list added
> ; ok, predicate variable P: (arity list nat) added
> ; ok, variable ns: list nat added
> ; ?_1: all ns P ns
> ; ok, ?_1 can be obtained from
; ?_3: all n1824,ns1825 P((Cons nat)n1824 ns1825) from
;   ns1819

; ?_2: P(Nil nat) from
;   ns1819
> ; ?_1: all ns^(SE ns^ -> P ns^)
> ; ok, ?_1 can be obtained from
; ?_3: all n^1831,ns^1832(SE ns^1832 -> P((Cons nat)n^1831 ns^1832)) from
;   ns^1826  1:SE ns^1826

; ?_2: P(Nil nat) from
;   ns^1826  1:SE ns^1826
> ; ?_1: all ns^(STotal ns^ -> P ns^)
> ; ok, ?_1 can be obtained from
; ?_3: all n^1838,ns^1839(SE ns^1839 -> P((Cons nat)n^1838 ns^1839)) from
;   ns^1833  1:SE ns^1833

; ?_2: P(Nil nat) from
;   ns^1833  1:SE ns^1833
> ; ?_1: all ns^ P ns^
> ; ok, we now have the new goal 
; ?_2: P ns^ from
;   ns^
> ; ok, ?_2 can be obtained from
; ?_5: all n^1848,ns^1849(
;       SE ns^1849 -> 
;       Equal ns^((Cons nat)n^1848 ns^1849) -> P((Cons nat)n^1848 ns^1849)) from
;   ns^

; ?_4: Equal ns^(Nil nat) -> P(Nil nat) from
;   ns^

; ?_3: SE ns^ from
;   ns^
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity list nat)
> ; ok, variable ns is removed
; warning: ns was default variable of type list nat
> ; ok, predicate variable P: (arity list alpha) added
> ; ok, variable x: alpha added
> ; ok, variable xs: list alpha added
> ; ?_1: all xs P xs
> ; ok, ?_1 can be obtained from
; ?_3: all x1855,xs1856 P((Cons alpha)x1855 xs1856) from
;   xs1850

; ?_2: P(Nil alpha) from
;   xs1850
> ; ?_1: all xs^(SE xs^ -> P xs^)
> ; ok, ?_1 can be obtained from
; ?_3: all x^1862,xs^1863(SE xs^1863 -> P((Cons alpha)x^1862 xs^1863)) from
;   xs^1857  1:SE xs^1857

; ?_2: P(Nil alpha) from
;   xs^1857  1:SE xs^1857
> ; ?_1: all xs^(STotal xs^ -> P xs^)
> ; ok, ?_1 can be obtained from
; ?_3: all x^1869,xs^1870(SE xs^1870 -> P((Cons alpha)x^1869 xs^1870)) from
;   xs^1864  1:SE xs^1864

; ?_2: P(Nil alpha) from
;   xs^1864  1:SE xs^1864
> ; ok, predicate variable P is removed
; warning: P was default pvariable of arity (arity list alpha)
> ; ok, variable x is removed
; warning: x was default variable of type alpha
; ok, variable xs is removed
; warning: xs was default variable of type list alpha
> ; ok, algebra list removed
; ok, constructor Cons removed
; ok, constructor Nil removed
> ; ?_1: all boole^(STotal boole^ -> boole^ =boole^)
> ; ok, ?_1 can be obtained from
; ?_3: False=False from
;   boole^1871  1:E boole^1871

; ?_2: True=True from
;   boole^1871  1:E boole^1871
> ; ok, ?_2 is proved.  The active goal now is
; ?_3: False=False from
;   boole^1871  1:E boole^1871
> ; ok, ?_3 is proved.  Proof finished.
> ; ?_1: all boole^ boole^ =boole^
> ; ok, we now have the new goal 
; ?_2: boole^ =boole^ from
;   boole^
> ; ok, ?_2 can be obtained from
; ?_5: (boole^ -> F) -> False=False from
;   boole^

; ?_4: boole^ -> True=True from
;   boole^

; ?_3: E boole^ from
;   boole^
> ; ok, inductively defined predicate constant Even added
> ; ?_1: allnc n^(Even n^ -> ex m n^ =m+m)
> ; ok, we now have the new goal 
; ?_2: Even n^ -> ex m n^ =m+m from
;   {n^}
> ; ok, ?_2 can be obtained from
; ?_4: allnc n^(Even n^ -> ex m n^ =m+m -> ex m n^ +2=m+m) from
;   {n^}  1:Even n^

; ?_3: ex m 0=m+m from
;   {n^}  1:Even n^
> ; ok, ?_3 can be obtained from
; ?_5: 0=0+0 from
;   {n^}  1:Even n^
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: allnc n^(Even n^ -> ex m n^ =m+m -> ex m n^ +2=m+m) from
;   {n^}  1:Even n^
> ; ok, we now have the new goal 
; ?_6: ex m n^1+2=m+m from
;   {n^}  1:Even n^
;   {n^1}  Even n^1:Even n^1
;   IH:ex m n^1=m+m
> ; ok, we now have the new goal 
; ?_9: ex m n^1+2=m+m from
;   {n^}  1:Even n^
;   {n^1}  Even n^1:Even n^1
;   m  n^1=m+m:n^1=m+m
> ; ok, ?_9 can be obtained from
; ?_10: n^1+2=m+1+(m+1) from
;   {n^}  1:Even n^
;   {n^1}  Even n^1:Even n^1
;   m  n^1=m+m:n^1=m+m
> ; ok, the normalized goal is
; ?_11: n^1=m+m from
;   {n^}  1:Even n^
;   {n^1}  Even n^1:Even n^1
;   m  n^1=m+m:n^1=m+m
> ; ok, ?_11 is proved.  Proof finished.
> > > [algEven0](Rec algEven=>nat)algEven0 0([algEven1]Succ)
> ; ok, inductively defined predicate constant Even removed
> ; ok, inductively defined predicate constant Ev added
; ok, inductively defined predicate constant Od added
> ; ?_1: allnc n^(Ev n^ -> ex m n^ =m+m)
> ; ok, we now have the new goal 
; ?_2: Ev n^ -> ex m n^ =m+m from
;   {n^}
> ; ok, ?_2 can be obtained from
; ?_5: allnc n^(Ev n^ -> ex m n^ =m+m -> ex m n^ +1=m+m+1) from
;   {n^}  1:Ev n^

; ?_4: allnc n^(Od n^ -> ex m n^ =m+m+1 -> ex m n^ +1=m+m) from
;   {n^}  1:Ev n^

; ?_3: ex m 0=m+m from
;   {n^}  1:Ev n^
> ; ok, ?_3 can be obtained from
; ?_6: 0=0+0 from
;   {n^}  1:Ev n^
> ; ok, ?_6 is proved.  The active goal now is
; ?_4: allnc n^(Od n^ -> ex m n^ =m+m+1 -> ex m n^ +1=m+m) from
;   {n^}  1:Ev n^
> ; ok, we now have the new goal 
; ?_7: ex m n^1+1=m+m from
;   {n^}  1:Ev n^
;   {n^1}  Od n^1:Od n^1
;   H1:ex m n^1=m+m+1
> ; ok, we now have the new goal 
; ?_10: ex m n^1+1=m+m from
;   {n^}  1:Ev n^
;   {n^1}  Od n^1:Od n^1
;   m  H2:n^1=m+m+1
> ; ok, ?_10 can be obtained from
; ?_11: n^1+1=Succ m+Succ m from
;   {n^}  1:Ev n^
;   {n^1}  Od n^1:Od n^1
;   m  H2:n^1=m+m+1
> ; ok, ?_11 is proved.  The active goal now is
; ?_5: allnc n^(Ev n^ -> ex m n^ =m+m -> ex m n^ +1=m+m+1) from
;   {n^}  1:Ev n^
> ; ok, we now have the new goal 
; ?_12: ex m n^1+1=m+m+1 from
;   {n^}  1:Ev n^
;   {n^1}  Ev n^1:Ev n^1
;   H1:ex m n^1=m+m
> ; ok, we now have the new goal 
; ?_15: ex m n^1+1=m+m+1 from
;   {n^}  1:Ev n^
;   {n^1}  Ev n^1:Ev n^1
;   m  H2:n^1=m+m
> ; ok, ?_15 can be obtained from
; ?_16: n^1+1=m+m+1 from
;   {n^}  1:Ev n^
;   {n^1}  Ev n^1:Ev n^1
;   m  H2:n^1=m+m
> ; ok, ?_16 is proved.  Proof finished.
> > > [algEv0](Rec algEv=>nat algOd=>nat)algEv0 0([algOd1]Succ)([algEv1,n2]n2)
> ; ok, inductively defined predicate constant Ev removed
; ok, inductively defined predicate constant Od removed
> ; ok, variable x: alpha added
; ok, variable y: alpha added
; ok, variable z: alpha added
> ; ok, predicate variable Q: (arity alpha) added
> ; ok, inductively defined predicate constant EqD added
> ; ?_1: all x^ x^ eqd x^
> ; ok, we now have the new goal 
; ?_2: x^ eqd x^ from
;   x^
> ; ok, ?_2 is proved.  Proof finished.
> ; ok, EqDRefl has been added as a new theorem.
> ; ?_1: all x^,y^(x^ eqd y^ -> Q x^ -> Q y^)
> ; ok, we now have the new goal 
; ?_2: x^ eqd y^ -> Q x^ -> Q y^ from
;   x^  y^
> ; ok, ?_2 can be obtained from
; ?_3: allnc x^(Q x^ -> Q x^) from
;   x^  y^  1:x^ eqd y^
> ; ok, we now have the new goal 
; ?_4: Q x^1 from
;   x^  y^  1:x^ eqd y^
;   {x^1}  H1:Q x^1
> ; ok, ?_4 is proved.  Proof finished.
> ; ok, EqDCompat has been added as a new theorem.
; ok, program constant cEqDCompat: alpha=>alpha=>alpha16=>alpha16
; of t-degree 0 and arity 0 added
> ; ?_1: all x^,y^(x^ eqd y^ -> y^ eqd x^)
> ; ok, we now have the new goal 
; ?_2: y^ eqd x^ from
;   x^  y^  H1:x^ eqd y^
> ; ok, ?_2 can be obtained from
; ?_4: x^ eqd x^ from
;   x^  y^  H1:x^ eqd y^

; ?_3: x^ eqd y^ from
;   x^  y^  H1:x^ eqd y^
> ; ok, ?_3 is proved.  The active goal now is
; ?_4: x^ eqd x^ from
;   x^  y^  H1:x^ eqd y^
> ; ok, ?_4 is proved.  Proof finished.
> ; ok, EqDSym has been added as a new theorem.
> ; ?_1: all x^,y^,z^(x^ eqd y^ -> y^ eqd z^ -> x^ eqd z^)
> ; ok, we now have the new goal 
; ?_2: y^ eqd z^ -> x^ eqd z^ from
;   x^  y^  z^  H1:x^ eqd y^
> ; ok, ?_2 can be obtained from
; ?_4: x^ eqd z^ -> x^ eqd z^ from
;   x^  y^  z^  H1:x^ eqd y^

; ?_3: x^ eqd y^ from
;   x^  y^  z^  H1:x^ eqd y^
> ; ok, ?_3 is proved.  The active goal now is
; ?_4: x^ eqd z^ -> x^ eqd z^ from
;   x^  y^  z^  H1:x^ eqd y^
> ; ok, we now have the new goal 
; ?_5: x^ eqd z^ from
;   x^  y^  z^  H1:x^ eqd y^
;   H2:x^ eqd z^
> ; ok, ?_5 is proved.  Proof finished.
> ; ok, EqDTrans has been added as a new theorem.
> ; ?_1: all x^,y^(False eqd True -> x^ eqd y^)
> ; ok, we now have the new goal 
; ?_2: x^ eqd y^ from
;   x^  y^  FF:False eqd True
> ; ok, ?_2 can be obtained from
; ?_4: [if False x^ y^]eqd[if False x^ y^] from
;   x^  y^  FF:False eqd True

; ?_3: False eqd True from
;   x^  y^  FF:False eqd True
> ; ok, ?_3 is proved.  The active goal now is
; ?_4: [if False x^ y^]eqd[if False x^ y^] from
;   x^  y^  FF:False eqd True
> ; ok, ?_4 is proved.  Proof finished.
> ; ok, EFEdD has been added as a new theorem.
> ; ok, variable x is removed
; warning: x was default variable of type alpha
; ok, variable y is removed
; ok, variable z is removed
> ; ok, predicate variable Q is removed
; warning: Q was default pvariable of arity (arity alpha)
> ; ok, inductively defined predicate constant EqD removed
> ; ok, inductively defined predicate constant Even added
> ; ?_1: all n(Even(Succ(Succ n)) -> Even n)
> ; ok, we now have the new goal 
; ?_2: Even n from
;   n  H:Even(Succ(Succ n))
> ; ok, ?_2 can be obtained from
; ?_3: allnc n^(
;       Even n^ -> 
;       (Succ(Succ n)=n^ -> Even n) -> Succ(Succ n)=n^ +2 -> Even n) from
;   n  H:Even(Succ(Succ n))
> ; ok, we now have the new goal 
; ?_4: Even m^ -> (Succ(Succ n)=m^ -> Even n) -> Succ(Succ n)=m^ +2 -> Even n from
;   n  H:Even(Succ(Succ n))
;   {m^}
> ; ok, the normalized goal is
; ?_5: Even m^ -> (Succ(Succ n)=m^ -> Even n) -> n=m^ -> Even n from
;   n  H:Even(Succ(Succ n))
;   {m^}
> ; ok, we now have the new goal 
; ?_6: Even n from
;   n  H:Even(Succ(Succ n))
;   {m^}  Even m^:Even m^
;   H1:Succ(Succ n)=m^ -> Even n
;   n=m^:n=m^
> ; ok, ?_6 can be obtained from
; ?_7: Even m^ from
;   n  H:Even(Succ(Succ n))
;   {m^}  Even m^:Even m^
;   H1:Succ(Succ n)=m^ -> Even n
;   n=m^:n=m^
> ; ok, ?_7 is proved.  Proof finished.
> ; ok, inductively defined predicate constant Even removed
> > > loading list.scm ...
> > ; ok, variable l: nat added
> ; ok, algebra type added
> > > ; ok, variable rho: type added
; ok, variable sig: type added
; ok, variable tau: type added
> ; ok, program constant Argtyp: type=>type
; of t-degree 1 and arity 1 added
; warning: theorem ArgtypTotal stating totality missing
> ; ok, program constant Valtyp: type=>type
; of t-degree 1 and arity 1 added
; warning: theorem ValtypTotal stating totality missing
> ; ok, program constant Arrowtyp: type=>boole
; of t-degree 1 and arity 1 added
; warning: theorem ArrowtypTotal stating totality missing
> ; ok, computation rule Argtyp Iota -> Iota added
> ; ok, computation rule Valtyp Iota -> Iota added
> ; ok, computation rule Argtyp(rho to sig) -> rho added
> ; ok, computation rule Valtyp(rho to sig) -> sig added
> ; ok, computation rule Arrowtyp Iota -> False added
> ; ok, computation rule Arrowtyp(rho to sig) -> True added
> ; ok, algebra term added
> > > ; ok, variable r: term added
; ok, variable s: term added
; ok, variable t: term added
> ; ok, variable rs: list term added
; ok, variable ss: list term added
; ok, variable ts: list term added
> ; ok, variable rhos: list type added
; ok, variable sigs: list type added
; ok, variable taus: list type added
> ; ok, program constant Typ: list type=>term=>type
; of t-degree 1 and arity 2 added
; warning: theorem TypTotal stating totality missing
> ; ok, computation rule Typ(Nil type)(Var n) -> Iota added
> ; ok, computation rule Typ(rho::rhos)(Var 0) -> rho added
> ; ok, computation rule Typ(rho::rhos)(Var(Succ n)) -> Typ rhos(Var n) added
> ; ok, computation rule Typ rhos(r s) -> Valtyp(Typ rhos r) added
> ; ok, computation rule Typ rhos(Abs rho r) -> rho to Typ(rho::rhos)r added
> ; ok, program constant Cor: list type=>term=>boole
; of t-degree 1 and arity 2 added
; warning: theorem CorTotal stating totality missing
> ; ok, computation rule Cor rhos(Var n) -> n<Lh rhos added
> ; ok, computation rule Cor rhos(r s) -> Cor rhos r andb Cor rhos s andb Typ rhos r=(Typ rhos s to Valtyp(Typ rhos r)) added
> ; ok, computation rule Cor rhos(Abs rho r) -> Cor(rho::rhos)r added
> ; ok, program constant Lift: term=>nat=>nat=>term
; of t-degree 1 and arity 3 added
; warning: theorem LiftTotal stating totality missing
> ; ok, computation rule Lift(Var n)l k -> [if (n<l) (Var n) (Var(n+k))] added
> ; ok, computation rule Lift(r s)l k -> Lift r l k(Lift s l k) added
> ; ok, computation rule Lift(Abs rho r)l k -> Abs rho(Lift r(l+1)k) added
> ; ok, algebra sub added
> ; ok, variable theta: sub added
> ; ok, program constant Sublift: sub=>nat=>sub
; of t-degree 1 and arity 2 added
; warning: theorem SubliftTotal stating totality missing
> ; ok, computation rule Sublift(Up m)n -> Up(m+n) added
> ; ok, computation rule Sublift(Dot r theta)n -> Dot(Lift r 0 n)(Sublift theta n) added
> ; ok, program constant Mksub: list term=>nat=>sub
; of t-degree 1 and arity 2 added
; warning: theorem MksubTotal stating totality missing
> ; ok, computation rule Mksub(Nil term)n -> Up n added
> ; ok, computation rule Mksub(r::rs)n -> Dot r(Mksub rs n) added
> ; ok, program constant Sublist: sub=>list term
; of t-degree 1 and arity 1 added
; warning: theorem SublistTotal stating totality missing
> ; ok, computation rule Sublist(Up n) -> (Nil term) added
> ; ok, computation rule Sublist(Dot r theta) -> r::Sublist theta added
> ; ok, program constant Subup: sub=>nat
; of t-degree 1 and arity 1 added
; warning: theorem SubupTotal stating totality missing
> ; ok, computation rule Subup(Up n) -> n added
> ; ok, computation rule Subup(Dot r theta) -> Subup theta added
> ; ok, program constant Sub: term=>sub=>term
; of t-degree 1 and arity 2 added
; warning: theorem SubTotal stating totality missing
> ; ok, computation rule Sub(Var n)(Up m) -> Var(n+m) added
> ; ok, computation rule Sub(Var 0)(Dot r theta) -> r added
> ; ok, computation rule Sub(Var(Succ n))(Dot r theta) -> Sub(Var n)theta added
> ; ok, computation rule Sub(r s)theta -> Sub r theta(Sub s theta) added
> ; ok, computation rule Sub(Abs rho r)theta -> Abs rho(Sub r(Dot(Var 0)(Sublift theta 1))) added
> ; ok, program constant Wrap: nat=>list term=>sub
; of t-degree 1 and arity 2 added
; warning: theorem WrapTotal stating totality missing
> ; ok, computation rule Wrap n(Nil term) -> Up n added
> ; ok, computation rule Wrap n(r::rs) -> Dot r(Wrap n rs) added
> ; ok, program constant Eta: type=>term=>term
; of t-degree 1 and arity 2 added
; warning: theorem EtaTotal stating totality missing
> ; ok, computation rule Eta Iota r -> r added
> ; ok, computation rule Eta(rho to sig)r -> Abs rho(Eta sig(Lift r 0 1(Eta rho(Var 0)))) added
> Abs Iota(Var 1(Var 0))
> Abs Iota(Var 8(Var 0))
> Abs(Iota to Iota)(Abs Iota(Var 9(Abs Iota(Var 2(Var 0)))(Var 0)))
> ; ok, program constant Exp: list type=>type=>term=>term
; of t-degree 1 and arity 3 added
; warning: theorem ExpTotal stating totality missing
> ; ok, program constant IExp: list type=>term=>term
; of t-degree 1 and arity 2 added
; warning: theorem IExpTotal stating totality missing
> ; ok, computation rule Exp rhos rho(Var n) -> Eta rho(Var n) added
> ; ok, computation rule Exp rhos rho(r s) -> Eta rho(IExp rhos(r s)) added
> ; ok, computation rule Exp rhos tau(Abs rho r) -> Abs rho(Exp(rho::rhos)(Valtyp tau)r) added
> ; ok, computation rule IExp rhos(Var n) -> Var n added
> ; ok, computation rule IExp rhos(r s) -> IExp rhos r(Exp rhos(Typ rhos s)s) added
> Abs rho(Abs sig(Var 1))
> Abs(rho to sig to rho)(Abs(rho to sig)(Abs rho(Var 2(Var 0)(Var 1(Var 0)))))
> > > Typ(Nil type)
(Abs((Iota to Iota)to Iota to Iota to Iota)
 (Abs((Iota to Iota)to Iota)(Abs(Iota to Iota)(Var 2(Var 0)(Var 1(Var 0))))))
> ((Iota to Iota)to Iota to Iota to Iota)to
((Iota to Iota)to Iota)to(Iota to Iota)to Iota to Iota
> Abs((Iota to Iota)to Iota to Iota to Iota)
(Abs((Iota to Iota)to Iota)
 (Abs(Iota to Iota)
  (Abs Iota
   (Var 3(Abs Iota(Var 2(Var 0)))(Var 2(Abs Iota(Var 2(Var 0))))(Var 0)))))
> ; ok, program constant FoldApp: term=>list term=>term
; of t-degree 1 and arity 2 added
; warning: theorem FoldAppTotal stating totality missing
> ; ok, computation rule FoldApp r(Nil term) -> r added
> ; ok, computation rule FoldApp r(s::ss) -> FoldApp(r s)ss added
> ; ok, inductively defined predicate constant WN added
; ok, inductively defined predicate constant WNs added
> ; ?_1: all r,s,rs,ss(WNs(r::rs)(s::ss) -> WNs rs ss)
> ; ok, we now have the new goal 
; ?_2: WNs rs ss from
;   r  s  rs  ss  WNs(r::rs)(s::ss):
;     WNs(r::rs)(s::ss)
> ; ok, ?_2 can be obtained from
; ?_3: all r3026,s3027,rs3028,ss3029(
;       WNs rs3028 ss3029 -> 
;       ((r::rs)=rs3028 -> (s::ss)=ss3029 -> WNs rs ss) -> 
;       (r::rs)=(r3026::rs3028) -> (s::ss)=(s3027::ss3029) -> WNs rs ss) from
;   r  s  rs  ss  WNs(r::rs)(s::ss):
;     WNs(r::rs)(s::ss)
> ; ok, we now have the new goal 
; ?_4: WNs rs1 ss1 -> 
;      ((r::rs)=rs1 -> (s::ss)=ss1 -> WNs rs ss) -> 
;      (r::rs)=(r1::rs1) -> (s::ss)=(s1::ss1) -> WNs rs ss from
;   r  s  rs  ss  WNs(r::rs)(s::ss):
;     WNs(r::rs)(s::ss)
;   r1  s1  rs1  ss1
> ; ok, we now have the new goal 
; ?_5: WNs rs ss from
;   r  s  rs  ss  WNs(r::rs)(s::ss):
;     WNs(r::rs)(s::ss)
;   r1  s1  rs1  ss1  WNs rs1 ss1:
;     WNs rs1 ss1
;   H1:(r::rs)=rs1 -> (s::ss)=ss1 -> WNs rs ss
;   (r::rs)=(r1::rs1):(r::rs)=(r1::rs1)
;   (s::ss)=(s1::ss1):(s::ss)=(s1::ss1)
> ; ok, the normalized goal is
; ?_6: WNs rs ss from
;   r  s  rs  ss  WNs(r::rs)(s::ss):
;     WNs(r::rs)(s::ss)
;   r1  s1  rs1  ss1  WNs rs1 ss1:
;     WNs rs1 ss1
;   H1:(r::rs)=rs1 -> (s::ss)=ss1 -> WNs rs ss
;   (r::rs)=(r1::rs1):r=r1 andb rs=rs1
;   (s::ss)=(s1::ss1):s=s1 andb ss=ss1
> ; ok, ?_6 can be obtained from
; ?_8: WNs rs ss from
;   r  s  rs  ss  WNs(r::rs)(s::ss):
;     WNs(r::rs)(s::ss)
;   r1  s1  rs1  ss1  WNs rs1 ss1:
;     WNs rs1 ss1
;   H1:(r::rs)=rs1 -> (s::ss)=ss1 -> WNs rs ss
;   (r::rs)=(r1::rs1):r=r1 andb rs=rs1
;   (s::ss)=(s1::ss1):s=s1 andb ss=ss1
;   rs=rs1:rs=rs1
> ; ok, ?_8 can be obtained from
; ?_9: WNs rs1 ss from
;   r  s  rs  ss  WNs(r::rs)(s::ss):
;     WNs(r::rs)(s::ss)
;   r1  s1  rs1  ss1  WNs rs1 ss1:
;     WNs rs1 ss1
;   H1:(r::rs)=rs1 -> (s::ss)=ss1 -> WNs rs ss
;   (r::rs)=(r1::rs1):r=r1 andb rs=rs1
;   (s::ss)=(s1::ss1):s=s1 andb ss=ss1
;   rs=rs1:rs=rs1
> ; ok, ?_9 can be obtained from
; ?_11: WNs rs1 ss from
;   r  s  rs  ss  WNs(r::rs)(s::ss):
;     WNs(r::rs)(s::ss)
;   r1  s1  rs1  ss1  WNs rs1 ss1:
;     WNs rs1 ss1
;   H1:(r::rs)=rs1 -> (s::ss)=ss1 -> WNs rs ss
;   (r::rs)=(r1::rs1):r=r1 andb rs=rs1
;   (s::ss)=(s1::ss1):s=s1 andb ss=ss1
;   rs=rs1:rs=rs1
;   ss=ss1:ss=ss1
> ; ok, ?_11 can be obtained from
; ?_12: WNs rs1 ss1 from
;   r  s  rs  ss  WNs(r::rs)(s::ss):
;     WNs(r::rs)(s::ss)
;   r1  s1  rs1  ss1  WNs rs1 ss1:
;     WNs rs1 ss1
;   H1:(r::rs)=rs1 -> (s::ss)=ss1 -> WNs rs ss
;   (r::rs)=(r1::rs1):r=r1 andb rs=rs1
;   (s::ss)=(s1::ss1):s=s1 andb ss=ss1
;   rs=rs1:rs=rs1
;   ss=ss1:ss=ss1
> ; ok, ?_12 is proved.  Proof finished.
> > [r,s,rs,ss,algWNs3060]
 (Rec algWNs=>algWNs)algWNs3060 cWNsNil
 ([r1,s1,rs1,ss1,algWNs3067,algWNs3068]
   ([algWNs3063]algWNs3063)(([algWNs3066]algWNs3066)algWNs3067))
> ; ?_1: all r,rs,ss(WNs(r::rs)ss -> ss=(Nil term) -> F)
> ; ok, we now have the new goal 
; ?_2: ss=(Nil term) -> F from
;   r  rs  ss  H1:WNs(r::rs)ss
> ; ok, ?_2 can be obtained from
; ?_3: all r3080,s,rs3081,ss3082(
;       WNs rs3081 ss3082 -> 
;       ((r::rs)=rs3081 -> ss=ss3082 -> ss=(Nil term) -> F) -> 
;       (r::rs)=(r3080::rs3081) -> ss=(s::ss3082) -> ss=(Nil term) -> F) from
;   r  rs  ss  H1:WNs(r::rs)ss
> ; ok, we now have the new goal 
; ?_4: ss=(Nil term) -> F from
;   r  rs  ss  H1:WNs(r::rs)ss
;   r1  s1  rs1  ss1  H2:WNs rs1 ss1
;   H3:(r::rs)=rs1 -> ss=ss1 -> ss=(Nil term) -> F
;   H4:(r::rs)=(r1::rs1)
;   H5:ss=(s1::ss1)
> ; ok, ?_4 can be obtained from
; ?_5: (s1::ss1)=(Nil term) -> F from
;   r  rs  ss  H1:WNs(r::rs)ss
;   r1  s1  rs1  ss1  H2:WNs rs1 ss1
;   H3:(r::rs)=rs1 -> ss=ss1 -> ss=(Nil term) -> F
;   H4:(r::rs)=(r1::rs1)
;   H5:ss=(s1::ss1)
> ; ok, ?_5 is proved in minimal propositional logic.  Proof finished.
> ; ?_1: all rs,ss(WNs rs ss -> rs=(Nil term) -> ss=(Nil term))
> ; ok, we now have the new goal 
; ?_2: WNs rs ss -> rs=(Nil term) -> ss=(Nil term) from
;   rs  ss
> ; ok, ?_2 can be obtained from
; ?_4: all r,s,rs,ss(
;       WNs rs ss -> 
;       (rs=(Nil term) -> ss=(Nil term)) -> 
;       (r::rs)=(Nil term) -> (s::ss)=(Nil term)) from
;   rs  ss  1:WNs rs ss

; ?_3: (Nil term)=(Nil term) -> (Nil term)=(Nil term) from
;   rs  ss  1:WNs rs ss
> ; ok, ?_3 is proved in minimal propositional logic.  The active goal now is
; ?_4: all r,s,rs,ss(
;       WNs rs ss -> 
;       (rs=(Nil term) -> ss=(Nil term)) -> 
;       (r::rs)=(Nil term) -> (s::ss)=(Nil term)) from
;   rs  ss  1:WNs rs ss
> ; ok, we now have the new goal 
; ?_5: (s::ss3105)=(Nil term) from
;   rs  ss  1:WNs rs ss
;   r  s  rs3104  ss3105  2:
;     WNs rs3104 ss3105
;   3:rs3104=(Nil term) -> ss3105=(Nil term)
;   4:(r::rs3104)=(Nil term)
> ; ok, ?_5 is proved in minimal propositional logic.  Proof finished.
> ; ?_1: all ss(WNs(Nil term)ss -> ss=(Nil term))
> ; ok, we now have the new goal 
; ?_2: ss=(Nil term) from
;   ss  H1:WNs(Nil term)ss
> ; ok, ?_2 can be obtained from
; ?_3: (Nil term)=(Nil term) -> ss=(Nil term) -> ss=(Nil term) from
;   ss  H1:WNs(Nil term)ss
> ; ok, ?_3 is proved in minimal propositional logic.  Proof finished.
> ; ?_1: all rs1,ss1,rs2,ss2(
;       WNs rs1 ss1 -> WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
> ; ok, ?_1 can be obtained from
; ?_3: all r3127,rs3128(
;       all ss1,rs2,ss2(
;        WNs rs3128 ss1 -> WNs rs2 ss2 -> WNs(rs3128:+:rs2)(ss1:+:ss2)) -> 
;       all ss1,rs2,ss2(
;        WNs(r3127::rs3128)ss1 -> 
;        WNs rs2 ss2 -> WNs((r3127::rs3128):+:rs2)(ss1:+:ss2))) from
;   rs3122

; ?_2: all ss1,rs2,ss2(
;       WNs(Nil term)ss1 -> WNs rs2 ss2 -> WNs((Nil term):+:rs2)(ss1:+:ss2)) from
;   rs3122
> ; ok, ?_2 can be obtained from
; ?_5: all r3134,rs3135,rs2,ss2(
;       WNs(Nil term)(r3134::rs3135) -> 
;       WNs rs2 ss2 -> WNs((Nil term):+:rs2)((r3134::rs3135):+:ss2)) from
;   rs3122  ss3129

; ?_4: all rs2,ss2(
;       WNs(Nil term)(Nil term) -> 
;       WNs rs2 ss2 -> WNs((Nil term):+:rs2)((Nil term):+:ss2)) from
;   rs3122  ss3129
> ; ok, we now have the new goal 
; ?_6: WNs((Nil term):+:rs2)((Nil term):+:ss2) from
;   rs3122  ss3129  rs2  ss2  1:
;     WNs(Nil term)(Nil term)
;   2:WNs rs2 ss2
> ; ok, the normalized goal is
; ?_7: WNs rs2 ss2 from
;   rs3122  ss3129  rs2  ss2  1:
;     WNs(Nil term)(Nil term)
;   2:WNs rs2 ss2
> ; ok, ?_7 is proved.  The active goal now is
; ?_5: all r3134,rs3135,rs2,ss2(
;       WNs(Nil term)(r3134::rs3135) -> 
;       WNs rs2 ss2 -> WNs((Nil term):+:rs2)((r3134::rs3135):+:ss2)) from
;   rs3122  ss3129
> ; ok, we now have the new goal 
; ?_8: WNs((Nil term):+:rs2)((r3134::rs3135):+:ss2) from
;   rs3122  ss3129  r3134  rs3135  rs2  ss2  1:
;     WNs(Nil term)(r3134::rs3135)
;   2:WNs rs2 ss2
> ; ok, ?_8 is proved.  The active goal now is
; ?_3: all r3127,rs3128(
;       all ss1,rs2,ss2(
;        WNs rs3128 ss1 -> WNs rs2 ss2 -> WNs(rs3128:+:rs2)(ss1:+:ss2)) -> 
;       all ss1,rs2,ss2(
;        WNs(r3127::rs3128)ss1 -> 
;        WNs rs2 ss2 -> WNs((r3127::rs3128):+:rs2)(ss1:+:ss2))) from
;   rs3122
> ; ok, we now have the new goal 
; ?_9: all ss1,rs2,ss2(
;       WNs(r1::rs1)ss1 -> WNs rs2 ss2 -> WNs((r1::rs1):+:rs2)(ss1:+:ss2)) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
> ; ok, ?_9 can be obtained from
; ?_11: all r3151,rs3152,rs2,ss2(
;        WNs(r1::rs1)(r3151::rs3152) -> 
;        WNs rs2 ss2 -> WNs((r1::rs1):+:rs2)((r3151::rs3152):+:ss2)) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146

; ?_10: all rs2,ss2(
;        WNs(r1::rs1)(Nil term) -> 
;        WNs rs2 ss2 -> WNs((r1::rs1):+:rs2)((Nil term):+:ss2)) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146
> ; ok, we now have the new goal 
; ?_12: WNs((r1::rs1):+:rs2)((Nil term):+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  rs2  ss2  2:WNs(r1::rs1)(Nil term)
;   3:WNs rs2 ss2
> ; ok, ?_12 is proved.  The active goal now is
; ?_11: all r3151,rs3152,rs2,ss2(
;        WNs(r1::rs1)(r3151::rs3152) -> 
;        WNs rs2 ss2 -> WNs((r1::rs1):+:rs2)((r3151::rs3152):+:ss2)) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146
> ; ok, we now have the new goal 
; ?_13: WNs rs2 ss2 -> WNs((r1::rs1):+:rs2)((s1::ss1):+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
> ; ok, ?_13 can be obtained from
; ?_14: all r,s,rs,ss(
;        WN r s -> 
;        WNs rs ss -> 
;        WN r s -> 
;        ((r1::rs1)=rs -> 
;         (s1::ss1)=ss -> 
;         WNs rs2 ss2 -> WNs((r1::rs1):+:rs2)((s1::ss1):+:ss2)) -> 
;        (r1::rs1)=(r::rs) -> 
;        (s1::ss1)=(s::ss) -> 
;        WNs rs2 ss2 -> WNs((r1::rs1):+:rs2)((s1::ss1):+:ss2)) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
> ; ok, we now have the new goal 
; ?_15: WN r s -> 
;       WNs rs ss -> 
;       WN r s -> 
;       ((r1::rs1)=rs -> 
;        (s1::ss1)=ss -> 
;        WNs rs2 ss2 -> WNs((r1::rs1):+:rs2)((s1::ss1):+:ss2)) -> 
;       (r1::rs1)=(r::rs) -> 
;       (s1::ss1)=(s::ss) -> 
;       WNs rs2 ss2 -> WNs((r1::rs1):+:rs2)((s1::ss1):+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss
> ; ok, we now have the new goal 
; ?_16: WNs((r1::rs1):+:rs2)((s1::ss1):+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs((r1::rs1):+:rs2)((s1::ss1):+:ss2)
;   7:(r1::rs1)=(r::rs)
;   8:(s1::ss1)=(s::ss)
;   9:WNs rs2 ss2
> ; ok, the normalized goal is
; ?_17: WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
> ; ok, ?_17 can be obtained from
; ?_19: WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
> ; ok, ?_19 can be obtained from
; ?_20: WNs(r::rs1:+:rs2)(s1::ss1:+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
> ; ok, ?_20 can be obtained from
; ?_22: WNs(r::rs1:+:rs2)(s1::ss1:+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s
> ; ok, ?_22 can be obtained from
; ?_23: WNs(r::rs1:+:rs2)(s::ss1:+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s
> ; ok, ?_23 can be obtained from
; ?_25: WNs(rs1:+:rs2)(ss1:+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s

; ?_24: WN r s from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s
> ; ok, ?_24 is proved.  The active goal now is
; ?_25: WNs(rs1:+:rs2)(ss1:+:ss2) from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s
> ; ok, ?_25 can be obtained from
; ?_27: WNs rs2 ss2 from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s

; ?_26: WNs rs1 ss1 from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s
> ; ok, ?_26 can be obtained from
; ?_29: WNs rs1 ss1 from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s
;   rs1=rs:rs1=rs
> ; ok, ?_29 can be obtained from
; ?_30: WNs rs ss1 from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s
;   rs1=rs:rs1=rs
> ; ok, ?_30 can be obtained from
; ?_32: WNs rs ss1 from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s
;   rs1=rs:rs1=rs
;   ss1=ss:ss1=ss
> ; ok, ?_32 can be obtained from
; ?_33: WNs rs ss from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s
;   rs1=rs:rs1=rs
;   ss1=ss:ss1=ss
> ; ok, ?_33 is proved.  The active goal now is
; ?_27: WNs rs2 ss2 from
;   rs3122  r1  rs1  IH:all ss1,rs2,ss2(WNs rs1 ss1 -> 
;                        WNs rs2 ss2 -> WNs(rs1:+:rs2)(ss1:+:ss2))
;   ss3146  s1  ss1  rs2  ss2  H:
;     WNs(r1::rs1)(s1::ss1)
;   r  s  rs  ss  3:WN r s
;   4:WNs rs ss
;   5:WN r s
;   6:(r1::rs1)=rs -> 
;     (s1::ss1)=ss -> WNs rs2 ss2 -> WNs(r1::rs1:+:rs2)(s1::ss1:+:ss2)
;   7:r1=r andb rs1=rs
;   8:s1=s andb ss1=ss
;   9:WNs rs2 ss2
;   r1=r:r1=r
;   s1=s:s1=s
> ; ok, ?_27 is proved.  Proof finished.
> ; ok, inductively defined predicate constant H added
> ; ?_1: all r,s(WN r s -> H r)
> ; ok, we now have the new goal 
; ?_2: WN r s -> H r from
;   r  s
> ; ok, ?_2 can be obtained from
; ?_5: all rho,r,s,t,rs(
;       WN(FoldApp(Sub r(Wrap 0 s:))rs)t -> 
;       H(FoldApp(Sub r(Wrap 0 s:))rs) -> H(FoldApp(Abs rho r)(s::rs))) from
;   r  s  1:WN r s

; ?_4: all rho,r,s(WN r s -> H r -> H(Abs rho r)) from
;   r  s  1:WN r s

; ?_3: all n,rs,ss H(FoldApp(Var n)rs) from
;   r  s  1:WN r s
> ; ok, we now have the new goal 
; ?_6: H(FoldApp(Var n)rs) from
;   r  s  1:WN r s
;   n  rs  ss
> ; ok, ?_6 is proved.  The active goal now is
; ?_4: all rho,r,s(WN r s -> H r -> H(Abs rho r)) from
;   r  s  1:WN r s
> ; ok, we now have the new goal 
; ?_7: H(Abs rho r3252) from
;   r  s  1:WN r s
;   rho  r3252  s3253  2:WN r3252 s3253
;   3:H r3252
> ; ok, ?_7 can be obtained from
; ?_8: H r3252 from
;   r  s  1:WN r s
;   rho  r3252  s3253  2:WN r3252 s3253
;   3:H r3252
> ; ok, ?_8 is proved.  The active goal now is
; ?_5: all rho,r,s,t,rs(
;       WN(FoldApp(Sub r(Wrap 0 s:))rs)t -> 
;       H(FoldApp(Sub r(Wrap 0 s:))rs) -> H(FoldApp(Abs rho r)(s::rs))) from
;   r  s  1:WN r s
> ; ok, we now have the new goal 
; ?_9: H(FoldApp(Abs rho r3256)(s3257::rs)) from
;   r  s  1:WN r s
;   rho  r3256  s3257  t  rs  2:
;     WN(FoldApp(Sub r3256(Wrap 0 s3257:))rs)t
;   3:H(FoldApp(Sub r3256(Wrap 0 s3257:))rs)
> ; ok, ?_9 can be obtained from
; ?_10: H(FoldApp(Sub r3256(Wrap 0 s3257:))rs) from
;   r  s  1:WN r s
;   rho  r3256  s3257  t  rs  2:
;     WN(FoldApp(Sub r3256(Wrap 0 s3257:))rs)t
;   3:H(FoldApp(Sub r3256(Wrap 0 s3257:))rs)
> ; ok, ?_10 is proved.  Proof finished.
> > > [r0,r1,algWN2]
 (Rec algWN=>algH)algWN2([n3,rs4,rs5]cHVar n3 rs4)
 ([rho3,r4,r5,algWN6]cHAbs rho3 r4)
 ([rho3,r4,r5,r6,rs7,algWN8]cHBeta rho3 r4 r5 rs7)
> ; ok, variable l is removed
; ok, variable rho is removed
; warning: rho was default variable of type type
; ok, variable sig is removed
; ok, variable tau is removed
; ok, variable r is removed
; warning: r was default variable of type term
; ok, variable s is removed
; ok, variable t is removed
; ok, variable rs is removed
; warning: rs was default variable of type list term
; ok, variable ss is removed
; ok, variable ts is removed
; ok, variable rhos is removed
; warning: rhos was default variable of type list type
; ok, variable sigs is removed
; ok, variable taus is removed
; ok, variable theta is removed
; warning: theta was default variable of type sub
> ; ok, algebra type removed
; ok, constructor cHBeta removed
; ok, constructor cHAbs removed
; ok, constructor TwoH removed
; ok, constructor OneH removed
; ok, constructor cWNBeta removed
; ok, constructor cWNAbs removed
; ok, constructor TwoWN removed
; ok, constructor OneWN removed
; ok, constructor Abs removed
; ok, constructor Arrow removed
; ok, constructor Iota removed
; ok, program constant IExp removed
; ok, program constant Exp removed
; ok, program constant Eta removed
; ok, program constant Cor removed
; ok, program constant Typ removed
; ok, program constant Arrowtyp removed
; ok, program constant Valtyp removed
; ok, program constant Argtyp removed
; ok, algebra sub removed
; ok, constructor Dot removed
; ok, constructor Up removed
; ok, program constant Wrap removed
; ok, program constant Sub removed
; ok, program constant Subup removed
; ok, program constant Sublist removed
; ok, program constant Mksub removed
; ok, program constant Sublift removed
> ; ok, inductively defined predicate constant H removed
> ; ok, inductively defined predicate constant WN removed
; ok, inductively defined predicate constant WNs removed
> > > > > ; ?_1: all n1 ex n2 all n3(n1=n3 -> n2=n3)
> ; ok, ?_1 can be obtained from
; ?_3: all n3317 ex n2 all n3(Succ n3317=n3 -> n2=n3) from
;   n3315

; ?_2: ex n2 all n3(0=n3 -> n2=n3) from
;   n3315
> ; ok, ?_2 can be obtained from
; ?_4: all n3(0=n3 -> 0=n3) from
;   n3315
> ; ok, we now have the new goal 
; ?_5: 0=n from
;   n3315  n  u:0=n
> ; ok, ?_5 is proved.  The active goal now is
; ?_3: all n3317 ex n2 all n3(Succ n3317=n3 -> n2=n3) from
;   n3315
> ; ok, we now have the new goal 
; ?_6: ex n2 all n3(Succ n1=n3 -> n2=n3) from
;   n3315  n1
> ; ok, we now have the new goal 
; ?_7: ex n2 all n3(Succ n1=n3 -> n2=n3) from
;   n3315  n1
> ; ok, ?_7 can be obtained from
; ?_8: all n3(Succ n1=n3 -> Succ n1=n3) from
;   n3315  n1
> ; ok, we now have the new goal 
; ?_9: Succ n1=n from
;   n3315  n1  n  u:Succ n1=n
> ; ok, ?_9 is proved.  Proof finished.
> [n3315]
 ([n3324,n3323,(nat=>nat)_3322][if n3324 n3323 (nat=>nat)_3322])n3315
 (([n2]n2)0)
 ([n1]([n2]n2)(Succ n1))

[n0]n0

[n3325]
 ([n3338]
   [if n3338
     (left(([n2]n2@([n3348]n3348))0))
     ([n3331]left(([n2]n2@([n3340]n3340))(Succ n3331)))])
 n3325

[n0]n0

> ; ?_1: all n1 ex n2 all n3(n1=n3 -> n2=n3)
> ; ok, ?_1 can be obtained from
; ?_3: all n3361(
;       ex n2 all n3(n3361=n3 -> n2=n3) -> 
;       ex n2 all n3(Succ n3361=n3 -> n2=n3)) from
;   n3359

; ?_2: ex n2 all n3(0=n3 -> n2=n3) from
;   n3359
> ; ok, ?_2 can be obtained from
; ?_4: all n3(0=n3 -> 0=n3) from
;   n3359
> ; ok, we now have the new goal 
; ?_5: 0=n from
;   n3359  n  u:0=n
> ; ok, ?_5 is proved.  The active goal now is
; ?_3: all n3361(
;       ex n2 all n3(n3361=n3 -> n2=n3) -> 
;       ex n2 all n3(Succ n3361=n3 -> n2=n3)) from
;   n3359
> ; ok, we now have the new goal 
; ?_6: ex n2 all n3(n1=n3 -> n2=n3) -> ex n2 all n3(Succ n1=n3 -> n2=n3) from
;   n3359  n1
> ; ok, we now have the new goal 
; ?_7: ex n2 all n3(Succ n1=n3 -> n2=n3) from
;   n3359  n1  1:ex n2 all n3(n1=n3 -> n2=n3)
> ; ok, ?_7 can be obtained from
; ?_8: all n3(Succ n1=n3 -> Succ n1=n3) from
;   n3359  n1  1:ex n2 all n3(n1=n3 -> n2=n3)
> ; ok, we now have the new goal 
; ?_9: Succ n1=n from
;   n3359  n1  1:ex n2 all n3(n1=n3 -> n2=n3)
;   n  u:Succ n1=n
> ; ok, ?_9 is proved.  Proof finished.
> [n3359](Rec nat=>nat)n3359(([n2]n2)0)([n1,n3368]([n2]n2)(Succ n1))

[n0]n0

[n3369]
 ([n3382]
   (Rec nat=>nat)n3382 left(([n2]n2@([n3394]n3394))0)
   ([n3375]
     left(([n3375]
            ([n3390]left(([n2]n2@([n3384]n3384))(Succ n3375)))@
            ([n3390,n3387]0))
          n3375)))
 n3369

[n0]n0

> ; ?_1: all n1 ex n2 all n3(n1=n3 -> n2=n3)
> ; ok, ?_1 can be obtained from
; ?_2: all n3407(
;       all n3408(
;        ([n]n)n3408<([n]n)n3407 -> ex n2 all n3(n3408=n3 -> n2=n3)) -> 
;       ex n2 all n3(n3407=n3 -> n2=n3)) from
;   n3405
> ; ok, we now have the new goal 
; ?_3: all n3408(([n]n)n3408<([n]n)n1 -> ex n2 all n3(n3408=n3 -> n2=n3)) -> 
;      ex n2 all n3(n1=n3 -> n2=n3) from
;   n3405  n1
> ; ok, we now have the new goal 
; ?_4: ex n2 all n3(n1=n3 -> n2=n3) from
;   n3405  n1  1:all n3408(([n]n)n3408<([n]n)n1 -> ex n2 all n3(n3408=n3 -> n2=n3))
> ; ok, ?_4 can be obtained from
; ?_5: all n3(n1=n3 -> n1=n3) from
;   n3405  n1  1:all n3408(([n]n)n3408<([n]n)n1 -> ex n2 all n3(n3408=n3 -> n2=n3))
> ; ok, we now have the new goal 
; ?_6: n1=n from
;   n3405  n1  1:all n3408(([n]n)n3408<([n]n)n1 -> ex n2 all n3(n3408=n3 -> n2=n3))
;   n  u:n1=n
> ; ok, ?_6 is proved.  Proof finished.
> [n3405](GRec nat nat)([n]n)n3405([n1,(nat=>nat)_3411]([n2]n2)n1)

[n0]n0

[n3412,n3430]
 (GRecGuard nat nat)([n]n)n3430
 ([n3430]
   left(([n3413]
          ([(nat=>nat)_3427]left(([n2]n2@([n3421]n3421))n3413))@
          ([(nat=>nat)_3427,n3424]0@0))
        n3430))
 True

[n0,n1]n1

> ; ?_1: all n1 ex n2 all n3(n1<n3 -> n2<=n3)
> ; ok, ?_1 can be obtained from
; ?_3: all n3436(
;       ex n2 all n3(n3436<n3 -> n2<=n3) -> 
;       ex n2 all n3(Succ n3436<n3 -> n2<=n3)) from
;   n3434

; ?_2: ex n2 all n3(0<n3 -> n2<=n3) from
;   n3434
> ; ok, ?_2 can be obtained from
; ?_4: all n3(0<n3 -> 1<=n3) from
;   n3434
> ; ok, ?_4 can be obtained from
; ?_6: all n3441(0<Succ n3441 -> 1<=Succ n3441) from
;   n3434  n3439

; ?_5: 0<0 -> 1<=0 from
;   n3434  n3439
> ; ok, we now have the new goal 
; ?_7: 1<=0 from
;   n3434  n3439  u:0<0
> ; ok, ?_7 is proved.  The active goal now is
; ?_6: all n3441(0<Succ n3441 -> 1<=Succ n3441) from
;   n3434  n3439
> ; ok, we now have the new goal 
; ?_8: 1<=Succ n3 from
;   n3434  n3439  n3  u:0<Succ n3
> ; ok, ?_8 is proved.  The active goal now is
; ?_3: all n3436(
;       ex n2 all n3(n3436<n3 -> n2<=n3) -> 
;       ex n2 all n3(Succ n3436<n3 -> n2<=n3)) from
;   n3434
> ; ok, we now have the new goal 
; ?_9: ex n2 all n3(Succ n1<n3 -> n2<=n3) from
;   n3434  n1  IH:ex n2 all n3(n1<n3 -> n2<=n3)
> ; ok, we now have the new goal 
; ?_12: ex n2 all n3(Succ n1<n3 -> n2<=n3) from
;   n3434  n1  n2  v:all n3(n1<n3 -> n2<=n3)
> ; ok, ?_12 can be obtained from
; ?_13: all n3(Succ n1<n3 -> Succ n2<=n3) from
;   n3434  n1  n2  v:all n3(n1<n3 -> n2<=n3)
> ; ok, ?_13 can be obtained from
; ?_15: all n3448(Succ n1<Succ n3448 -> Succ n2<=Succ n3448) from
;   n3434  n1  n2  v:all n3(n1<n3 -> n2<=n3)
;   n3446

; ?_14: Succ n1<0 -> Succ n2<=0 from
;   n3434  n1  n2  v:all n3(n1<n3 -> n2<=n3)
;   n3446
> ; ok, we now have the new goal 
; ?_16: Succ n2<=0 from
;   n3434  n1  n2  v:all n3(n1<n3 -> n2<=n3)
;   n3446  u:Succ n1<0
> ; ok, ?_16 is proved.  The active goal now is
; ?_15: all n3448(Succ n1<Succ n3448 -> Succ n2<=Succ n3448) from
;   n3434  n1  n2  v:all n3(n1<n3 -> n2<=n3)
;   n3446
> ; ok, we now have the new goal 
; ?_17: Succ n2<=Succ n3 from
;   n3434  n1  n2  v:all n3(n1<n3 -> n2<=n3)
;   n3446  n3  u:Succ n1<Succ n3
> ; ok, ?_17 can be obtained from
; ?_18: n1<n3 from
;   n3434  n1  n2  v:all n3(n1<n3 -> n2<=n3)
;   n3446  n3  u:Succ n1<Succ n3
> ; ok, ?_18 is proved.  Proof finished.
> [n3434]
 (Rec nat=>nat)n3434(([n2]n2)1)
 ([n1,n3454]
   ([n2,(nat=>nat)_3453](nat=>nat)_3453 n2)n3454([n2]([n2]n2)(Succ n2)))

[n0](Rec nat=>nat)n0 1([n1]Succ)

[n3455]
 ([n3476]
   (Rec nat=>nat)n3476 left(([n2]n2@([n3497]n3497))1)
   ([n3462]
     left(([n3462]
            ([n3492]
              left(([n3468]
                     left(([n2]n2@([n3478]n3478))(Succ n3468))@
                     ([n3488]
                       ([n3481][if n3481 0 ([n3475]n3475)])
                       (right(([n2]n2@([n3478]n3478))(Succ n3468))n3488)))
                   n3492))@
            ([n3492,n3488]
              right(([n3468]
                      left(([n2]n2@([n3478]n3478))(Succ n3468))@
                      ([n3488]
                        ([n3481][if n3481 0 ([n3475]n3475)])
                        (right(([n2]n2@([n3478]n3478))(Succ n3468))n3488)))
                    n3492)
              n3488))
          n3462)))
 n3455

[n0](Rec nat=>nat)n0 1([n1]Succ)

> ; ?_1: all n1,n2(
;       all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3)) -> 
;      all n1 ex n2 all n3(n1<n3 -> n2<=n3)
> ; ok, we now have the new goal 
; ?_2: all n1 ex n2 all n3(n1<n3 -> n2<=n3) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
> ; ok, ?_2 can be obtained from
; ?_4: all n3510(
;       ex n2 all n3(n3510<n3 -> n2<=n3) -> 
;       ex n2 all n3(Succ n3510<n3 -> n2<=n3)) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508

; ?_3: ex n2 all n3(0<n3 -> n2<=n3) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508
> ; ok, ?_3 can be obtained from
; ?_5: all n3(0<n3 -> 1<=n3) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508
> ; ok, ?_5 can be obtained from
; ?_7: all n3515(0<Succ n3515 -> 1<=Succ n3515) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508  n3513

; ?_6: 0<0 -> 1<=0 from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508  n3513
> ; ok, we now have the new goal 
; ?_8: 1<=0 from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508  n3513  u:0<0
> ; ok, ?_8 is proved.  The active goal now is
; ?_7: all n3515(0<Succ n3515 -> 1<=Succ n3515) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508  n3513
> ; ok, we now have the new goal 
; ?_9: 1<=Succ n3 from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508  n3513  n3  u:0<Succ n3
> ; ok, ?_9 is proved.  The active goal now is
; ?_4: all n3510(
;       ex n2 all n3(n3510<n3 -> n2<=n3) -> 
;       ex n2 all n3(Succ n3510<n3 -> n2<=n3)) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508
> ; ok, we now have the new goal 
; ?_10: ex n2 all n3(Succ n1<n3 -> n2<=n3) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508  n1  IH:ex n2 all n3(n1<n3 -> n2<=n3)
> ; ok, we now have the new goal 
; ?_13: ex n2 all n3(Succ n1<n3 -> n2<=n3) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508  n1  n2  v:all n3(n1<n3 -> n2<=n3)
> ; ok, ?_13 can be obtained from
; ?_14: all n3(Succ n1<n3 -> Succ n2<=n3) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508  n1  n2  v:all n3(n1<n3 -> n2<=n3)
> ; ok, ?_14 can be obtained from
; ?_15: all n3(n1<n3 -> n2<=n3) from
;   L:all n1,n2(all n3(n1<n3 -> n2<=n3) -> all n3(Succ n1<n3 -> Succ n2<=n3))
;   n3508  n1  n2  v:all n3(n1<n3 -> n2<=n3)
> ; ok, ?_15 is proved.  Proof finished.
> [n3508]
 (Rec nat=>nat)n3508(([n2]n2)1)
 ([n1,n3529]
   ([n2,(nat=>nat)_3528](nat=>nat)_3528 n2)n3529([n2]([n2]n2)(Succ n2)))

[n0](Rec nat=>nat)n0 1([n1]Succ)

([(nat=>nat=>nat=>nat)_3554,n3530]
  ([n3549]
    (Rec nat=>nat)n3549 left(([n2]n2@([n3569]n3569))1)
    ([n3537]
      left(([n3537]
             ([n3564]
               left(([n3543]
                      left(([n2]n2@([n3551]n3551))(Succ n3543))@
                      ([n3560]
                        (nat=>nat=>nat=>nat)_3554 n3537 n3543
                        (right(([n2]n2@([n3551]n3551))(Succ n3543))n3560)))
                    n3564))@
             ([n3564,n3560]
               right(([n3543]
                       left(([n2]n2@([n3551]n3551))(Succ n3543))@
                       ([n3560]
                         (nat=>nat=>nat=>nat)_3554 n3537 n3543
                         (right(([n2]n2@([n3551]n3551))(Succ n3543))n3560)))
                     n3564)
               n3560))
           n3537)))
  n3530)@
([(nat=>nat=>nat=>nat)_3554,(nat@@nat)_3581]
  ([n3549]
    (Rec nat=>nat=>nat@@nat@@nat)n3549([n3578]0@0@0)
    ([n3537,(nat=>nat@@nat@@nat)_3579,n3578]
      [let (nat@@nat@@nat)_3555
        (left(n3537@
             ([n3549]
               (Rec nat=>nat)n3549 left(([n2]n2@([n3569]n3569))1)
               ([n3537]
                 left(([n3537]
                        ([n3564]
                          left(([n3543]
                                 left(([n2]n2@([n3551]n3551))(Succ n3543))@
                                 ([n3560]
                                   (nat=>nat=>nat=>nat)_3554 n3537 n3543
                                   (right(([n2]n2@([n3551]n3551))
                                          (Succ n3543))
                                    n3560)))
                               n3564))@
                        ([n3564,n3560]
                          right(([n3543]
                                  left(([n2]n2@([n3551]n3551))(Succ n3543))@
                                  ([n3560]
                                    (nat=>nat=>nat=>nat)_3554 n3537 n3543
                                    (right(([n2]n2@([n3551]n3551))
                                           (Succ n3543))
                                     n3560)))
                                n3564)
                          n3560))
                      n3537)))
             n3537@
             n3578)@
        left(left right(n3537@
                        ([n3549]
                          (Rec nat=>nat)n3549 left(([n2]n2@([n3569]n3569))1)
                          ([n3537]
                            left(([n3537]
                                   ([n3564]
                                     left(([n3543]
                                            left(([n2]n2@([n3551]n3551))
                                                 (Succ n3543))@
                                            ([n3560]
                                              (nat=>nat=>nat=>nat)_3554 
                                              n3537 
                                              n3543
                                              (right(([n2]n2@([n3551]n3551))
                                                     (Succ n3543))
                                               n3560)))
                                          n3564))@
                                   ([n3564,n3560]
                                     right(([n3543]
                                             left(([n2]n2@([n3551]n3551))
                                                  (Succ n3543))@
                                             ([n3560]
                                               (nat=>nat=>nat=>nat)_3554 
                                               n3537 
                                               n3543
                                               (right(([n2]n2@([n3551]n3551))
                                                      (Succ n3543))
                                                n3560)))
                                           n3564)
                                     n3560))
                                 n3537)))
                        n3537@
                        n3578)@
             right right(n3537@
                         ([n3549]
                           (Rec nat=>nat)n3549 
                           left(([n2]n2@([n3569]n3569))1)
                           ([n3537]
                             left(([n3537]
                                    ([n3564]
                                      left(([n3543]
                                             left(([n2]n2@([n3551]n3551))
                                                  (Succ n3543))@
                                             ([n3560]
                                               (nat=>nat=>nat=>nat)_3554 
                                               n3537 
                                               n3543
                                               (right(([n2]n2@([n3551]n3551))
                                                      (Succ n3543))
                                                n3560)))
                                           n3564))@
                                    ([n3564,n3560]
                                      right(([n3543]
                                              left(([n2]n2@([n3551]n3551))
                                                   (Succ n3543))@
                                              ([n3560]
                                                (nat=>nat=>nat=>nat)_3554 
                                                n3537 
                                                n3543
                                                (right(([n2]
                                                         n2@([n3551]n3551))
                                                       (Succ n3543))
                                                 n3560)))
                                            n3564)
                                      n3560))
                                  n3537)))
                         n3537@
                         n3578))@
        right(([n2]n2@([n3551]n3551))
              (Succ 
               left(left right(n3537@
                               ([n3549]
                                 (Rec nat=>nat)n3549 
                                 left(([n2]n2@([n3569]n3569))1)
                                 ([n3537]
                                   left(([n3537]
                                          ([n3564]
                                            left(([n3543]
                                                   left(([n2]
                                                          n2@([n3551]n3551))
                                                        (Succ n3543))@
                                                   ([n3560]
                                                     (nat=>nat=>nat=>nat)_3554 
                                                     n3537 
                                                     n3543
                                                     (right(([n2]
                                                              n2@
                                                              ([n3551]n3551))
                                                            (Succ n3543))
                                                      n3560)))
                                                 n3564))@
                                          ([n3564,n3560]
                                            right(([n3543]
                                                    left(([n2]
                                                           n2@([n3551]n3551))
                                                         (Succ n3543))@
                                                    ([n3560]
                                                      (nat=>nat=>nat=>nat)_3554 
                                                      n3537 
                                                      n3543
                                                      (right(([n2]
                                                               n2@
                                                               ([n3551]n3551))
                                                             (Succ n3543))
                                                       n3560)))
                                                  n3564)
                                            n3560))
                                        n3537)))
                               n3537@
                               n3578)@
                    right right(n3537@
                                ([n3549]
                                  (Rec nat=>nat)n3549 
                                  left(([n2]n2@([n3569]n3569))1)
                                  ([n3537]
                                    left(([n3537]
                                           ([n3564]
                                             left(([n3543]
                                                    left(([n2]
                                                           n2@([n3551]n3551))
                                                         (Succ n3543))@
                                                    ([n3560]
                                                      (nat=>nat=>nat=>nat)_3554 
                                                      n3537 
                                                      n3543
                                                      (right(([n2]
                                                               n2@
                                                               ([n3551]n3551))
                                                             (Succ n3543))
                                                       n3560)))
                                                  n3564))@
                                           ([n3564,n3560]
                                             right(([n3543]
                                                     left(([n2]
                                                            n2@
                                                            ([n3551]n3551))
                                                          (Succ n3543))@
                                                     ([n3560]
                                                       (nat=>nat=>nat=>nat)_3554 
                                                       n3537 
                                                       n3543
                                                       (right(([n2]
                                                                n2@
                                                                ([n3551]
                                                                  n3551))
                                                              (Succ n3543))
                                                        n3560)))
                                                   n3564)
                                             n3560))
                                         n3537)))
                                n3537@
                                n3578))))
        right(left right(n3537@
                         ([n3549]
                           (Rec nat=>nat)n3549 
                           left(([n2]n2@([n3569]n3569))1)
                           ([n3537]
                             left(([n3537]
                                    ([n3564]
                                      left(([n3543]
                                             left(([n2]n2@([n3551]n3551))
                                                  (Succ n3543))@
                                             ([n3560]
                                               (nat=>nat=>nat=>nat)_3554 
                                               n3537 
                                               n3543
                                               (right(([n2]n2@([n3551]n3551))
                                                      (Succ n3543))
                                                n3560)))
                                           n3564))@
                                    ([n3564,n3560]
                                      right(([n3543]
                                              left(([n2]n2@([n3551]n3551))
                                                   (Succ n3543))@
                                              ([n3560]
                                                (nat=>nat=>nat=>nat)_3554 
                                                n3537 
                                                n3543
                                                (right(([n2]
                                                         n2@([n3551]n3551))
                                                       (Succ n3543))
                                                 n3560)))
                                            n3564)
                                      n3560))
                                  n3537)))
                         n3537@
                         n3578)@
              right right(n3537@
                          ([n3549]
                            (Rec nat=>nat)n3549 
                            left(([n2]n2@([n3569]n3569))1)
                            ([n3537]
                              left(([n3537]
                                     ([n3564]
                                       left(([n3543]
                                              left(([n2]n2@([n3551]n3551))
                                                   (Succ n3543))@
                                              ([n3560]
                                                (nat=>nat=>nat=>nat)_3554 
                                                n3537 
                                                n3543
                                                (right(([n2]
                                                         n2@([n3551]n3551))
                                                       (Succ n3543))
                                                 n3560)))
                                            n3564))@
                                     ([n3564,n3560]
                                       right(([n3543]
                                               left(([n2]n2@([n3551]n3551))
                                                    (Succ n3543))@
                                               ([n3560]
                                                 (nat=>nat=>nat=>nat)_3554 
                                                 n3537 
                                                 n3543
                                                 (right(([n2]
                                                          n2@([n3551]n3551))
                                                        (Succ n3543))
                                                  n3560)))
                                             n3564)
                                       n3560))
                                   n3537)))
                          n3537@
                          n3578)))
        [if (([(nat@@nat@@nat)_3555]
               (left(nat@@nat@@nat)_3555<
                (nat=>nat=>nat=>nat)_3554 left(nat@@nat@@nat)_3555 
                left right(nat@@nat@@nat)_3555 
                right right(nat@@nat@@nat)_3555 impb 
                left right(nat@@nat@@nat)_3555<=
                (nat=>nat=>nat=>nat)_3554 left(nat@@nat@@nat)_3555 
                left right(nat@@nat@@nat)_3555 
                right right(nat@@nat@@nat)_3555)impb 
               Succ left(nat@@nat@@nat)_3555<right right(nat@@nat@@nat)_3555 impb 
               Succ left right(nat@@nat@@nat)_3555<=
               right right(nat@@nat@@nat)_3555)
             (nat@@nat@@nat)_3555)
         ((nat=>nat@@nat@@nat)_3579
         (right(([n3537]
                  ([n3564]
                    left(([n3543]
                           left(([n2]n2@([n3551]n3551))(Succ n3543))@
                           ([n3560]
                             (nat=>nat=>nat=>nat)_3554 n3537 n3543
                             (right(([n2]n2@([n3551]n3551))(Succ n3543))
                              n3560)))
                         n3564))@
                  ([n3564,n3560]
                    right(([n3543]
                            left(([n2]n2@([n3551]n3551))(Succ n3543))@
                            ([n3560]
                              (nat=>nat=>nat=>nat)_3554 n3537 n3543
                              (right(([n2]n2@([n3551]n3551))(Succ n3543))
                               n3560)))
                          n3564)
                    n3560))
                n3537)
          (([n3549]
             (Rec nat=>nat)n3549 left(([n2]n2@([n3569]n3569))1)
             ([n3537]
               left(([n3537]
                      ([n3564]
                        left(([n3543]
                               left(([n2]n2@([n3551]n3551))(Succ n3543))@
                               ([n3560]
                                 (nat=>nat=>nat=>nat)_3554 n3537 n3543
                                 (right(([n2]n2@([n3551]n3551))(Succ n3543))
                                  n3560)))
                             n3564))@
                      ([n3564,n3560]
                        right(([n3543]
                                left(([n2]n2@([n3551]n3551))(Succ n3543))@
                                ([n3560]
                                  (nat=>nat=>nat=>nat)_3554 n3537 n3543
                                  (right(([n2]n2@([n3551]n3551))(Succ n3543))
                                   n3560)))
                              n3564)
                        n3560))
                    n3537)))
           n3537)
          n3578))
         (nat@@nat@@nat)_3555]]))
  left(nat@@nat)_3581 
  right(nat@@nat)_3581)

([(nat=>nat=>nat=>nat)_0,n1](Rec nat=>nat)n1 1([n2]Succ))@
([(nat=>nat=>nat=>nat)_0,(nat@@nat)_1]
  (Rec nat=>nat=>nat@@nat@@nat)left(nat@@nat)_1([n2]0@0@0)
  ([n2,(nat=>nat@@nat@@nat)_3,n4]
    [let (nat@@nat@@nat)_5
      (n2@(Rec nat=>nat)n2 1([n5]Succ)@n4)
      [if ((left(nat@@nat@@nat)_5<
            (nat=>nat=>nat=>nat)_0 left(nat@@nat@@nat)_5 
            left right(nat@@nat@@nat)_5 
            right right(nat@@nat@@nat)_5 impb 
            left right(nat@@nat@@nat)_5<=
            (nat=>nat=>nat=>nat)_0 left(nat@@nat@@nat)_5 
            left right(nat@@nat@@nat)_5 
            right right(nat@@nat@@nat)_5)impb 
           Succ left(nat@@nat@@nat)_5<right right(nat@@nat@@nat)_5 impb 
           Succ left right(nat@@nat@@nat)_5<=right right(nat@@nat@@nat)_5)
       ((nat=>nat@@nat@@nat)_3
       ((nat=>nat=>nat=>nat)_0 n2((Rec nat=>nat)n2 1([n6]Succ))n4))
       (nat@@nat@@nat)_5]])
  right(nat@@nat)_1)

> > minlog-load WARNING: file lib/list.scm already loaded !> > ; ok, variable ns: list nat added
> ; ?_1: all ns1 ex ns2 all ns3(ns1=ns3 -> ns2=ns3)
> ; ok, ?_1 can be obtained from
; ?_3: all n3588,ns3589(
;       ex ns2 all ns3(ns3589=ns3 -> ns2=ns3) -> 
;       ex ns2 all ns3((n3588::ns3589)=ns3 -> ns2=ns3)) from
;   ns3583

; ?_2: ex ns2 all ns3((Nil nat)=ns3 -> ns2=ns3) from
;   ns3583
> ; ok, ?_2 can be obtained from
; ?_4: all ns3((Nil nat)=ns3 -> (Nil nat)=ns3) from
;   ns3583
> ; ok, we now have the new goal 
; ?_5: (Nil nat)=ns from
;   ns3583  ns  u:(Nil nat)=ns
> ; ok, ?_5 is proved.  The active goal now is
; ?_3: all n3588,ns3589(
;       ex ns2 all ns3(ns3589=ns3 -> ns2=ns3) -> 
;       ex ns2 all ns3((n3588::ns3589)=ns3 -> ns2=ns3)) from
;   ns3583
> ; ok, we now have the new goal 
; ?_6: ex ns2 all ns3(ns1=ns3 -> ns2=ns3) -> 
;      ex ns2 all ns3((n::ns1)=ns3 -> ns2=ns3) from
;   ns3583  n  ns1
> ; ok, we now have the new goal 
; ?_7: ex ns2 all ns3((n::ns1)=ns3 -> ns2=ns3) from
;   ns3583  n  ns1  1:ex ns2 all ns3(ns1=ns3 -> ns2=ns3)
> ; ok, ?_7 can be obtained from
; ?_8: all ns3((n::ns1)=ns3 -> (n::ns1)=ns3) from
;   ns3583  n  ns1  1:ex ns2 all ns3(ns1=ns3 -> ns2=ns3)
> ; ok, we now have the new goal 
; ?_9: (n::ns1)=ns from
;   ns3583  n  ns1  1:ex ns2 all ns3(ns1=ns3 -> ns2=ns3)
;   ns  u:(n::ns1)=ns
> ; ok, ?_9 is proved.  Proof finished.
> [ns3583]
 (Rec list nat=>list nat)ns3583(([ns2]ns2)(Nil nat))
 ([n,ns1,ns3597]([ns2]ns2)(n::ns1))

[ns0]ns0

[ns3598]
 ([ns3624]
   (Rec list nat=>list nat)ns3624 left(([ns2]ns2@([ns3638]ns3638))(Nil nat))
   ([n3616,ns3617]
     left(([n3616,ns3617]
            ([ns3633]left(([ns2]ns2@([ns3626]ns3626))(n3616::ns3617)))@
            ([ns3633,ns3630](Nil nat)))
          n3616 
          ns3617)))
 ns3598

[ns0]ns0

> ; ?_1: all ns1 ex ns2 all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
> ; ok, ?_1 can be obtained from
; ?_3: all n3660,ns3661(
;       ex ns2 all ns3(Lh ns3661<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;       ex ns2 all ns3(Lh(n3660::ns3661)<Lh ns3 -> Lh ns2<=Lh ns3)) from
;   ns3655

; ?_2: ex ns2 all ns3(Lh(Nil nat)<Lh ns3 -> Lh ns2<=Lh ns3) from
;   ns3655
> ; ok, ?_2 can be obtained from
; ?_4: all ns3(Lh(Nil nat)<Lh ns3 -> Lh 0: <=Lh ns3) from
;   ns3655
> ; ok, ?_4 can be obtained from
; ?_6: all n3669,ns3670(
;       Lh(Nil nat)<Lh(n3669::ns3670) -> Lh 0: <=Lh(n3669::ns3670)) from
;   ns3655  ns3664

; ?_5: Lh(Nil nat)<Lh(Nil nat) -> Lh 0: <=Lh(Nil nat) from
;   ns3655  ns3664
> ; ok, we now have the new goal 
; ?_7: Lh 0: <=Lh(Nil nat) from
;   ns3655  ns3664  u:Lh(Nil nat)<Lh(Nil nat)
> ; ok, ?_7 is proved.  The active goal now is
; ?_6: all n3669,ns3670(
;       Lh(Nil nat)<Lh(n3669::ns3670) -> Lh 0: <=Lh(n3669::ns3670)) from
;   ns3655  ns3664
> ; ok, we now have the new goal 
; ?_8: Lh 0: <=Lh(n3::ns3) from
;   ns3655  ns3664  n3  ns3  u:
;     Lh(Nil nat)<Lh(n3::ns3)
> ; ok, ?_8 is proved.  The active goal now is
; ?_3: all n3660,ns3661(
;       ex ns2 all ns3(Lh ns3661<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;       ex ns2 all ns3(Lh(n3660::ns3661)<Lh ns3 -> Lh ns2<=Lh ns3)) from
;   ns3655
> ; ok, we now have the new goal 
; ?_9: ex ns2 all ns3(Lh(n1::ns1)<Lh ns3 -> Lh ns2<=Lh ns3) from
;   ns3655  n1  ns1  IH:ex ns2 all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
> ; ok, we now have the new goal 
; ?_12: ex ns2 all ns3(Lh(n1::ns1)<Lh ns3 -> Lh ns2<=Lh ns3) from
;   ns3655  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
> ; ok, ?_12 can be obtained from
; ?_13: all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3) from
;   ns3655  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
> ; ok, ?_13 can be obtained from
; ?_15: all n3680,ns3681(
;        Lh(n1::ns1)<Lh(n3680::ns3681) -> Lh(0::ns2)<=Lh(n3680::ns3681)) from
;   ns3655  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
;   ns3675

; ?_14: Lh(n1::ns1)<Lh(Nil nat) -> Lh(0::ns2)<=Lh(Nil nat) from
;   ns3655  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
;   ns3675
> ; ok, we now have the new goal 
; ?_16: Lh(0::ns2)<=Lh(Nil nat) from
;   ns3655  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
;   ns3675  u:Lh(n1::ns1)<Lh(Nil nat)
> ; ok, ?_16 is proved.  The active goal now is
; ?_15: all n3680,ns3681(
;        Lh(n1::ns1)<Lh(n3680::ns3681) -> Lh(0::ns2)<=Lh(n3680::ns3681)) from
;   ns3655  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
;   ns3675
> ; ok, we now have the new goal 
; ?_17: Lh(0::ns2)<=Lh(n3::ns3) from
;   ns3655  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
;   ns3675  n3  ns3  u:Lh(n1::ns1)<Lh(n3::ns3)
> ; ok, ?_17 can be obtained from
; ?_18: Lh ns1<Lh ns3 from
;   ns3655  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
;   ns3675  n3  ns3  u:Lh(n1::ns1)<Lh(n3::ns3)
> ; ok, ?_18 is proved.  Proof finished.
> [ns3655]
 (Rec list nat=>list nat)ns3655(([ns2]ns2)0:)
 ([n1,ns1,ns3688]
   ([ns2,(list nat=>list nat)_3687](list nat=>list nat)_3687 ns2)ns3688
   ([ns2]([ns2]ns2)(0::ns2)))

[ns0](Rec list nat=>list nat)ns0 0:([n1,ns2](Cons nat)0)

[ns3689]
 ([ns3752]
   (Rec list nat=>list nat)ns3752 left(([ns2]ns2@([ns3778]ns3778))0:)
   ([n3721,ns3722]
     left(([n3721,ns3722]
            ([ns3772]
              left(([ns3728]
                     left(([ns2]ns2@([ns3754]ns3754))(0::ns3728))@
                     ([ns3768]
                       ([ns3758]
                         [if ns3758
                           (Nil nat)
                           ([n3750,ns3751]right(n3750@ns3751))])
                       (right(([ns2]ns2@([ns3754]ns3754))(0::ns3728))ns3768)))
                   ns3772))@
            ([ns3772,ns3768]
              right(([ns3728]
                      left(([ns2]ns2@([ns3754]ns3754))(0::ns3728))@
                      ([ns3768]
                        ([ns3758]
                          [if ns3758
                            (Nil nat)
                            ([n3750,ns3751]right(n3750@ns3751))])
                        (right(([ns2]ns2@([ns3754]ns3754))(0::ns3728))ns3768)))
                    ns3772)
              ns3768))
          n3721 
          ns3722)))
 ns3689

[ns0](Rec list nat=>list nat)ns0 0:([n1,ns2](Cons nat)0)

> ; ?_1: all ns1,n1,ns2(
;       all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;       all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3)) -> 
;      all ns1 ex ns2 all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
> ; ok, we now have the new goal 
; ?_2: all ns1 ex ns2 all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
> ; ok, ?_2 can be obtained from
; ?_4: all n3796,ns3797(
;       ex ns2 all ns3(Lh ns3797<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;       ex ns2 all ns3(Lh(n3796::ns3797)<Lh ns3 -> Lh ns2<=Lh ns3)) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791

; ?_3: ex ns2 all ns3(Lh(Nil nat)<Lh ns3 -> Lh ns2<=Lh ns3) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791
> ; ok, ?_3 can be obtained from
; ?_5: all ns3(Lh(Nil nat)<Lh ns3 -> Lh 0: <=Lh ns3) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791
> ; ok, ?_5 can be obtained from
; ?_7: all n3805,ns3806(
;       Lh(Nil nat)<Lh(n3805::ns3806) -> Lh 0: <=Lh(n3805::ns3806)) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791  ns3800

; ?_6: Lh(Nil nat)<Lh(Nil nat) -> Lh 0: <=Lh(Nil nat) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791  ns3800
> ; ok, we now have the new goal 
; ?_8: Lh 0: <=Lh(Nil nat) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791  ns3800  u:Lh(Nil nat)<Lh(Nil nat)
> ; ok, ?_8 is proved.  The active goal now is
; ?_7: all n3805,ns3806(
;       Lh(Nil nat)<Lh(n3805::ns3806) -> Lh 0: <=Lh(n3805::ns3806)) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791  ns3800
> ; ok, we now have the new goal 
; ?_9: Lh 0: <=Lh(n3::ns3) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791  ns3800  n3  ns3  u:
;     Lh(Nil nat)<Lh(n3::ns3)
> ; ok, ?_9 is proved.  The active goal now is
; ?_4: all n3796,ns3797(
;       ex ns2 all ns3(Lh ns3797<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;       ex ns2 all ns3(Lh(n3796::ns3797)<Lh ns3 -> Lh ns2<=Lh ns3)) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791
> ; ok, we now have the new goal 
; ?_10: ex ns2 all ns3(Lh(n1::ns1)<Lh ns3 -> Lh ns2<=Lh ns3) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791  n1  ns1  IH:ex ns2 all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
> ; ok, we now have the new goal 
; ?_13: ex ns2 all ns3(Lh(n1::ns1)<Lh ns3 -> Lh ns2<=Lh ns3) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
> ; ok, ?_13 can be obtained from
; ?_14: all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(n1::ns2)<=Lh ns3) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
> ; ok, ?_14 can be obtained from
; ?_15: all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) from
;   L:all ns1,n1,ns2(
;      all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3) -> 
;      all ns3(Lh(n1::ns1)<Lh ns3 -> Lh(0::ns2)<=Lh ns3))
;   ns3791  n1  ns1  ns2  v:
;     all ns3(Lh ns1<Lh ns3 -> Lh ns2<=Lh ns3)
> ; ok, ?_15 is proved.  Proof finished.
> [ns3791]
 (Rec list nat=>list nat)ns3791(([ns2]ns2)0:)
 ([n1,ns1,ns3831]
   ([ns2,(list nat=>list nat)_3830](list nat=>list nat)_3830 ns2)ns3831
   ([ns2]([ns2]ns2)(n1::ns2)))

[ns0](Rec list nat=>list nat)ns0 0:([n1,ns2](Cons nat)n1)

([(list nat=>nat=>list nat=>list nat=>list nat)_3883,ns3832]
  ([ns3877]
    (Rec list nat=>list nat)ns3877 left(([ns2]ns2@([ns3900]ns3900))0:)
    ([n3864,ns3865]
      left(([n3864,ns3865]
             ([ns3894]
               left(([ns3871]
                      left(([ns2]ns2@([ns3879]ns3879))(n3864::ns3871))@
                      ([ns3890]
                        (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                        ns3865 
                        n3864 
                        ns3871
                        (right(([ns2]ns2@([ns3879]ns3879))(n3864::ns3871))
                         ns3890)))
                    ns3894))@
             ([ns3894,ns3890]
               right(([ns3871]
                       left(([ns2]ns2@([ns3879]ns3879))(n3864::ns3871))@
                       ([ns3890]
                         (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                         ns3865 
                         n3864 
                         ns3871
                         (right(([ns2]ns2@([ns3879]ns3879))(n3864::ns3871))
                          ns3890)))
                     ns3894)
               ns3890))
           n3864 
           ns3865)))
  ns3832)@
([(list nat=>nat=>list nat=>list nat=>list nat)_3883,(list nat@@list nat)_3915]
  ([ns3877]
    (Rec list nat=>list nat=>list nat@@nat@@list nat@@list nat)ns3877
    ([ns3911](Nil nat)@0@(Nil nat)@(Nil nat))
    ([n3864,ns3865,(list nat=>list nat@@nat@@list nat@@list nat)_3912,ns3911]
      [let (list nat@@nat@@list nat@@list nat)_3884
        (left right(n3864@
                   ns3865@
                   ([ns3877]
                     (Rec list nat=>list nat)ns3877 
                     left(([ns2]ns2@([ns3900]ns3900))0:)
                     ([n3864,ns3865]
                       left(([n3864,ns3865]
                              ([ns3894]
                                left(([ns3871]
                                       left(([ns2]ns2@([ns3879]ns3879))
                                            (n3864::ns3871))@
                                       ([ns3890]
                                         (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                         ns3865 
                                         n3864 
                                         ns3871
                                         (right(([ns2]ns2@([ns3879]ns3879))
                                                (n3864::ns3871))
                                          ns3890)))
                                     ns3894))@
                              ([ns3894,ns3890]
                                right(([ns3871]
                                        left(([ns2]ns2@([ns3879]ns3879))
                                             (n3864::ns3871))@
                                        ([ns3890]
                                          (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                          ns3865 
                                          n3864 
                                          ns3871
                                          (right(([ns2]ns2@([ns3879]ns3879))
                                                 (n3864::ns3871))
                                           ns3890)))
                                      ns3894)
                                ns3890))
                            n3864 
                            ns3865)))
                   ns3865@
                   ns3911)@
        left(n3864@
             ns3865@
             ([ns3877]
               (Rec list nat=>list nat)ns3877 
               left(([ns2]ns2@([ns3900]ns3900))0:)
               ([n3864,ns3865]
                 left(([n3864,ns3865]
                        ([ns3894]
                          left(([ns3871]
                                 left(([ns2]ns2@([ns3879]ns3879))
                                      (n3864::ns3871))@
                                 ([ns3890]
                                   (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                   ns3865 
                                   n3864 
                                   ns3871
                                   (right(([ns2]ns2@([ns3879]ns3879))
                                          (n3864::ns3871))
                                    ns3890)))
                               ns3894))@
                        ([ns3894,ns3890]
                          right(([ns3871]
                                  left(([ns2]ns2@([ns3879]ns3879))
                                       (n3864::ns3871))@
                                  ([ns3890]
                                    (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                    ns3865 
                                    n3864 
                                    ns3871
                                    (right(([ns2]ns2@([ns3879]ns3879))
                                           (n3864::ns3871))
                                     ns3890)))
                                ns3894)
                          ns3890))
                      n3864 
                      ns3865)))
             ns3865@
             ns3911)@
        left(left right right(n3864@
                              ns3865@
                              ([ns3877]
                                (Rec list nat=>list nat)ns3877 
                                left(([ns2]ns2@([ns3900]ns3900))0:)
                                ([n3864,ns3865]
                                  left(([n3864,ns3865]
                                         ([ns3894]
                                           left(([ns3871]
                                                  left(([ns2]
                                                         ns2@
                                                         ([ns3879]ns3879))
                                                       (n3864::ns3871))@
                                                  ([ns3890]
                                                    (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                    ns3865 
                                                    n3864 
                                                    ns3871
                                                    (right(([ns2]
                                                             ns2@
                                                             ([ns3879]ns3879))
                                                           (n3864::ns3871))
                                                     ns3890)))
                                                ns3894))@
                                         ([ns3894,ns3890]
                                           right(([ns3871]
                                                   left(([ns2]
                                                          ns2@
                                                          ([ns3879]ns3879))
                                                        (n3864::ns3871))@
                                                   ([ns3890]
                                                     (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                     ns3865 
                                                     n3864 
                                                     ns3871
                                                     (right(([ns2]
                                                              ns2@
                                                              ([ns3879]
                                                                ns3879))
                                                            (n3864::ns3871))
                                                      ns3890)))
                                                 ns3894)
                                           ns3890))
                                       n3864 
                                       ns3865)))
                              ns3865@
                              ns3911)@
             right right right(n3864@
                               ns3865@
                               ([ns3877]
                                 (Rec list nat=>list nat)ns3877 
                                 left(([ns2]ns2@([ns3900]ns3900))0:)
                                 ([n3864,ns3865]
                                   left(([n3864,ns3865]
                                          ([ns3894]
                                            left(([ns3871]
                                                   left(([ns2]
                                                          ns2@
                                                          ([ns3879]ns3879))
                                                        (n3864::ns3871))@
                                                   ([ns3890]
                                                     (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                     ns3865 
                                                     n3864 
                                                     ns3871
                                                     (right(([ns2]
                                                              ns2@
                                                              ([ns3879]
                                                                ns3879))
                                                            (n3864::ns3871))
                                                      ns3890)))
                                                 ns3894))@
                                          ([ns3894,ns3890]
                                            right(([ns3871]
                                                    left(([ns2]
                                                           ns2@
                                                           ([ns3879]ns3879))
                                                         (n3864::ns3871))@
                                                    ([ns3890]
                                                      (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                      ns3865 
                                                      n3864 
                                                      ns3871
                                                      (right(([ns2]
                                                               ns2@
                                                               ([ns3879]
                                                                 ns3879))
                                                             (n3864::ns3871))
                                                       ns3890)))
                                                  ns3894)
                                            ns3890))
                                        n3864 
                                        ns3865)))
                               ns3865@
                               ns3911))@
        right(([ns2]ns2@([ns3879]ns3879))
              (left(n3864@
                    ns3865@
                    ([ns3877]
                      (Rec list nat=>list nat)ns3877 
                      left(([ns2]ns2@([ns3900]ns3900))0:)
                      ([n3864,ns3865]
                        left(([n3864,ns3865]
                               ([ns3894]
                                 left(([ns3871]
                                        left(([ns2]ns2@([ns3879]ns3879))
                                             (n3864::ns3871))@
                                        ([ns3890]
                                          (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                          ns3865 
                                          n3864 
                                          ns3871
                                          (right(([ns2]ns2@([ns3879]ns3879))
                                                 (n3864::ns3871))
                                           ns3890)))
                                      ns3894))@
                               ([ns3894,ns3890]
                                 right(([ns3871]
                                         left(([ns2]ns2@([ns3879]ns3879))
                                              (n3864::ns3871))@
                                         ([ns3890]
                                           (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                           ns3865 
                                           n3864 
                                           ns3871
                                           (right(([ns2]ns2@([ns3879]ns3879))
                                                  (n3864::ns3871))
                                            ns3890)))
                                       ns3894)
                                 ns3890))
                             n3864 
                             ns3865)))
                    ns3865@
                    ns3911)::
               left(left right right(n3864@
                                     ns3865@
                                     ([ns3877]
                                       (Rec list nat=>list nat)ns3877 
                                       left(([ns2]ns2@([ns3900]ns3900))0:)
                                       ([n3864,ns3865]
                                         left(([n3864,ns3865]
                                                ([ns3894]
                                                  left(([ns3871]
                                                         left(([ns2]
                                                                ns2@
                                                                ([ns3879]
                                                                  ns3879))
                                                              (n3864::ns3871))@
                                                         ([ns3890]
                                                           (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                           ns3865 
                                                           n3864 
                                                           ns3871
                                                           (right(([ns2]
                                                                    ns2@
                                                                    ([ns3879]
                                                                      ns3879))
                                                                  (n3864::
                                                                   ns3871))
                                                            ns3890)))
                                                       ns3894))@
                                                ([ns3894,ns3890]
                                                  right(([ns3871]
                                                          left(([ns2]
                                                                 ns2@
                                                                 ([ns3879]
                                                                   ns3879))
                                                               (n3864::
                                                                ns3871))@
                                                          ([ns3890]
                                                            (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                            ns3865 
                                                            n3864 
                                                            ns3871
                                                            (right(([ns2]
                                                                     ns2@
                                                                     ([ns3879]
                                                                       ns3879))
                                                                   (n3864::
                                                                    ns3871))
                                                             ns3890)))
                                                        ns3894)
                                                  ns3890))
                                              n3864 
                                              ns3865)))
                                     ns3865@
                                     ns3911)@
                    right right right(n3864@
                                      ns3865@
                                      ([ns3877]
                                        (Rec list nat=>list nat)ns3877 
                                        left(([ns2]ns2@([ns3900]ns3900))0:)
                                        ([n3864,ns3865]
                                          left(([n3864,ns3865]
                                                 ([ns3894]
                                                   left(([ns3871]
                                                          left(([ns2]
                                                                 ns2@
                                                                 ([ns3879]
                                                                   ns3879))
                                                               (n3864::
                                                                ns3871))@
                                                          ([ns3890]
                                                            (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                            ns3865 
                                                            n3864 
                                                            ns3871
                                                            (right(([ns2]
                                                                     ns2@
                                                                     ([ns3879]
                                                                       ns3879))
                                                                   (n3864::
                                                                    ns3871))
                                                             ns3890)))
                                                        ns3894))@
                                                 ([ns3894,ns3890]
                                                   right(([ns3871]
                                                           left(([ns2]
                                                                  ns2@
                                                                  ([ns3879]
                                                                    ns3879))
                                                                (n3864::
                                                                 ns3871))@
                                                           ([ns3890]
                                                             (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                             ns3865 
                                                             n3864 
                                                             ns3871
                                                             (right(([ns2]
                                                                      ns2@
                                                                      ([ns3879]
                                                                        ns3879))
                                                                    (n3864::
                                                                     ns3871))
                                                              ns3890)))
                                                         ns3894)
                                                   ns3890))
                                               n3864 
                                               ns3865)))
                                      ns3865@
                                      ns3911))))
        right(left right right(n3864@
                               ns3865@
                               ([ns3877]
                                 (Rec list nat=>list nat)ns3877 
                                 left(([ns2]ns2@([ns3900]ns3900))0:)
                                 ([n3864,ns3865]
                                   left(([n3864,ns3865]
                                          ([ns3894]
                                            left(([ns3871]
                                                   left(([ns2]
                                                          ns2@
                                                          ([ns3879]ns3879))
                                                        (n3864::ns3871))@
                                                   ([ns3890]
                                                     (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                     ns3865 
                                                     n3864 
                                                     ns3871
                                                     (right(([ns2]
                                                              ns2@
                                                              ([ns3879]
                                                                ns3879))
                                                            (n3864::ns3871))
                                                      ns3890)))
                                                 ns3894))@
                                          ([ns3894,ns3890]
                                            right(([ns3871]
                                                    left(([ns2]
                                                           ns2@
                                                           ([ns3879]ns3879))
                                                         (n3864::ns3871))@
                                                    ([ns3890]
                                                      (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                      ns3865 
                                                      n3864 
                                                      ns3871
                                                      (right(([ns2]
                                                               ns2@
                                                               ([ns3879]
                                                                 ns3879))
                                                             (n3864::ns3871))
                                                       ns3890)))
                                                  ns3894)
                                            ns3890))
                                        n3864 
                                        ns3865)))
                               ns3865@
                               ns3911)@
              right right right(n3864@
                                ns3865@
                                ([ns3877]
                                  (Rec list nat=>list nat)ns3877 
                                  left(([ns2]ns2@([ns3900]ns3900))0:)
                                  ([n3864,ns3865]
                                    left(([n3864,ns3865]
                                           ([ns3894]
                                             left(([ns3871]
                                                    left(([ns2]
                                                           ns2@
                                                           ([ns3879]ns3879))
                                                         (n3864::ns3871))@
                                                    ([ns3890]
                                                      (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                      ns3865 
                                                      n3864 
                                                      ns3871
                                                      (right(([ns2]
                                                               ns2@
                                                               ([ns3879]
                                                                 ns3879))
                                                             (n3864::ns3871))
                                                       ns3890)))
                                                  ns3894))@
                                           ([ns3894,ns3890]
                                             right(([ns3871]
                                                     left(([ns2]
                                                            ns2@
                                                            ([ns3879]ns3879))
                                                          (n3864::ns3871))@
                                                     ([ns3890]
                                                       (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                                       ns3865 
                                                       n3864 
                                                       ns3871
                                                       (right(([ns2]
                                                                ns2@
                                                                ([ns3879]
                                                                  ns3879))
                                                              (n3864::ns3871))
                                                        ns3890)))
                                                   ns3894)
                                             ns3890))
                                         n3864 
                                         ns3865)))
                                ns3865@
                                ns3911)))
        [if (([(list nat@@nat@@list nat@@list nat)_3884]
               (Lh left(list nat@@nat@@list nat@@list nat)_3884<
                Lh((list nat=>nat=>list nat=>list nat=>list nat)_3883 
                   left(list nat@@nat@@list nat@@list nat)_3884 
                   left right(list nat@@nat@@list nat@@list nat)_3884 
                   left right right(list nat@@nat@@list nat@@list nat)_3884 
                   right right right(list nat@@nat@@list nat@@list nat)_3884)impb 
                Lh left right right(list nat@@nat@@list nat@@list nat)_3884<=
                Lh((list nat=>nat=>list nat=>list nat=>list nat)_3883 
                   left(list nat@@nat@@list nat@@list nat)_3884 
                   left right(list nat@@nat@@list nat@@list nat)_3884 
                   left right right(list nat@@nat@@list nat@@list nat)_3884 
                   right right right(list nat@@nat@@list nat@@list nat)_3884))impb 
               Lh(left right(list nat@@nat@@list nat@@list nat)_3884::
                  left(list nat@@nat@@list nat@@list nat)_3884)<
               Lh right right right(list nat@@nat@@list nat@@list nat)_3884 impb 
               Lh(0::
                  left right right(list nat@@nat@@list nat@@list nat)_3884)<=
               Lh right right right(list nat@@nat@@list nat@@list nat)_3884)
             (list nat@@nat@@list nat@@list nat)_3884)
         ((list nat=>list nat@@nat@@list nat@@list nat)_3912
         (right(([n3864,ns3865]
                  ([ns3894]
                    left(([ns3871]
                           left(([ns2]ns2@([ns3879]ns3879))(n3864::ns3871))@
                           ([ns3890]
                             (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                             ns3865 
                             n3864 
                             ns3871
                             (right(([ns2]ns2@([ns3879]ns3879))
                                    (n3864::ns3871))
                              ns3890)))
                         ns3894))@
                  ([ns3894,ns3890]
                    right(([ns3871]
                            left(([ns2]ns2@([ns3879]ns3879))(n3864::ns3871))@
                            ([ns3890]
                              (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                              ns3865 
                              n3864 
                              ns3871
                              (right(([ns2]ns2@([ns3879]ns3879))
                                     (n3864::ns3871))
                               ns3890)))
                          ns3894)
                    ns3890))
                n3864 
                ns3865)
          (([ns3877]
             (Rec list nat=>list nat)ns3877 
             left(([ns2]ns2@([ns3900]ns3900))0:)
             ([n3864,ns3865]
               left(([n3864,ns3865]
                      ([ns3894]
                        left(([ns3871]
                               left(([ns2]ns2@([ns3879]ns3879))
                                    (n3864::ns3871))@
                               ([ns3890]
                                 (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                 ns3865 
                                 n3864 
                                 ns3871
                                 (right(([ns2]ns2@([ns3879]ns3879))
                                        (n3864::ns3871))
                                  ns3890)))
                             ns3894))@
                      ([ns3894,ns3890]
                        right(([ns3871]
                                left(([ns2]ns2@([ns3879]ns3879))
                                     (n3864::ns3871))@
                                ([ns3890]
                                  (list nat=>nat=>list nat=>list nat=>list nat)_3883 
                                  ns3865 
                                  n3864 
                                  ns3871
                                  (right(([ns2]ns2@([ns3879]ns3879))
                                         (n3864::ns3871))
                                   ns3890)))
                              ns3894)
                        ns3890))
                    n3864 
                    ns3865)))
           ns3865)
          ns3911))
         (list nat@@nat@@list nat@@list nat)_3884]]))
  left(list nat@@list nat)_3915 
  right(list nat@@list nat)_3915)

([(list nat=>nat=>list nat=>list nat=>list nat)_0,ns1]
  (Rec list nat=>list nat)ns1 0:([n2,ns3](Cons nat)n2))@
([(list nat=>nat=>list nat=>list nat=>list nat)_0,(list nat@@list nat)_1]
  (Rec list nat=>list nat=>list nat@@nat@@list nat@@list nat)
  left(list nat@@list nat)_1
  ([ns2](Nil nat)@0@(Nil nat)@(Nil nat))
  ([n2,ns3,(list nat=>list nat@@nat@@list nat@@list nat)_4,ns5]
    [let (list nat@@nat@@list nat@@list nat)_6
      (ns3@n2@(Rec list nat=>list nat)ns3 0:([n6,ns7](Cons nat)n6)@ns5)
      [if ((Lh left(list nat@@nat@@list nat@@list nat)_6<
            Lh((list nat=>nat=>list nat=>list nat=>list nat)_0 
               left(list nat@@nat@@list nat@@list nat)_6 
               left right(list nat@@nat@@list nat@@list nat)_6 
               left right right(list nat@@nat@@list nat@@list nat)_6 
               right right right(list nat@@nat@@list nat@@list nat)_6)impb 
            Lh left right right(list nat@@nat@@list nat@@list nat)_6<=
            Lh((list nat=>nat=>list nat=>list nat=>list nat)_0 
               left(list nat@@nat@@list nat@@list nat)_6 
               left right(list nat@@nat@@list nat@@list nat)_6 
               left right right(list nat@@nat@@list nat@@list nat)_6 
               right right right(list nat@@nat@@list nat@@list nat)_6))impb 
           Succ Lh left(list nat@@nat@@list nat@@list nat)_6<
           Lh right right right(list nat@@nat@@list nat@@list nat)_6 impb 
           Succ Lh left right right(list nat@@nat@@list nat@@list nat)_6<=
           Lh right right right(list nat@@nat@@list nat@@list nat)_6)
       ((list nat=>list nat@@nat@@list nat@@list nat)_4
       ((list nat=>nat=>list nat=>list nat=>list nat)_0 ns3 n2
        ((Rec list nat=>list nat)ns3 0:([n7,ns8](Cons nat)n7))
        ns5))
       (list nat@@nat@@list nat@@list nat)_6]])
  right(list nat@@list nat)_1)

> ; ok, predicate variable R: (arity nat nat) added
> ; ?_1: R 0 1 -> all n1 ex n2 R(Succ n1)(Succ n2) -> all n1 ex n2 R n1 n2
> ; ok, we now have the new goal 
; ?_2: all n1 ex n2 R n1 n2 from
;   Base:R 0 1
;   Step:all n1 ex n2 R(Succ n1)(Succ n2)
> ; ok, ?_2 can be obtained from
; ?_4: all n3919 ex n2 R(Succ n3919)n2 from
;   Base:R 0 1
;   Step:all n1 ex n2 R(Succ n1)(Succ n2)
;   n3917

; ?_3: ex n2 R 0 n2 from
;   Base:R 0 1
;   Step:all n1 ex n2 R(Succ n1)(Succ n2)
;   n3917
> ; ok, ?_3 can be obtained from
; ?_5: R 0 1 from
;   Base:R 0 1
;   Step:all n1 ex n2 R(Succ n1)(Succ n2)
;   n3917
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all n3919 ex n2 R(Succ n3919)n2 from
;   Base:R 0 1
;   Step:all n1 ex n2 R(Succ n1)(Succ n2)
;   n3917
> ; ok, we now have the new goal 
; ?_6: ex n2 R(Succ n1)n2 from
;   Base:R 0 1
;   Step:all n1 ex n2 R(Succ n1)(Succ n2)
;   n3917  n1
> ; ok, ?_6 can be obtained from
; ?_8: ex n2 R(Succ n1)n2 from
;   Base:R 0 1
;   Step:all n1 ex n2 R(Succ n1)(Succ n2)
;   n3917  n1  Step1:ex n2 R(Succ n1)(Succ n2)
> ; ok, we now have the new goal 
; ?_11: ex n2 R(Succ n1)n2 from
;   Base:R 0 1
;   Step:all n1 ex n2 R(Succ n1)(Succ n2)
;   n3917  n1  n2  Step2:R(Succ n1)(Succ n2)
> ; ok, ?_11 can be obtained from
; ?_12: R(Succ n1)(Succ n2) from
;   Base:R 0 1
;   Step:all n1 ex n2 R(Succ n1)(Succ n2)
;   n3917  n1  n2  Step2:R(Succ n1)(Succ n2)
> ; ok, ?_12 is proved.  Proof finished.
> [alpha198_3930,(nat=>nat@@alpha198)_3936,n3917]
 ([n3928,(nat@@alpha198)_3927,(nat=>nat@@alpha198)_3926]
   [if n3928 (nat@@alpha198)_3927 (nat=>nat@@alpha198)_3926])
 n3917
 (([n2,alpha198_3929]n2@alpha198_3929)1 alpha198_3930)
 ([n1]
   ([(nat@@alpha198)_3933]
     ([(nat@@alpha198)_3932,(nat=>alpha198=>nat@@alpha198)_3931]
       (nat=>alpha198=>nat@@alpha198)_3931 left(nat@@alpha198)_3932 
       right(nat@@alpha198)_3932)
     (nat@@alpha198)_3933
     ([n2,alpha198_3935]
       ([n2,alpha198_3934]n2@alpha198_3934)(Succ n2)alpha198_3935))
   ((nat=>nat@@alpha198)_3936 n1))

[alpha198_0,(nat=>nat@@alpha198)_1,n2]
 [if n2
   (1@alpha198_0)
   ([n3]Succ left((nat=>nat@@alpha198)_1 n3)@right((nat=>nat@@alpha198)_1 n3))]

([alpha200_3976]
  ([(nat=>nat@@alpha200)_3969,n3938]
    ([n3955]
      [if n3955
        (left(([n2]
               ([alpha200_3973]n2@alpha200_3973)@
               ([alpha200_3973,alpha201_3974]alpha201_3974))
             1)
        alpha200_3976)
        ([n3943]
         left(([(nat@@alpha200)_3966]
                left(([n3949]
                       ([alpha200_3961]
                         left(([n2]
                                ([alpha200_3957]n2@alpha200_3957)@
                                ([alpha200_3957,alpha201_3958]alpha201_3958))
                              (Succ n3949))
                         alpha200_3961)@
                       ([alpha200_3961,alpha201_3963]
                         right(([n2]
                                 ([alpha200_3957]n2@alpha200_3957)@
                                 ([alpha200_3957,alpha201_3958]alpha201_3958))
                               (Succ n3949))
                         alpha200_3961 
                         alpha201_3963))
                     left(nat@@alpha200)_3966)
                right(nat@@alpha200)_3966)@
              ([(nat@@alpha200)_3966,alpha201_3963]
                right(([n3949]
                        ([alpha200_3961]
                          left(([n2]
                                 ([alpha200_3957]n2@alpha200_3957)@
                                 ([alpha200_3957,alpha201_3958]alpha201_3958))
                               (Succ n3949))
                          alpha200_3961)@
                        ([alpha200_3961,alpha201_3963]
                          right(([n2]
                                  ([alpha200_3957]n2@alpha200_3957)@
                                  ([alpha200_3957,alpha201_3958]
                                    alpha201_3958))
                                (Succ n3949))
                          alpha200_3961 
                          alpha201_3963))
                      left(nat@@alpha200)_3966)
                right(nat@@alpha200)_3966 
                alpha201_3963))
         ((nat=>nat@@alpha200)_3969 n3943))])
    n3938)@
  ([(nat=>nat@@alpha200)_3969,(nat@@alpha201)_3985]
    ([n3955]
      [if n3955
        ([alpha201_3984]0@(Inhab alpha201))
        ([n3943,alpha201_3984]
         left(n3943@alpha201_3984)@
         right(([(nat@@alpha200)_3966]
                 left(([n3949]
                        ([alpha200_3961]
                          left(([n2]
                                 ([alpha200_3957]n2@alpha200_3957)@
                                 ([alpha200_3957,alpha201_3958]alpha201_3958))
                               (Succ n3949))
                          alpha200_3961)@
                        ([alpha200_3961,alpha201_3963]
                          right(([n2]
                                  ([alpha200_3957]n2@alpha200_3957)@
                                  ([alpha200_3957,alpha201_3958]
                                    alpha201_3958))
                                (Succ n3949))
                          alpha200_3961 
                          alpha201_3963))
                      left(nat@@alpha200)_3966)
                 right(nat@@alpha200)_3966)@
               ([(nat@@alpha200)_3966,alpha201_3963]
                 right(([n3949]
                         ([alpha200_3961]
                           left(([n2]
                                  ([alpha200_3957]n2@alpha200_3957)@
                                  ([alpha200_3957,alpha201_3958]
                                    alpha201_3958))
                                (Succ n3949))
                           alpha200_3961)@
                         ([alpha200_3961,alpha201_3963]
                           right(([n2]
                                   ([alpha200_3957]n2@alpha200_3957)@
                                   ([alpha200_3957,alpha201_3958]
                                     alpha201_3958))
                                 (Succ n3949))
                           alpha200_3961 
                           alpha201_3963))
                       left(nat@@alpha200)_3966)
                 right(nat@@alpha200)_3966 
                 alpha201_3963))
         ((nat=>nat@@alpha200)_3969 left(n3943@alpha201_3984))
         right(n3943@alpha201_3984))])
    left(nat@@alpha201)_3985 
    right(nat@@alpha201)_3985))@
([alpha200_3976,((nat=>nat@@alpha200)@@nat@@alpha201)_3986]
  ([n3955]
    [if n3955
      ([alpha201_3984]
       right(([n2]
               ([alpha200_3973]n2@alpha200_3973)@
               ([alpha200_3973,alpha201_3974]alpha201_3974))
             1)
       alpha200_3976 
       alpha201_3984)
      ([n3943,alpha201_3984](Inhab alpha201))])
  left right((nat=>nat@@alpha200)@@nat@@alpha201)_3986 
  right right((nat=>nat@@alpha200)@@nat@@alpha201)_3986)

([alpha200_0]
  ([(nat=>nat@@alpha200)_1,n2]
    [if n2
      (1@alpha200_0)
      ([n3]
       Succ left((nat=>nat@@alpha200)_1 n3)@right((nat=>nat@@alpha200)_1 n3))])@
  ([(nat=>nat@@alpha200)_1,(nat@@alpha201)_2]
    [if (left(nat@@alpha201)_2)
      (0@(Inhab alpha201))
      ([n3]n3@right(nat@@alpha201)_2)]))@
([alpha200_0,((nat=>nat@@alpha200)@@nat@@alpha201)_1]
  [if (left right((nat=>nat@@alpha200)@@nat@@alpha201)_1)
    (right right((nat=>nat@@alpha200)@@nat@@alpha201)_1)
    ([n2](Inhab alpha201))])

> ; ?_1: R^ 0 1 -> all n1 ex n2 R^(Succ n1)(Succ n2) -> all n1 ex n2 R^ n1 n2
> ; ok, we now have the new goal 
; ?_2: all n1 ex n2 R^ n1 n2 from
;   Base:R^ 0 1
;   Step:all n1 ex n2 R^(Succ n1)(Succ n2)
> ; ok, ?_2 can be obtained from
; ?_4: all n3996 ex n2 R^(Succ n3996)n2 from
;   Base:R^ 0 1
;   Step:all n1 ex n2 R^(Succ n1)(Succ n2)
;   n3994

; ?_3: ex n2 R^ 0 n2 from
;   Base:R^ 0 1
;   Step:all n1 ex n2 R^(Succ n1)(Succ n2)
;   n3994
> ; ok, ?_3 can be obtained from
; ?_5: R^ 0 1 from
;   Base:R^ 0 1
;   Step:all n1 ex n2 R^(Succ n1)(Succ n2)
;   n3994
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all n3996 ex n2 R^(Succ n3996)n2 from
;   Base:R^ 0 1
;   Step:all n1 ex n2 R^(Succ n1)(Succ n2)
;   n3994
> ; ok, we now have the new goal 
; ?_6: ex n2 R^(Succ n1)n2 from
;   Base:R^ 0 1
;   Step:all n1 ex n2 R^(Succ n1)(Succ n2)
;   n3994  n1
> ; ok, ?_6 can be obtained from
; ?_8: ex n2 R^(Succ n1)n2 from
;   Base:R^ 0 1
;   Step:all n1 ex n2 R^(Succ n1)(Succ n2)
;   n3994  n1  Step1:ex n2 R^(Succ n1)(Succ n2)
> ; ok, we now have the new goal 
; ?_11: ex n2 R^(Succ n1)n2 from
;   Base:R^ 0 1
;   Step:all n1 ex n2 R^(Succ n1)(Succ n2)
;   n3994  n1  n2  Step2:R^(Succ n1)(Succ n2)
> ; ok, ?_11 can be obtained from
; ?_12: R^(Succ n1)(Succ n2) from
;   Base:R^ 0 1
;   Step:all n1 ex n2 R^(Succ n1)(Succ n2)
;   n3994  n1  n2  Step2:R^(Succ n1)(Succ n2)
> ; ok, ?_12 is proved.  Proof finished.
> [(nat=>nat)_4008,n3994]
 ([n4005,n4004,(nat=>nat)_4003][if n4005 n4004 (nat=>nat)_4003])n3994
 (([n2]n2)1)
 ([n1]
   ([n4007]
     ([n2,(nat=>nat)_4006](nat=>nat)_4006 n2)n4007([n2]([n2]n2)(Succ n2)))
   ((nat=>nat)_4008 n1))

[(nat=>nat)_0,n1][if n1 1 ([n2]Succ((nat=>nat)_0 n2))]

(([(nat=>nat)_4038,n4009]
   ([n4026]
     [if n4026
       (left(([n2]n2@([alpha207_4042]alpha207_4042))1))
       ([n4014]
        left(([n4035]
               left(([n4020]
                      left(([n2]n2@([alpha207_4028]alpha207_4028))
                           (Succ n4020))@
                      ([alpha207_4032]
                        right(([n2]n2@([alpha207_4028]alpha207_4028))
                              (Succ n4020))
                        alpha207_4032))
                    n4035))@
             ([n4035,alpha207_4032]
               right(([n4020]
                       left(([n2]n2@([alpha207_4028]alpha207_4028))
                            (Succ n4020))@
                       ([alpha207_4032]
                         right(([n2]n2@([alpha207_4028]alpha207_4028))
                               (Succ n4020))
                         alpha207_4032))
                     n4035)
               alpha207_4032))
        ((nat=>nat)_4038 n4014))])
   n4009)@
 ([(nat=>nat)_4038,(nat@@alpha207)_4052]
   ([n4026]
     [if n4026
       ([alpha207_4051]0@(Inhab alpha207))
       ([n4014,alpha207_4051]
        left(n4014@alpha207_4051)@
        right(([n4035]
                left(([n4020]
                       left(([n2]n2@([alpha207_4028]alpha207_4028))
                            (Succ n4020))@
                       ([alpha207_4032]
                         right(([n2]n2@([alpha207_4028]alpha207_4028))
                               (Succ n4020))
                         alpha207_4032))
                     n4035))@
              ([n4035,alpha207_4032]
                right(([n4020]
                        left(([n2]n2@([alpha207_4028]alpha207_4028))
                             (Succ n4020))@
                        ([alpha207_4032]
                          right(([n2]n2@([alpha207_4028]alpha207_4028))
                                (Succ n4020))
                          alpha207_4032))
                      n4035)
                alpha207_4032))
        ((nat=>nat)_4038 left(n4014@alpha207_4051))
        right(n4014@alpha207_4051))])
   left(nat@@alpha207)_4052 
   right(nat@@alpha207)_4052))@
([((nat=>nat)@@nat@@alpha207)_4053]
  ([n4026]
    [if n4026
      ([alpha207_4051]
       right(([n2]n2@([alpha207_4042]alpha207_4042))1)alpha207_4051)
      ([n4014,alpha207_4051](Inhab alpha207))])
  left right((nat=>nat)@@nat@@alpha207)_4053 
  right right((nat=>nat)@@nat@@alpha207)_4053)

(([(nat=>nat)_0,n1][if n1 1 ([n2]Succ((nat=>nat)_0 n2))])@
 ([(nat=>nat)_0,(nat@@alpha207)_1]
   [if (left(nat@@alpha207)_1)
     (0@(Inhab alpha207))
     ([n2]n2@right(nat@@alpha207)_1)]))@
([((nat=>nat)@@nat@@alpha207)_0]
  [if (left right((nat=>nat)@@nat@@alpha207)_0)
    (right right((nat=>nat)@@nat@@alpha207)_0)
    ([n1](Inhab alpha207))])

> ; ?_1: R' 0 1 -> all n1 ex n2 R'(Succ n1)(Succ n2) -> all n1 ex n2 R' n1 n2
> ; ok, we now have the new goal 
; ?_2: all n1 ex n2 R' n1 n2 from
;   Base:R' 0 1
;   Step:all n1 ex n2 R'(Succ n1)(Succ n2)
> ; ok, ?_2 can be obtained from
; ?_4: all n4062 ex n2 R'(Succ n4062)n2 from
;   Base:R' 0 1
;   Step:all n1 ex n2 R'(Succ n1)(Succ n2)
;   n4060

; ?_3: ex n2 R' 0 n2 from
;   Base:R' 0 1
;   Step:all n1 ex n2 R'(Succ n1)(Succ n2)
;   n4060
> ; ok, ?_3 can be obtained from
; ?_5: R' 0 1 from
;   Base:R' 0 1
;   Step:all n1 ex n2 R'(Succ n1)(Succ n2)
;   n4060
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all n4062 ex n2 R'(Succ n4062)n2 from
;   Base:R' 0 1
;   Step:all n1 ex n2 R'(Succ n1)(Succ n2)
;   n4060
> ; ok, we now have the new goal 
; ?_6: ex n2 R'(Succ n1)n2 from
;   Base:R' 0 1
;   Step:all n1 ex n2 R'(Succ n1)(Succ n2)
;   n4060  n1
> ; ok, ?_6 can be obtained from
; ?_8: ex n2 R'(Succ n1)n2 from
;   Base:R' 0 1
;   Step:all n1 ex n2 R'(Succ n1)(Succ n2)
;   n4060  n1  Step1:ex n2 R'(Succ n1)(Succ n2)
> ; ok, we now have the new goal 
; ?_11: ex n2 R'(Succ n1)n2 from
;   Base:R' 0 1
;   Step:all n1 ex n2 R'(Succ n1)(Succ n2)
;   n4060  n1  n2  Step2:R'(Succ n1)(Succ n2)
> ; ok, ?_11 can be obtained from
; ?_12: R'(Succ n1)(Succ n2) from
;   Base:R' 0 1
;   Step:all n1 ex n2 R'(Succ n1)(Succ n2)
;   n4060  n1  n2  Step2:R'(Succ n1)(Succ n2)
> ; ok, ?_12 is proved.  Proof finished.
> [alpha212_4073,(nat=>nat@@alpha212)_4079,n4060]
 ([n4071,(nat@@alpha212)_4070,(nat=>nat@@alpha212)_4069]
   [if n4071 (nat@@alpha212)_4070 (nat=>nat@@alpha212)_4069])
 n4060
 (([n2,alpha212_4072]n2@alpha212_4072)1 alpha212_4073)
 ([n1]
   ([(nat@@alpha212)_4076]
     ([(nat@@alpha212)_4075,(nat=>alpha212=>nat@@alpha212)_4074]
       (nat=>alpha212=>nat@@alpha212)_4074 left(nat@@alpha212)_4075 
       right(nat@@alpha212)_4075)
     (nat@@alpha212)_4076
     ([n2,alpha212_4078]
       ([n2,alpha212_4077]n2@alpha212_4077)(Succ n2)alpha212_4078))
   ((nat=>nat@@alpha212)_4079 n1))

[alpha212_0,(nat=>nat@@alpha212)_1,n2]
 [if n2
   (1@alpha212_0)
   ([n3]Succ left((nat=>nat@@alpha212)_1 n3)@right((nat=>nat@@alpha212)_1 n3))]

[alpha214_4115]
 ([(nat=>nat@@alpha214)_4109,n4081]
   ([n4098]
     [if n4098
       (([n2,alpha214_4113]n2@alpha214_4113)1 alpha214_4115)
       ([n4086]
        ([(nat@@alpha214)_4106]
          ([n4092,alpha214_4103]
            ([n2,alpha214_4100]n2@alpha214_4100)(Succ n4092)alpha214_4103)
          left(nat@@alpha214)_4106 
          right(nat@@alpha214)_4106)
        ((nat=>nat@@alpha214)_4109 n4086))])
   n4081)@
 ([(nat=>nat@@alpha214)_4109,n4121]([n4098][if n4098 0 ([n4086]n4086)])n4121)

[alpha214_0]
 ([(nat=>nat@@alpha214)_1,n2]
   [if n2
     (1@alpha214_0)
     ([n3]
      Succ left((nat=>nat@@alpha214)_1 n3)@right((nat=>nat@@alpha214)_1 n3))])@
 ([(nat=>nat@@alpha214)_1,n2][if n2 0 ([n3]n3)])

> ; ?_1: R^' 0 1 -> all n1 ex n2 R^'(Succ n1)(Succ n2) -> all n1 ex n2 R^' n1 n2
> ; ok, we now have the new goal 
; ?_2: all n1 ex n2 R^' n1 n2 from
;   Base:R^' 0 1
;   Step:all n1 ex n2 R^'(Succ n1)(Succ n2)
> ; ok, ?_2 can be obtained from
; ?_4: all n4127 ex n2 R^'(Succ n4127)n2 from
;   Base:R^' 0 1
;   Step:all n1 ex n2 R^'(Succ n1)(Succ n2)
;   n4125

; ?_3: ex n2 R^' 0 n2 from
;   Base:R^' 0 1
;   Step:all n1 ex n2 R^'(Succ n1)(Succ n2)
;   n4125
> ; ok, ?_3 can be obtained from
; ?_5: R^' 0 1 from
;   Base:R^' 0 1
;   Step:all n1 ex n2 R^'(Succ n1)(Succ n2)
;   n4125
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all n4127 ex n2 R^'(Succ n4127)n2 from
;   Base:R^' 0 1
;   Step:all n1 ex n2 R^'(Succ n1)(Succ n2)
;   n4125
> ; ok, we now have the new goal 
; ?_6: ex n2 R^'(Succ n1)n2 from
;   Base:R^' 0 1
;   Step:all n1 ex n2 R^'(Succ n1)(Succ n2)
;   n4125  n1
> ; ok, ?_6 can be obtained from
; ?_8: ex n2 R^'(Succ n1)n2 from
;   Base:R^' 0 1
;   Step:all n1 ex n2 R^'(Succ n1)(Succ n2)
;   n4125  n1  Step1:ex n2 R^'(Succ n1)(Succ n2)
> ; ok, we now have the new goal 
; ?_11: ex n2 R^'(Succ n1)n2 from
;   Base:R^' 0 1
;   Step:all n1 ex n2 R^'(Succ n1)(Succ n2)
;   n4125  n1  n2  Step2:R^'(Succ n1)(Succ n2)
> ; ok, ?_11 can be obtained from
; ?_12: R^'(Succ n1)(Succ n2) from
;   Base:R^' 0 1
;   Step:all n1 ex n2 R^'(Succ n1)(Succ n2)
;   n4125  n1  n2  Step2:R^'(Succ n1)(Succ n2)
> ; ok, ?_12 is proved.  Proof finished.
> [(nat=>nat)_4139,n4125]
 ([n4136,n4135,(nat=>nat)_4134][if n4136 n4135 (nat=>nat)_4134])n4125
 (([n2]n2)1)
 ([n1]
   ([n4138]
     ([n2,(nat=>nat)_4137](nat=>nat)_4137 n2)n4138([n2]([n2]n2)(Succ n2)))
   ((nat=>nat)_4139 n1))

[(nat=>nat)_0,n1][if n1 1 ([n2]Succ((nat=>nat)_0 n2))]

([(nat=>nat)_4165,n4140]
  ([n4157]
    [if n4157
      (([n2]n2)1)
      ([n4145]
       ([n4162]([n4151]([n2]n2)(Succ n4151))n4162)((nat=>nat)_4165 n4145))])
  n4140)@
([(nat=>nat)_4165,n4174]([n4157][if n4157 0 ([n4145]n4145)])n4174)

([(nat=>nat)_0,n1][if n1 1 ([n2]Succ((nat=>nat)_0 n2))])@
([(nat=>nat)_0,n1][if n1 0 ([n2]n2)])

> ; ?_1: R 0 1 -> all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2)) -> all n1 ex n2 R n1 n2
> ; ok, we now have the new goal 
; ?_2: all n1 ex n2 R n1 n2 from
;   Base:R 0 1
;   Step:all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2))
> ; ok, ?_2 can be obtained from
; ?_4: all n4179(ex n2 R n4179 n2 -> ex n2 R(Succ n4179)n2) from
;   Base:R 0 1
;   Step:all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2))
;   n4177

; ?_3: ex n2 R 0 n2 from
;   Base:R 0 1
;   Step:all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2))
;   n4177
> ; ok, ?_3 can be obtained from
; ?_5: R 0 1 from
;   Base:R 0 1
;   Step:all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2))
;   n4177
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all n4179(ex n2 R n4179 n2 -> ex n2 R(Succ n4179)n2) from
;   Base:R 0 1
;   Step:all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2))
;   n4177
> ; ok, we now have the new goal 
; ?_6: ex n2 R(Succ n1)n2 from
;   Base:R 0 1
;   Step:all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2))
;   n4177  n1  IH:ex n2 R n1 n2
> ; ok, we now have the new goal 
; ?_9: ex n2 R(Succ n1)n2 from
;   Base:R 0 1
;   Step:all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2))
;   n4177  n1  n2  IH1:R n1 n2
> ; ok, ?_9 can be obtained from
; ?_11: ex n2 R(Succ n1)n2 from
;   Base:R 0 1
;   Step:all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2))
;   n4177  n1  n2  IH1:R n1 n2
;   Step1:all n2(R n1 n2 -> R(Succ n1)(Succ n2))
> ; ok, ?_11 can be obtained from
; ?_12: R(Succ n1)(Succ n2) from
;   Base:R 0 1
;   Step:all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2))
;   n4177  n1  n2  IH1:R n1 n2
;   Step1:all n2(R n1 n2 -> R(Succ n1)(Succ n2))
> ; ok, ?_12 can be obtained from
; ?_13: R n1 n2 from
;   Base:R 0 1
;   Step:all n1,n2(R n1 n2 -> R(Succ n1)(Succ n2))
;   n4177  n1  n2  IH1:R n1 n2
;   Step1:all n2(R n1 n2 -> R(Succ n1)(Succ n2))
> ; ok, ?_13 is proved.  Proof finished.
> [alpha198_4190,(nat=>nat=>alpha198=>alpha198)_4197,n4177]
 (Rec nat=>nat@@alpha198)n4177
 (([n2,alpha198_4189]n2@alpha198_4189)1 alpha198_4190)
 ([n1,(nat@@alpha198)_4193]
   ([(nat@@alpha198)_4192,(nat=>alpha198=>nat@@alpha198)_4191]
     (nat=>alpha198=>nat@@alpha198)_4191 left(nat@@alpha198)_4192 
     right(nat@@alpha198)_4192)
   (nat@@alpha198)_4193
   ([n2,alpha198_4196]
     ([(nat=>alpha198=>alpha198)_4195]
       ([n2,alpha198_4194]n2@alpha198_4194)(Succ n2)
       ((nat=>alpha198=>alpha198)_4195 n2 alpha198_4196))
     ((nat=>nat=>alpha198=>alpha198)_4197 n1)))

[alpha198_0,(nat=>nat=>alpha198=>alpha198)_1,n2]
 (Rec nat=>nat@@alpha198)n2(1@alpha198_0)
 ([n3,(nat@@alpha198)_4]
   Succ left(nat@@alpha198)_4@
   (nat=>nat=>alpha198=>alpha198)_1 n3 left(nat@@alpha198)_4 
   right(nat@@alpha198)_4)

> ; ?_1: R^' 0 1 -> 
;      all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2)) -> 
;      all n1 ex n2 R^' n1 n2
> ; ok, we now have the new goal 
; ?_2: all n1 ex n2 R^' n1 n2 from
;   Base:R^' 0 1
;   Step:all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
> ; ok, ?_2 can be obtained from
; ?_4: all n4200(ex n2 R^' n4200 n2 -> ex n2 R^'(Succ n4200)n2) from
;   Base:R^' 0 1
;   Step:all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4198

; ?_3: ex n2 R^' 0 n2 from
;   Base:R^' 0 1
;   Step:all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4198
> ; ok, ?_3 can be obtained from
; ?_5: R^' 0 1 from
;   Base:R^' 0 1
;   Step:all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4198
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all n4200(ex n2 R^' n4200 n2 -> ex n2 R^'(Succ n4200)n2) from
;   Base:R^' 0 1
;   Step:all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4198
> ; ok, we now have the new goal 
; ?_6: ex n2 R^'(Succ n1)n2 from
;   Base:R^' 0 1
;   Step:all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4198  n1  IH:ex n2 R^' n1 n2
> ; ok, we now have the new goal 
; ?_9: ex n2 R^'(Succ n1)n2 from
;   Base:R^' 0 1
;   Step:all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4198  n1  n2  IH1:R^' n1 n2
> ; ok, ?_9 can be obtained from
; ?_11: ex n2 R^'(Succ n1)n2 from
;   Base:R^' 0 1
;   Step:all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4198  n1  n2  IH1:R^' n1 n2
;   Step1:all n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
> ; ok, ?_11 can be obtained from
; ?_12: R^'(Succ n1)(Succ n2) from
;   Base:R^' 0 1
;   Step:all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4198  n1  n2  IH1:R^' n1 n2
;   Step1:all n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
> ; ok, ?_12 can be obtained from
; ?_13: R^' n1 n2 from
;   Base:R^' 0 1
;   Step:all n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4198  n1  n2  IH1:R^' n1 n2
;   Step1:all n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
> ; ok, ?_13 is proved.  Proof finished.
> [n4198]
 (Rec nat=>nat)n4198(([n2]n2)1)
 ([n1,n4211]
   ([n2,(nat=>nat)_4210](nat=>nat)_4210 n2)n4211([n2]([n2]n2)(Succ n2)))

[n0](Rec nat=>nat)n0 1([n1]Succ)

> ; ?_1: R^' 0 1 -> 
;      allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2)) -> 
;      all n1 ex n2 R^' n1 n2
> ; ok, we now have the new goal 
; ?_2: all n1 ex n2 R^' n1 n2 from
;   Base:R^' 0 1
;   Step:allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
> ; ok, ?_2 can be obtained from
; ?_4: all n4214(ex n2 R^' n4214 n2 -> ex n2 R^'(Succ n4214)n2) from
;   Base:R^' 0 1
;   Step:allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4212

; ?_3: ex n2 R^' 0 n2 from
;   Base:R^' 0 1
;   Step:allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4212
> ; ok, ?_3 can be obtained from
; ?_5: R^' 0 1 from
;   Base:R^' 0 1
;   Step:allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4212
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all n4214(ex n2 R^' n4214 n2 -> ex n2 R^'(Succ n4214)n2) from
;   Base:R^' 0 1
;   Step:allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4212
> ; ok, we now have the new goal 
; ?_6: ex n2 R^'(Succ n1)n2 from
;   Base:R^' 0 1
;   Step:allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4212  n1  IH:ex n2 R^' n1 n2
> ; ok, we now have the new goal 
; ?_9: ex n2 R^'(Succ n1)n2 from
;   Base:R^' 0 1
;   Step:allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4212  n1  n2  IH1:R^' n1 n2
> ; ok, ?_9 can be obtained from
; ?_11: ex n2 R^'(Succ n1)n2 from
;   Base:R^' 0 1
;   Step:allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4212  n1  n2  IH1:R^' n1 n2
;   Step1:allnc n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
> ; ok, ?_11 can be obtained from
; ?_12: R^'(Succ n1)(Succ n2) from
;   Base:R^' 0 1
;   Step:allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4212  n1  n2  IH1:R^' n1 n2
;   Step1:allnc n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
> ; ok, ?_12 can be obtained from
; ?_13: R^' n1 n2 from
;   Base:R^' 0 1
;   Step:allnc n1,n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
;   n4212  n1  n2  IH1:R^' n1 n2
;   Step1:allnc n2(R^' n1 n2 -> R^'(Succ n1)(Succ n2))
> ; ok, ?_13 is proved.  Proof finished.
> [n4212]
 (Rec nat=>nat)n4212(([n2]n2)1)
 ([n1,n4225]
   ([n2,(nat=>nat)_4224](nat=>nat)_4224 n2)n4225([n2]([n2]n2)(Succ n2)))

[n0](Rec nat=>nat)n0 1([n1]Succ)

[n4226]
 ([n4243]
   (Rec nat=>nat)n4243(([n2]n2)1)
   ([n4231,n4248]([n4237]([n2]n2)(Succ n4237))n4248))
 n4226

[n0](Rec nat=>nat)n0 1([n1]Succ)

> ; ?_1: all n1(all n3(n3<n1 -> ex n2 R n3 n2) -> ex n2 R n1 n2) -> 
;      all n1 ex n2 R n1 n2
> ; ok, we now have the new goal 
; ?_2: all n1 ex n2 R n1 n2 from
;   L:all n1(all n3(n3<n1 -> ex n2 R n3 n2) -> ex n2 R n1 n2)
> ; ok, ?_2 can be obtained from
; ?_3: all n4263(
;       all n4264(([n]n)n4264<([n]n)n4263 -> ex n2 R n4264 n2) -> 
;       ex n2 R n4263 n2) from
;   L:all n1(all n3(n3<n1 -> ex n2 R n3 n2) -> ex n2 R n1 n2)
;   n4261
> ; ok, we now have the new goal 
; ?_4: ex n2 R n1 n2 from
;   L:all n1(all n3(n3<n1 -> ex n2 R n3 n2) -> ex n2 R n1 n2)
;   n4261  n1  GIH:all n4264(([n]n)n4264<([n]n)n1 -> ex n2 R n4264 n2)
> ; ok, ?_4 can be obtained from
; ?_5: all n3(n3<n1 -> ex n2 R n3 n2) from
;   L:all n1(all n3(n3<n1 -> ex n2 R n3 n2) -> ex n2 R n1 n2)
;   n4261  n1  GIH:all n4264(([n]n)n4264<([n]n)n1 -> ex n2 R n4264 n2)
> ; ok, ?_5 is proved.  Proof finished.
> [(nat=>(nat=>nat@@alpha198)=>nat@@alpha198)_4271,n4261]
 (GRec nat nat@@alpha198)([n]n)n4261
 ([n1,(nat=>nat@@alpha198)_4272]
   (nat=>(nat=>nat@@alpha198)=>nat@@alpha198)_4271 n1
   (nat=>nat@@alpha198)_4272)

[(nat=>(nat=>nat@@alpha198)=>nat@@alpha198)_0,n1]
 (nat=>(nat=>nat@@alpha198)=>nat@@alpha198)_0 n1
 ([n2]
   (GRecGuard nat nat@@alpha198)([n3]n3)n2
   (nat=>(nat=>nat@@alpha198)=>nat@@alpha198)_0
   (n2<n1))

> ; ok, predicate variable R is removed
; warning: R was default pvariable of arity (arity nat nat)
> ; ok, predicate variable R: (arity list nat list nat) added
> ; ?_1: R(Nil nat)(0:) -> 
;      all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2)) -> 
;      all ns1 ex ns2 R ns1 ns2
> ; ok, we now have the new goal 
; ?_2: all ns1 ex ns2 R ns1 ns2 from
;   Base:R(Nil nat)(0:)
;   Step:all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
> ; ok, ?_2 can be obtained from
; ?_4: all n4278,ns4279(ex ns2 R ns4279 ns2 -> ex ns2 R(n4278::ns4279)ns2) from
;   Base:R(Nil nat)(0:)
;   Step:all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
;   ns4273

; ?_3: ex ns2 R(Nil nat)ns2 from
;   Base:R(Nil nat)(0:)
;   Step:all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
;   ns4273
> ; ok, ?_3 can be obtained from
; ?_5: R(Nil nat)(0:) from
;   Base:R(Nil nat)(0:)
;   Step:all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
;   ns4273
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all n4278,ns4279(ex ns2 R ns4279 ns2 -> ex ns2 R(n4278::ns4279)ns2) from
;   Base:R(Nil nat)(0:)
;   Step:all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
;   ns4273
> ; ok, we now have the new goal 
; ?_6: ex ns2 R(n::ns1)ns2 from
;   Base:R(Nil nat)(0:)
;   Step:all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
;   ns4273  n  ns1  IH:ex ns2 R ns1 ns2
> ; ok, we now have the new goal 
; ?_9: ex ns2 R(n::ns1)ns2 from
;   Base:R(Nil nat)(0:)
;   Step:all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
;   ns4273  n  ns1  ns2  IH1:
;     R ns1 ns2
> ; ok, ?_9 can be obtained from
; ?_11: ex ns2 R(n::ns1)ns2 from
;   Base:R(Nil nat)(0:)
;   Step:all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
;   ns4273  n  ns1  ns2  IH1:
;     R ns1 ns2
;   Step1:all ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
> ; ok, ?_11 can be obtained from
; ?_12: R(n::ns1)(n::ns2) from
;   Base:R(Nil nat)(0:)
;   Step:all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
;   ns4273  n  ns1  ns2  IH1:
;     R ns1 ns2
;   Step1:all ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
> ; ok, ?_12 can be obtained from
; ?_13: R ns1 ns2 from
;   Base:R(Nil nat)(0:)
;   Step:all ns1,ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
;   ns4273  n  ns1  ns2  IH1:
;     R ns1 ns2
;   Step1:all ns2,n(R ns1 ns2 -> R(n::ns1)(n::ns2))
> ; ok, ?_13 is proved.  Proof finished.
> [alpha238_4292,(list nat=>list nat=>nat=>alpha238=>alpha238)_4299,ns4273]
 (Rec list nat=>list nat@@alpha238)ns4273
 (([ns2,alpha238_4291]ns2@alpha238_4291)0:alpha238_4292)
 ([n,ns1,(list nat@@alpha238)_4295]
   ([(list nat@@alpha238)_4294,(list nat=>alpha238=>list nat@@alpha238)_4293]
     (list nat=>alpha238=>list nat@@alpha238)_4293 
     left(list nat@@alpha238)_4294 
     right(list nat@@alpha238)_4294)
   (list nat@@alpha238)_4295
   ([ns2,alpha238_4298]
     ([(list nat=>nat=>alpha238=>alpha238)_4297]
       ([ns2,alpha238_4296]ns2@alpha238_4296)(n::ns2)
       ((list nat=>nat=>alpha238=>alpha238)_4297 ns2 n alpha238_4298))
     ((list nat=>list nat=>nat=>alpha238=>alpha238)_4299 ns1)))

[alpha238_0,(list nat=>list nat=>nat=>alpha238=>alpha238)_1,ns2]
 (Rec list nat=>list nat@@alpha238)ns2(0: @alpha238_0)
 ([n3,ns4,(list nat@@alpha238)_5]
   (n3::left(list nat@@alpha238)_5)@
   (list nat=>list nat=>nat=>alpha238=>alpha238)_1 ns4 
   left(list nat@@alpha238)_5 
   n3 
   right(list nat@@alpha238)_5)

> ; ?_1: R^'(Nil nat)(0:) -> 
;      all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2)) -> 
;      all ns1 ex ns2 R^' ns1 ns2
> ; ok, we now have the new goal 
; ?_2: all ns1 ex ns2 R^' ns1 ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
> ; ok, ?_2 can be obtained from
; ?_4: all n4305,ns4306(ex ns2 R^' ns4306 ns2 -> ex ns2 R^'(n4305::ns4306)ns2) from
;   Base:R^'(Nil nat)(0:)
;   Step:all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4300

; ?_3: ex ns2 R^'(Nil nat)ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4300
> ; ok, ?_3 can be obtained from
; ?_5: R^'(Nil nat)(0:) from
;   Base:R^'(Nil nat)(0:)
;   Step:all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4300
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all n4305,ns4306(ex ns2 R^' ns4306 ns2 -> ex ns2 R^'(n4305::ns4306)ns2) from
;   Base:R^'(Nil nat)(0:)
;   Step:all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4300
> ; ok, we now have the new goal 
; ?_6: ex ns2 R^'(n::ns1)ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4300  n  ns1  IH:ex ns2 R^' ns1 ns2
> ; ok, we now have the new goal 
; ?_9: ex ns2 R^'(n::ns1)ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4300  n  ns1  ns2  IH1:
;     R^' ns1 ns2
> ; ok, ?_9 can be obtained from
; ?_11: ex ns2 R^'(n::ns1)ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4300  n  ns1  ns2  IH1:
;     R^' ns1 ns2
;   Step1:all ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
> ; ok, ?_11 can be obtained from
; ?_12: R^'(n::ns1)(n::ns2) from
;   Base:R^'(Nil nat)(0:)
;   Step:all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4300  n  ns1  ns2  IH1:
;     R^' ns1 ns2
;   Step1:all ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
> ; ok, ?_12 can be obtained from
; ?_13: R^' ns1 ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:all ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4300  n  ns1  ns2  IH1:
;     R^' ns1 ns2
;   Step1:all ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
> ; ok, ?_13 is proved.  Proof finished.
> [ns4300]
 (Rec list nat=>list nat)ns4300(([ns2]ns2)0:)
 ([n,ns1,ns4319]
   ([ns2,(list nat=>list nat)_4318](list nat=>list nat)_4318 ns2)ns4319
   ([ns2]([ns2]ns2)(n::ns2)))

[ns0](Rec list nat=>list nat)ns0 0:([n1,ns2](Cons nat)n1)

> ; ?_1: R^'(Nil nat)(0:) -> 
;      allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2)) -> 
;      all ns1 ex ns2 R^' ns1 ns2
> ; ok, we now have the new goal 
; ?_2: all ns1 ex ns2 R^' ns1 ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
> ; ok, ?_2 can be obtained from
; ?_4: all n4325,ns4326(ex ns2 R^' ns4326 ns2 -> ex ns2 R^'(n4325::ns4326)ns2) from
;   Base:R^'(Nil nat)(0:)
;   Step:allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4320

; ?_3: ex ns2 R^'(Nil nat)ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4320
> ; ok, ?_3 can be obtained from
; ?_5: R^'(Nil nat)(0:) from
;   Base:R^'(Nil nat)(0:)
;   Step:allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4320
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all n4325,ns4326(ex ns2 R^' ns4326 ns2 -> ex ns2 R^'(n4325::ns4326)ns2) from
;   Base:R^'(Nil nat)(0:)
;   Step:allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4320
> ; ok, we now have the new goal 
; ?_6: ex ns2 R^'(n::ns1)ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4320  n  ns1  IH:ex ns2 R^' ns1 ns2
> ; ok, we now have the new goal 
; ?_9: ex ns2 R^'(n::ns1)ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4320  n  ns1  ns2  IH1:
;     R^' ns1 ns2
> ; ok, ?_9 can be obtained from
; ?_11: ex ns2 R^'(n::ns1)ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4320  n  ns1  ns2  IH1:
;     R^' ns1 ns2
;   Step1:allnc ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
> ; ok, ?_11 can be obtained from
; ?_12: R^'(n::ns1)(n::ns2) from
;   Base:R^'(Nil nat)(0:)
;   Step:allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4320  n  ns1  ns2  IH1:
;     R^' ns1 ns2
;   Step1:allnc ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
> ; ok, ?_12 can be obtained from
; ?_13: R^' ns1 ns2 from
;   Base:R^'(Nil nat)(0:)
;   Step:allnc ns1,ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
;   ns4320  n  ns1  ns2  IH1:
;     R^' ns1 ns2
;   Step1:allnc ns2,n(R^' ns1 ns2 -> R^'(n::ns1)(n::ns2))
> ; ok, ?_13 is proved.  Proof finished.
> [ns4320]
 (Rec list nat=>list nat)ns4320(([ns2]ns2)0:)
 ([n,ns1,ns4339]
   ([ns2,(list nat=>list nat)_4338](list nat=>list nat)_4338 ns2)ns4339
   ([ns2]([ns2]ns2)(n::ns2)))

[ns0](Rec list nat=>list nat)ns0 0:([n1,ns2](Cons nat)n1)

[ns4340]
 ([ns4370]
   (Rec list nat=>list nat)ns4370(([ns2]ns2)0:)
   ([n4357,ns4358,ns4376]([ns4364]([ns2]ns2)(n4357::ns4364))ns4376))
 ns4340

[ns0](Rec list nat=>list nat)ns0 0:([n1,ns2](Cons nat)n1)

> ; ok, predicate variable R is removed
; warning: R was default pvariable of arity (arity list nat list nat)
> ; ok, variable ns is removed
; warning: ns was default variable of type list nat
> ; ok, variable x: alpha added
> ; ok, variable xs: list alpha added
> ; ok, predicate variable R: (arity list alpha list alpha) added
> ; ?_1: R(Nil alpha)(Nil alpha) -> 
;      all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2)) -> 
;      all xs1 ex xs2 R xs1 xs2
> ; ok, we now have the new goal 
; ?_2: all xs1 ex xs2 R xs1 xs2 from
;   Base:R(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
> ; ok, ?_2 can be obtained from
; ?_4: all x4397,xs4398(ex xs2 R xs4398 xs2 -> ex xs2 R(x4397::xs4398)xs2) from
;   Base:R(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
;   xs4392

; ?_3: ex xs2 R(Nil alpha)xs2 from
;   Base:R(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
;   xs4392
> ; ok, ?_3 can be obtained from
; ?_5: R(Nil alpha)(Nil alpha) from
;   Base:R(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
;   xs4392
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all x4397,xs4398(ex xs2 R xs4398 xs2 -> ex xs2 R(x4397::xs4398)xs2) from
;   Base:R(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
;   xs4392
> ; ok, we now have the new goal 
; ?_6: ex xs2 R(x::xs1)xs2 from
;   Base:R(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
;   xs4392  x  xs1  IH:ex xs2 R xs1 xs2
> ; ok, we now have the new goal 
; ?_9: ex xs2 R(x::xs1)xs2 from
;   Base:R(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
;   xs4392  x  xs1  xs2  IH1:
;     R xs1 xs2
> ; ok, ?_9 can be obtained from
; ?_11: ex xs2 R(x::xs1)xs2 from
;   Base:R(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
;   xs4392  x  xs1  xs2  IH1:
;     R xs1 xs2
;   Step1:all xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
> ; ok, ?_11 can be obtained from
; ?_12: R(x::xs1)(x::xs2) from
;   Base:R(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
;   xs4392  x  xs1  xs2  IH1:
;     R xs1 xs2
;   Step1:all xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
> ; ok, ?_12 can be obtained from
; ?_13: R xs1 xs2 from
;   Base:R(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
;   xs4392  x  xs1  xs2  IH1:
;     R xs1 xs2
;   Step1:all xs2,x(R xs1 xs2 -> R(x::xs1)(x::xs2))
> ; ok, ?_13 is proved.  Proof finished.
> [alpha260_4411,(list alpha=>list alpha=>alpha=>alpha260=>alpha260)_4418,xs4392]
 (Rec list alpha=>list alpha@@alpha260)xs4392
 (([xs2,alpha260_4410]xs2@alpha260_4410)(Nil alpha)alpha260_4411)
 ([x,xs1,(list alpha@@alpha260)_4414]
   ([(list alpha@@alpha260)_4413,(list alpha=>alpha260=>list alpha@@alpha260)_4412]
     (list alpha=>alpha260=>list alpha@@alpha260)_4412 
     left(list alpha@@alpha260)_4413 
     right(list alpha@@alpha260)_4413)
   (list alpha@@alpha260)_4414
   ([xs2,alpha260_4417]
     ([(list alpha=>alpha=>alpha260=>alpha260)_4416]
       ([xs2,alpha260_4415]xs2@alpha260_4415)(x::xs2)
       ((list alpha=>alpha=>alpha260=>alpha260)_4416 xs2 x alpha260_4417))
     ((list alpha=>list alpha=>alpha=>alpha260=>alpha260)_4418 xs1)))

[alpha260_0,(list alpha=>list alpha=>alpha=>alpha260=>alpha260)_1,xs2]
 (Rec list alpha=>list alpha@@alpha260)xs2((Nil alpha)@alpha260_0)
 ([x3,xs4,(list alpha@@alpha260)_5]
   (x3::left(list alpha@@alpha260)_5)@
   (list alpha=>list alpha=>alpha=>alpha260=>alpha260)_1 xs4 
   left(list alpha@@alpha260)_5 
   x3 
   right(list alpha@@alpha260)_5)

> ; ?_1: R^'(Nil alpha)(Nil alpha) -> 
;      all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2)) -> 
;      all xs1 ex xs2 R^' xs1 xs2
> ; ok, we now have the new goal 
; ?_2: all xs1 ex xs2 R^' xs1 xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
> ; ok, ?_2 can be obtained from
; ?_4: all x4424,xs4425(ex xs2 R^' xs4425 xs2 -> ex xs2 R^'(x4424::xs4425)xs2) from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4419

; ?_3: ex xs2 R^'(Nil alpha)xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4419
> ; ok, ?_3 can be obtained from
; ?_5: R^'(Nil alpha)(Nil alpha) from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4419
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all x4424,xs4425(ex xs2 R^' xs4425 xs2 -> ex xs2 R^'(x4424::xs4425)xs2) from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4419
> ; ok, we now have the new goal 
; ?_6: ex xs2 R^'(x::xs1)xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4419  x  xs1  IH:ex xs2 R^' xs1 xs2
> ; ok, we now have the new goal 
; ?_9: ex xs2 R^'(x::xs1)xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4419  x  xs1  xs2  IH1:
;     R^' xs1 xs2
> ; ok, ?_9 can be obtained from
; ?_11: ex xs2 R^'(x::xs1)xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4419  x  xs1  xs2  IH1:
;     R^' xs1 xs2
;   Step1:all xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
> ; ok, ?_11 can be obtained from
; ?_12: R^'(x::xs1)(x::xs2) from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4419  x  xs1  xs2  IH1:
;     R^' xs1 xs2
;   Step1:all xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
> ; ok, ?_12 can be obtained from
; ?_13: R^' xs1 xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:all xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4419  x  xs1  xs2  IH1:
;     R^' xs1 xs2
;   Step1:all xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
> ; ok, ?_13 is proved.  Proof finished.
> [xs4419]
 (Rec list alpha=>list alpha)xs4419(([xs2]xs2)(Nil alpha))
 ([x,xs1,xs4438]
   ([xs2,(list alpha=>list alpha)_4437](list alpha=>list alpha)_4437 xs2)
   xs4438
   ([xs2]([xs2]xs2)(x::xs2)))

[xs0](Rec list alpha=>list alpha)xs0(Nil alpha)([x1,xs2](Cons alpha)x1)

> ; ?_1: R^'(Nil alpha)(Nil alpha) -> 
;      allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2)) -> 
;      all xs1 ex xs2 R^' xs1 xs2
> ; ok, we now have the new goal 
; ?_2: all xs1 ex xs2 R^' xs1 xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
> ; ok, ?_2 can be obtained from
; ?_4: all x4444,xs4445(ex xs2 R^' xs4445 xs2 -> ex xs2 R^'(x4444::xs4445)xs2) from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4439

; ?_3: ex xs2 R^'(Nil alpha)xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4439
> ; ok, ?_3 can be obtained from
; ?_5: R^'(Nil alpha)(Nil alpha) from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4439
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all x4444,xs4445(ex xs2 R^' xs4445 xs2 -> ex xs2 R^'(x4444::xs4445)xs2) from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4439
> ; ok, we now have the new goal 
; ?_6: ex xs2 R^'(x::xs1)xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4439  x  xs1  IH:ex xs2 R^' xs1 xs2
> ; ok, we now have the new goal 
; ?_9: ex xs2 R^'(x::xs1)xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4439  x  xs1  xs2  IH1:
;     R^' xs1 xs2
> ; ok, ?_9 can be obtained from
; ?_11: ex xs2 R^'(x::xs1)xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4439  x  xs1  xs2  IH1:
;     R^' xs1 xs2
;   Step1:allnc xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
> ; ok, ?_11 can be obtained from
; ?_12: R^'(x::xs1)(x::xs2) from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4439  x  xs1  xs2  IH1:
;     R^' xs1 xs2
;   Step1:allnc xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
> ; ok, ?_12 can be obtained from
; ?_13: R^' xs1 xs2 from
;   Base:R^'(Nil alpha)(Nil alpha)
;   Step:allnc xs1,xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
;   xs4439  x  xs1  xs2  IH1:
;     R^' xs1 xs2
;   Step1:allnc xs2,x(R^' xs1 xs2 -> R^'(x::xs1)(x::xs2))
> ; ok, ?_13 is proved.  Proof finished.
> [xs4439]
 (Rec list alpha=>list alpha)xs4439(([xs2]xs2)(Nil alpha))
 ([x,xs1,xs4458]
   ([xs2,(list alpha=>list alpha)_4457](list alpha=>list alpha)_4457 xs2)
   xs4458
   ([xs2]([xs2]xs2)(x::xs2)))

[xs0](Rec list alpha=>list alpha)xs0(Nil alpha)([x1,xs2](Cons alpha)x1)

[xs4459]
 ([xs4489]
   (Rec list alpha=>list alpha)xs4489(([xs2]xs2)(Nil alpha))
   ([x4476,xs4477,xs4495]([xs4483]([xs2]xs2)(x4476::xs4483))xs4495))
 xs4459

[xs0](Rec list alpha=>list alpha)xs0(Nil alpha)([x1,xs2](Cons alpha)x1)

> ; ok, predicate variable R is removed
; warning: R was default pvariable of arity (arity list alpha list alpha)
> ; ok, variable x is removed
; warning: x was default variable of type alpha
; ok, variable xs is removed
; warning: xs was default variable of type list alpha
>