proposition: Lemma switch5IsPR : forall (f1 f2 f3 f4 f5 : nat -> nat -> nat) (g : nat -> nat), isPR 2 f1 -> isPR 2 f2 -> isPR 2 f3 -> isPR 2 f4 -> isPR 2 f5 -> isPR 1 g -> isPR 2 (fun n recs : nat => switchPR (g n) (switchPR (pred (g n)) (switchPR (pred (pred (g n))) (switchPR (pred (pred (pred (g n)))) (f1 n recs) (f2 n recs)) (f3 n recs)) (f4 n recs)) (f5 n recs)).
proof: Proof. intros ? ? ? ? ? g H H0 H1 H2 H3 H4. assert (H5: isPR 1 (fun trace : nat => pred (g trace))). { apply compose1_1IsPR. assumption. apply predIsPR. } assert (H6: isPR 1 (fun trace : nat => pred (pred (g trace)))). { apply compose1_1IsPR with (f := fun trace : nat => pred (g trace)). assumption. apply predIsPR. } assert (H7: isPR 1 (fun trace : nat => pred (pred (pred (g trace))))). { apply compose1_1IsPR with (f := fun trace : nat => pred (pred (g trace))). - assumption. - apply predIsPR. } apply compose2_3IsPR with (f1 := fun trace recs : nat => g trace) (f2 := fun trace recs : nat => switchPR (pred (g trace)) (switchPR (pred (pred (g trace))) (switchPR (pred (pred (pred (g trace)))) (f1 trace recs) (f2 trace recs)) (f3 trace recs)) (f4 trace recs)) (f3 := f5). - apply filter10IsPR; assumption. - apply compose2_3IsPR with (f1 := fun trace recs : nat => pred (g trace)) (f2 := fun trace recs : nat => switchPR (pred (pred (g trace))) (switchPR (pred (pred (pred (g trace)))) (f1 trace recs) (f2 trace recs)) (f3 trace recs)) (f3 := f4). + apply filter10IsPR with (g := fun trace : nat => pred (g trace)); assumption. + apply compose2_3IsPR with (f1 := fun trace recs : nat => pred (pred (g trace))) (f2 := fun trace recs : nat => switchPR (pred (pred (pred (g trace)))) (f1 trace recs) (f2 trace recs)) (f3 := f3). * apply filter10IsPR with (g := fun trace : nat => pred (pred (g trace))). assumption. * apply compose2_3IsPR with (f1 := fun trace recs : nat => pred (pred (pred (g trace)))) (f2 := f1) (f3 := f2). -- apply filter10IsPR with (g := fun trace : nat => pred (pred (pred (g trace)))). assumption. -- assumption. -- assumption. -- apply switchIsPR. * assumption. * apply switchIsPR; assumption. + assumption. + apply switchIsPR. - assumption. - apply switchIsPR. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)