trace of eval lazy (iseven (2 * 1))

context.v

Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => S (p + m)
  end

where "n + m" := (add n m) : nat_scope.

Fixpoint mul n m :=
  match n with
  | 0 => 0
  | S p => m + p * m
  end

where "n * m" := (mul n m) : nat_scope.

Fixpoint iseven n :=
  match n with
  | 0 => true
  | S x =>
      match x with
      | 0 => false
      | S y => iseven y
      end
  end.

explanations.md

we look at evaluating iseven (2 * 1) with term sharing OFF (on this evaluation I think term sharing mostly turns some FCLOS(S 0,[]) into FApp(S, 0) but it makes it harder to keep track of what's changing)

reminder: kni = knh followed by knr knit = knht followed by knr

terms in explicit substitutions (fclos) are written term[subst] terms containing explicit substitutions are written (fun x : a => b)@[subst] knht takes a substitution as first argument

stack elements are applicative by default (ie we say ZFIX but not ZAPP)

(U) means the stack of the previous step TODO use (POP n) instead of copying the full tail when popping?

I will write !iseven !* and !+ for the raw fixpoints ((*) (+) (!*) (!+) when not applied)

?iseven, add and mul are the unbound rels in the respective raw fixpoints

trace.txt

KNI (iseven (2 * 1))[] |
KNH (iseven (2 * 1))[] |
KNHT [] (iseven (2 * 1)) |
KNHT [] iseven | (2 * 1)[]
KNR iseven | (U)
DELTA iseven (INJECT body of iseven)
KNH (!iseven)[] | (U)
KNHT [] (!iseven) | (U)
KNH !iseven@[] | (U)
KNH (2 * 1)[] | ZFIX(!iseven@[])
KNHT [] (2 * 1) | (U)
KNHT [] (*) | 2[]; 1[]; (U)
KNR (*) | (U)
DELTA (*) (INJECT body of (*))
KNH (!*)[] | (U)
KNHT [] (!*) | (U)
KNH (!*@[]) | (U)
KNH 2[] | ZFIX(!*@[]); 1[]; ZFIX(!iseven@[])
KNHT [] 2 | (U)
KNHT [] S | 1[]; (U)
KNR S | (U)
UNFOLD FIX (!*@[]) (reconstruct argument "S 1[]")
KNHT [mul:=(!*)@[]] (fun n m => body of (!*)) | (S 1[]); 1[]; ZFIX(!iseven@[])
KNR (fun n m => body of (!*))@[mul:=(!*)@[]] | (U)
BETA (2 beta steps combined)
KNHT [mul:=(!*)@[]; n:=(S 1[]); m:=1[]] ((*)'s match n with ...) | ZFIX(!iseven@[])
KNHT [mul:=(!*)@[]; n:=(S 1[]); m:=1[]] n | ZCASE((*)'s match ? with ... end@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]]); ZFIX(!iseven@[])
KNH (S 1[]) | (U)
KNH S | 1[]; (U)
IOTA (*)'s match@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]] branch S, arg p:=1[]
KNHT [mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]] (m + mul p m) | ZFIX(!iseven@[])
KNHT [mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]] (+) | 1[]; (mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; (U)
KNR (+) | (U)
DELTA (+) (INJECT body of (+))
KNH (!+)[] | (U)
KNHT [] (!+) | (U)
KNH (+!@[]) | (U)
KNH 1[] | ZFIX(!+@[]); (mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; ZFIX(!iseven@[])
KNHT [] 1 | (U)
KNHT [] S | 0; (U)
KNR S | (U)
UNFOLD FIX (!+@[]) (reconstruct argument "S 0")
KNHT [add:=(!+)@[]] (fun n m => body of (+)) | S 0; (mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; ZFIX(!iseven@[])
KNR (fun n m => body of (+))@[add:=(!+)@[]] | (U)
BETA (2 beta steps combined)
KNHT [add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]] (body of (+)) | ZFIX(!iseven@[])
KNHT [add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]] n | ZCASE((+)'s match ? with end@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]]); (U)
KNH S 0 | (U)
KNH S | 0; (U)
KNR S | 0; (U)
IOTA (+)'s match@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]] branch S, arg p:=0
KNHT [add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0] S (add p m) | ZFIX(!iseven@[])
KNHT [add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0] S | (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; (U)
KNR S | (U)
UNFOLD FIX (!iseven@[]) (reconstruct argument "S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]")
KNHT [iseven:=(!iseven@[])] (fun n => body of iseven) | S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]
KNR (fun n => body of iseven)@[iseven:=(!iseven@[])] | (U)
BETA (1 step)
KNHT [iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]] (1st match of iseven) |
KNHT [iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]] n | ZCASE(1st match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNH S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0] | (U)
KNH S | (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; (U)
KNR S | (U)
IOTA (1st match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]]) branch S, arg x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]
KNHT [iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]] (2nd match of iseven) |
KNHT [iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]] x | ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNH (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0] | (U)
KNHT [add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0] (add p m) | (U)
KNHT [add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0] add | 0; (mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; (U)
KNH (!+)@[] | (U)
KNH 0 | ZFIX(!+@[]); (mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNR 0 | (U)
UNFOLD FIX (!+@[]) (trivial reconstruct argument "0")
KNHT [add:=(!+@[])] (fun n m => body of +) | 0; (mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNR (fun n m => body of +)@[add:=(!+@[])] | (U)
BETA (2 steps)
KNHT [add:=(!+@[]); n:=0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]] (body of +) | ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNHT [add:=(!+@[]); n:=0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]] n | ZCASE(+'s match @[add:=(!+@[]); n:=0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]]); (U)
KNH 0 | (U)
KNR 0 | (U)
IOTA (+'s match @[add:=(!+@[]); n:=0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]]) branch 0
KNHT [add:=(!+@[]); n:=0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]] m | ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNH (mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]] | (U)
KNHT [mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]] mul p m | (U)
KNHT [mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]] mul | 1[]; 1[]; (U)
KNH (!*)@[] | (U)
KNH 1[] | ZFIX(!*@[]); 1[]; ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNHT [] 1 | (U)
KNHT [] S | 0; (U)
KNR S | (U)
UNFOLD FIX (!*@[]) (reconstruct arg "S 0")
KNHT [mul:=(!*@[])] (fun n m => body of *) | S 0; 1[]; ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNR (fun n m => body of *)@[mul:=(!*@[])] | (U)
BETA (2 steps)
KNHT [mul:=(!*@[]); n:=S 0; m:=1[]] (body of *) | ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNHT [mul:=(!*@[]); n:=S 0; m:=1[]] n | ZCASE(match of * @[mul:=(!*@[]); n:=S 0; m:=1[]]); (U)
KNH S 0 | (U)
KNH S | 0; (U)
KNR S | (U)
IOTA (match of * @[mul:=(!*@[]); n:=S 0; m:=1[]]) branch S, arg p:=0
KNHT [mul:=(!*@[]); n:=S 0; m:=1[]; p:=0] (m + mul p m) | ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNHT [mul:=(!*@[]); n:=S 0; m:=1[]; p:=0] (+) | 1[]; (mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; (U)
KNR (+) | (U)
DELTA (+) (already injected)
KNH (!+)[] | (U)
KNHT [] (!+) | (U)
KNH (!+@[]) | (U)
KNH 1[] | ZFIX(!+@[]); (mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNHT [] 1 | (U)
KNHT [] S | 0; (U)
KNR S | (U)
UNFOLD FIX (!+@[]) (reconstruct arg "S 0")
KNHT [add:=(!+@[])] (fun n m => body of +) | S 0; (mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNR (fun n m => body of +)@[add:=(!+@[])] | (U)
BETA (2 steps)
KNHT [add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]] (match of +) | ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNHT [add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]] n | ZCASE(match of + @[add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]]); (U)
KNH S 0 | (U)
KNH S | 0; (U)
KNR S | (U)
IOTA (match of + @[add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]]) branch S, arg p:=0
KNHT [add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0] S (add p m) | ZCASE(2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]])
KNHT [add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0] S | (add p m)@[add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0]; (U)
KNR S | (U)
IOTA (2nd match of iseven @[iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]]) branch S, arg y:=(add p m)@[add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0]
KNHT [iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0], y:=(add p m)@[add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0]] ?iseven y |
KNHT [iseven:=(!iseven@[]); n:=S (add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0]; x:=(add p m)@[add:=(!+)@[]; n:=S 0; m:=(mul p m)@[mul:=(!*)@[]; n:=(S 1[]); m:=1[]; p:=1[]]; p:=0], y:=(add p m)@[add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0]] ?iseven | (add p m)@[add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0]
KNH (!iseven@[]) | (add p m)@[add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0]
KNH (add p m)@[add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0] | ZFIX(!iseven@[])
KNHT [add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0] add p m | (U)
KNHT [add:=(!+@[]); n:=S 0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; p:=0] add | 0; (mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; (U)
KNH (!@[]) | (U)
KNH 0 | ZFIX(!+@[]); (mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; ZFIX(!iseven@[])
KNR 0 | (U)
UNFOLD FIX (!+@[]) (trivial reconstruct arg "0")
KNHT [add:=(!+@[])] (fun n m => body of +) | 0; (mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]; ZFIX(!iseven@[])
KNR (fun n m => body of +)@[add:=(!+@[])] | (U)
BETA (2 steps)
KNHT [add:=(!+@[]); n:=0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]] (body of +) | ZFIX(!iseven@[])
KNHT [add:=(!+@[]); n:=0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]] n | ZCASE(match of + @[add:=(!+@[]); n:=0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]]); (U)
KNH 0 | (U)
KNR 0 | (U)
IOTA (match of + @[add:=(!+@[]); n:=0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]]) branch 0
KNHT [add:=(!+@[]); n:=0; m:=(mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0]] m | ZFIX(!iseven@[])
KNH (mul p m)@[mul:=(!*@[]); n:=S 0; m:=1[]; p:=0] | (U)
KNHT [mul:=(!*@[]); n:=S 0; m:=1[]; p:=0] (mul p m) | (U)
KNHT [mul:=(!*@[]); n:=S 0; m:=1[]; p:=0] mul | 0; 1[]; (U)
KNH (!*@[]) | (U)
KNH 0 | ZFIX(!*@[]); 1[]; ZFIX(!iseven@[])
KNR 0 | (U)
UNFOLD FIX (!*@[]) (trivial reconstruct argument "0")
KNHT [mul:=(!*@[])] (fun n m => body of *) | 0; 1[]; ZFIX(!iseven@[])
KNR (fun n m => body of *)@[mul:=(!*@[])] | (U)
BETA (2 steps)
KNHT [mul:=(!*@[]); n:=0; m:=1[]] (body of *) | ZFIX(!iseven@[])
KNHT [mul:=(!*@[]); n:=0; m:=1[]] n | ZCASE(match of * @ [mul:=(!*@[]); n:=0; m:=1[]]); (U)
KNH 0 | (U)
KNR 0 | (U)
IOTA (match of * @ [mul:=(!*@[]); n:=0; m:=1[]]) branch 0
KNHT [mul:=(!*@[]); n:=0; m:=1[]] 0 | ZFIX(!iseven@[])
KNR 0 | ZFIX(!iseven@[])
UNFOLD FIX !iseven@[] (trivial reconstruct arg "0")
KNHT [iseven:=!iseven@[]] (fun n => body of iseven) | 0
KNR (fun n => body of iseven)@[iseven:=!iseven@[]] | 0
BETA (1 step)
KNHT [iseven:=!iseven@[]; n:=0] (body of iseven) |
KNHT [iseven:=!iseven@[]; n:=0] n | ZCASE(1st match of iseven @ [iseven:=!iseven@[]; n:=0])
KNH 0 | (U)
KNR 0 | (U)
IOTA (1st match of iseven @ [iseven:=!iseven@[]; n:=0]) branch 0
KNHT [iseven:=!iseven@[]; n:=0] true |
KNR true |
FAPP_STACK (true | )
TO_CONSTR true
true