Definition Por' := R (.\ "p", "n", "s", "t";
 !Eva "n" "s" !(lam(lam(true)))
(!Eva "n" "t" !(lam(lam(false))) (.\"x"; ("p" (!Succ "n") "s" "t"))) !I).

Definition Por'2 := R (lam (lam (lam (lam (
  Eva #2 #1 (lam(lam(true)))
      (Eva #2 #0 (lam(lam(false))) (lam (#4 (Succ #3) #2 #1))) I ))))).


Lemma Por'_rec n s t: Por' (enc n) (tenc s) (tenc t) ==
  Eva (enc n) (tenc s) (lam(lam(true)))
 (Eva (enc n) (tenc t) (lam(lam(false))) (lam ((lam(Por'#0)) (Succ (enc n)) (tenc s) (tenc t)))) I.

Definition Por := Por' (enc 0).

Lemma Por'_n_Sn n s t : converges (Por' (enc n) (tenc s) (tenc t)) ↔ converges ( Por' (enc (S n)) (tenc s) (tenc t)).

Lemma Por'_n_conv n s t: converges (Por' (enc 0) (tenc s) (tenc t)) ↔ converges ( Por' (enc n) (tenc s) (tenc t)).

Lemma Por_correct_1a s t : converges s → converges (Por (tenc s) (tenc t)).


Lemma Por_correct_1b s t : converges t → converges( Por (tenc s) (tenc t)).

Lemma Por_correct_1 s t : converges s ∨ converges t → converges (Por (tenc s) (tenc t)).

Lemma Por_correct_2' s t n : converges (Por' (enc n) (tenc s) (tenc t)) → Por' (enc n) (tenc s) (tenc t) == true ∧ converges s ∨ Por' (enc n) (tenc s) (tenc t) == false ∧ converges t.

Lemma Por_correct_2 s t : converges (Por (tenc s) (tenc t)) →
  Por (tenc s) (tenc t) == true ∧ converges s ∨ Por (tenc s) (tenc t) == false ∧ converges t.

Lemma Por_correct_true s t : Por (tenc s) (tenc t) == true → converges s.

Lemma Por_correct_false s t : Por (tenc s) (tenc t) == false → converges t.