Definition of parallel or

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 sconverges (Por (tenc s) (tenc t)).

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

Lemma Por_correct_1 s t : converges s converges tconverges (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) == trueconverges s.

Lemma Por_correct_false s t : Por (tenc s) (tenc t) == falseconverges t.